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

• 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¹).