Quasi-Borel Spaces

This repository contains a formalization of Quasi-Borel Spaces¹ in Lean 4².

Usage

[[require]]
name = "quasi-borel-spaces"
git = "https://github.com/YellPika/quasi-borel-spaces"
rev = "main"

Differences from the Paper

We differ from the original paper¹ in the following ways:

• The definition of variable for Sigma types (e.g., (i : I) × P i or Σi : I, P i) is tweaked to more easily support types which are uninhabited.

• A QuasiBorelSpace instance is defined for all types (i : I) × P i (the paper only allows countable I).

• Probability measures from the paper are called PreProbabilityMeasures. We reserve the name ProbabilityMeasure for the monad defined in Section V-D¹, i.e. probability measures quotiented by the relation

  $$ (α, μ) \sim (β, ν) \iff ∀f\ldotp \int f\ d(α, μ) = \int f\ d(β, ν). $$

• We prove the probability measure monad is strong by constructing the strength operation (as in the Isabelle formalization³), instead of by showing bind is a morphism (as in Section V-D¹).

Footnotes

1. A Convenient Category for Higher-Order Probability Theory ↩ ↩² ↩³ ↩⁴

2. https://lean-lang.org/ ↩

3. Quasi_Borel_Spaces - Archive of Formal Proofs ↩