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.

@[instance_reducible]

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_reducible]

instance QuasiBorelSpace.Real.instReal : QuasiBorelSpace ℝ

Equations

• QuasiBorelSpace.Real.instReal = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.ENNReal.instENNReal : QuasiBorelSpace ENNReal

Equations

• QuasiBorelSpace.ENNReal.instENNReal = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.Prop.instProp : QuasiBorelSpace Prop

Equations

• QuasiBorelSpace.Prop.instProp = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.Bool.instBool : QuasiBorelSpace Bool

Equations

• QuasiBorelSpace.Bool.instBool = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.Empty.instEmpty : QuasiBorelSpace Empty

Equations

• QuasiBorelSpace.Empty.instEmpty = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.PEmpty.instPEmpty : QuasiBorelSpace PEmpty.{u_4 + 1}

Equations

• QuasiBorelSpace.PEmpty.instPEmpty = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.Unit.instUnit : QuasiBorelSpace Unit

Equations

• QuasiBorelSpace.Unit.instUnit = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.PUnit.instPUnit : QuasiBorelSpace PUnit.{u_4 + 1}

Equations

• QuasiBorelSpace.PUnit.instPUnit = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

instance QuasiBorelSpace.Nat.instNat : QuasiBorelSpace ℕ

Equations

• QuasiBorelSpace.Nat.instNat = QuasiBorelSpace.ofMeasurableSpace

@[instance_reducible]

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.

@[instance_reducible]

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_reducible]

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

Equations

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

@[instance_reducible]

instance QuasiBorelSpace.instSubtype {A : Type u_1} [QuasiBorelSpace A] {p : A → Prop} : QuasiBorelSpace (Subtype p)

Equations

• QuasiBorelSpace.instSubtype = QuasiBorelSpace.lift Subtype.val

@[instance_reducible]

instance QuasiBorelSpace.ULift.instULift {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (ULift.{u_4, u_1} A)

Equations

• QuasiBorelSpace.ULift.instULift = QuasiBorelSpace.lift ULift.down

@[instance_reducible]

instance QuasiBorelSpace.PLift.instPLift {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (PLift A)

Equations

• QuasiBorelSpace.PLift.instPLift = QuasiBorelSpace.lift PLift.down

@[instance_reducible]

instance QuasiBorelSpace.instProd {A : Type u_4} {B : Type u_5} [QuasiBorelSpace A] [QuasiBorelSpace B] : QuasiBorelSpace (A × B)

Equations

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

@[instance_reducible]

instance QuasiBorelSpace.instForall {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] : QuasiBorelSpace ((i : I) → P i)

Equations

• QuasiBorelSpace.instForall = { IsVar := fun (φ : ℝ → (i : I) → P i) => ∀ (i : I), QuasiBorelSpace.IsVar fun (x : ℝ) => φ x i, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

class QuasiBorelSpace.IsHomAdd (A : Type u_4) [QuasiBorelSpace A] [Add A] : Prop

• isHom_const_add (c : A) : IsHom fun (x : A) => c + x
• isHom_add_const (c : A) : IsHom fun (x : A) => x + c

class QuasiBorelSpace.IsHomAdd₂ (A : Type u_4) [QuasiBorelSpace A] [Add A] : Prop

• isHom_add : IsHom fun (x : A × A) => x.1 + x.2

class QuasiBorelSpace.IsHomMul (A : Type u_4) [QuasiBorelSpace A] [Mul A] : Prop

• isHom_const_mul (c : A) : IsHom fun (x : A) => c * x
• isHom_mul_const (c : A) : IsHom fun (x : A) => x * c

class QuasiBorelSpace.IsHomMul₂ (A : Type u_4) [QuasiBorelSpace A] [Mul A] : Prop

• isHom_mul : IsHom fun (x : A × A) => x.1 * x.2

class MeasurableQuasiBorelSpace (A : Type u_4) [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_4) [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 φ