Quasi-Borel Spaces

This file defines the concept of a quasi-borel space, as given by [HKSY17].

class QuasiBorelSpace (A : Type u_1) : Type u_1

A quasi‑borel space consists of a type A together with a set of "random variables" in ℝ → A satisfying closure under constants, measurable precomposition, and gluing along borel partitions.

See [HKSY17], Definition 7.

• IsVar : (ℝ → A) → Prop

  IsVar φ denotes whether φ is a random variable. Variables can be approximately thought of as the measurable functions in ℝ → A.

  Avoid using this predicate directly. Prefer IsHom instead.

• isVar_const (x : A) : IsVar fun (x_1 : ℝ) => x

  Variables are closed under constant functions.

• isVar_comp {f : ℝ → ℝ} {φ : ℝ → A} : Measurable f → IsVar φ → IsVar fun (r : ℝ) => φ (f r)

  Variables are closed under precomposition with measurable functions.

• isVar_cases' {ix : ℝ → ℕ} {φ : ℕ → ℝ → A} : Measurable ix → (∀ (n : ℕ), IsVar (φ n)) → IsVar fun (r : ℝ) => φ (ix r) r

  Variables are closed under gluing of countable families.

theorem QuasiBorelSpace.ext {A : Type u_1} {x y : QuasiBorelSpace A} (IsVar : IsVar = IsVar) : x = y

theorem QuasiBorelSpace.ext_iff {A : Type u_1} {x y : QuasiBorelSpace A} : x = y ↔ IsVar = IsVar

inductive QuasiBorelSpace.IsHom {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (f : A → B) : Prop

A function f : A → B between QuasiBorelSpaces is a morphism if it preserves variables under pre-composition.

See [HKSY17], Definition 11.

• intro {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} : (∀ ⦃φ : ℝ → A⦄, IsVar φ → IsVar fun (x : ℝ) => f (φ x)) → IsHom f

  Do not use this directly.

def QuasiBorelSpace.«termIsHom[_,_]» : Lean.ParserDescr

A function f : A → B between QuasiBorelSpaces is a morphism if it preserves variables under pre-composition.

See [HKSY17], Definition 11.

Equations

• One or more equations did not get rendered due to their size.

def QuasiBorelSpace.ofMeasurableSpace {A : Type u_1} [MeasurableSpace A] : QuasiBorelSpace A

Every MeasurableSpace induces a QuasiBorelSpace.

Equations

• QuasiBorelSpace.ofMeasurableSpace = { IsVar := fun (φ : ℝ → A) => Measurable φ, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

instance QuasiBorelSpace.Real.instReal : QuasiBorelSpace ℝ

Equations

• QuasiBorelSpace.Real.instReal = QuasiBorelSpace.ofMeasurableSpace

instance QuasiBorelSpace.ENNReal.instENNReal : QuasiBorelSpace ENNReal

Equations

• QuasiBorelSpace.ENNReal.instENNReal = QuasiBorelSpace.ofMeasurableSpace

def QuasiBorelSpace.toMeasurableSpace {A : Type u_1} [QuasiBorelSpace A] : MeasurableSpace A

Every QuasiBorelSpace induces a MeasurableSpace.

See [HKSY17], Proposition 14.

Equations

• One or more equations did not get rendered due to their size.

def QuasiBorelSpace.lift {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] (f : B → A) : QuasiBorelSpace B

We can lift a QuasiBorelSpace from one type to another.

Equations

• QuasiBorelSpace.lift f = { IsVar := fun (φ : ℝ → B) => QuasiBorelSpace.IsVar fun (x : ℝ) => f (φ x), isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

instance QuasiBorelSpace.instInhabited {A : Type u_1} : Inhabited (QuasiBorelSpace A)

Equations

• QuasiBorelSpace.instInhabited = { default := QuasiBorelSpace.ofMeasurableSpace }

class MeasurableQuasiBorelSpace (A : Type u_3) [QuasiBorelSpace A] [MeasurableSpace A] : Prop

A measurable quasi-borel space is the quasi-borel space where the notion of variable aligns with measurable functions.

• isHom_iff_measurable (φ : ℝ → A) : QuasiBorelSpace.IsHom φ ↔ Measurable φ

  Variables are measurable functions.

class DiscreteQuasiBorelSpace (A : Type u_3) [QuasiBorelSpace A] [MeasurableSpace A] extends DiscreteMeasurableSpace A, MeasurableQuasiBorelSpace A : Prop

A discrete quasi-borel space is the quasi-borel space analogue of the discrete measurable space.

• forall_measurableSet (s : Set A) : MeasurableSet s
• isHom_iff_measurable (φ : ℝ → A) : QuasiBorelSpace.IsHom φ ↔ Measurable φ

instance QuasiBorelSpace.Prop.instProp : QuasiBorelSpace Prop

Equations

• QuasiBorelSpace.Prop.instProp = QuasiBorelSpace.ofMeasurableSpace

@[simp]

theorem QuasiBorelSpace.Prop.IsVar_def (φ : ℝ → Prop) : IsVar φ = Measurable φ