Quasi-Borel Spaces

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

Usage

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

Differences from the Papers

We differ from the original papers¹² 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¹).

• We provide a QuasiBorelSpace instance for Chains, which allows a more succinct definition of OmegaQuasiBorelSpace: we only require the supremum function ωSup : Chain A → A is a morphism.