Small Coproducts of Quasi-Borel Spaces

This file defines small coproducts of quasi-borel spaces by giving a QuasiBorelSpace instance for the Σ type.

See [HKSY17], Proposition 17.

structure QuasiBorelSpace.Sigma.Var (I : Type u_8) (P : I → Type u_9) [(i : I) → QuasiBorelSpace (P i)] : Type (max u_8 u_9)

Represents a variable for a Σ-type. Intuitively, a variable in Σi, P i is a gluing of a countable number of variables, each in some P i.

• embed : ℕ → I

  Each index represents some I.

• index : ℝ → ℕ

  Obtains the index of the underlying variable, given the intended input.

• var (i : ℕ) : ℝ → P (self.embed i)

  The family of variables.

• isHom_var (i : ℕ) : IsHom (self.var i)

  Each variable is, in fact, a variable.

• measurable_index : Measurable self.index

  The index function is measurable.

def QuasiBorelSpace.Sigma.Var.apply {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (x : Var I P) (r : ℝ) : Sigma P

Since every Var represents a variable, each Var induces a function ℝ → Σi, P i.

Equations

• x.apply r = ⟨x.embed (x.index r), x.var (x.index r) r⟩

@[simp]

theorem QuasiBorelSpace.Sigma.Var.apply_mk {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {f : ℕ → I} {i : ℝ → ℕ} {φ : (i : ℕ) → ℝ → P (f i)} {r : ℝ} (hφ : ∀ (i : ℕ), IsHom (φ i)) (hi : Measurable i) : { embed := f, index := i, var := φ, isHom_var := hφ, measurable_index := hi }.apply r = ⟨f (i r), φ (i r) r⟩

def QuasiBorelSpace.Sigma.Var.mk' {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (Index : Type u_8) [Encodable Index] (embed : Index → I) (index : ℝ → Index) (var : (i : Index) → ℝ → P (embed i)) (isHom_var : ∀ (i : Index), IsHom (var i)) (measurable_index : Measurable index) : Var I P

A Var can be constructed from any Encodable index type.

Equations

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

@[simp]

theorem QuasiBorelSpace.Sigma.Var.apply_mk' {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {J : Type u_8} [Encodable J] {f : J → I} {i : ℝ → J} {φ : (i : J) → ℝ → P (f i)} {r : ℝ} (hφ : ∀ (i : J), IsHom (φ i)) (hi : Measurable i) : (mk' J f i φ hφ hi).apply r = ⟨f (i r), φ (i r) r⟩

instance QuasiBorelSpace.Sigma.Var.instCoeFunForallRealSigma {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] : CoeFun (Var I P) fun (x : Var I P) => ℝ → Sigma P

Equations

• QuasiBorelSpace.Sigma.Var.instCoeFunForallRealSigma = { coe := QuasiBorelSpace.Sigma.Var.apply }

def QuasiBorelSpace.Sigma.Var.const {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (x : Sigma P) : Var I P

The constant variable.

Equations

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

@[simp]

theorem QuasiBorelSpace.Sigma.Var.const_apply {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (x : Sigma P) (r : ℝ) : (const x).apply r = x

def QuasiBorelSpace.Sigma.Var.comp {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {f : ℝ → ℝ} (hf : Measurable f) (x : Var I P) : Var I P

Composition under measurable functions.

Equations

• QuasiBorelSpace.Sigma.Var.comp hf x = { embed := x.embed, index := fun (r : ℝ) => x.index (f r), var := fun (i : ℕ) (r : ℝ) => x.var i (f r), isHom_var := ⋯, measurable_index := ⋯ }

@[simp]

theorem QuasiBorelSpace.Sigma.Var.comp_apply {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {f : ℝ → ℝ} (hf : Measurable f) (x : Var I P) (r : ℝ) : (comp hf x).apply r = x.apply (f r)

def QuasiBorelSpace.Sigma.Var.cases {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {ix : ℝ → ℕ} (hix : Measurable ix) (φ : ℕ → Var I P) : Var I P

Gluing of a countable number of variables.

Equations

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

@[simp]

theorem QuasiBorelSpace.Sigma.Var.cases_apply {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {ix : ℝ → ℕ} (hix : Measurable ix) (φ : ℕ → Var I P) (r : ℝ) : (cases hix φ).apply r = (φ (ix r)).apply r

def QuasiBorelSpace.Sigma.Var.distrib {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} [QuasiBorelSpace A] {φ₁ : ℝ → A} (hφ₁ : IsHom φ₁) (φ₂ : Var I P) : Var I fun (i : I) => A × P i

Normal QuasiBorelSpace.Vars can be pushed 'inside' a Var.

Equations

• QuasiBorelSpace.Sigma.Var.distrib hφ₁ φ₂ = { embed := φ₂.embed, index := φ₂.index, var := fun (i : ℕ) (r : ℝ) => (φ₁ r, φ₂.var i r), isHom_var := ⋯, measurable_index := ⋯ }

@[simp]

theorem QuasiBorelSpace.Sigma.Var.distrib_apply {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} [QuasiBorelSpace A] {φ₁ : ℝ → A} (hφ₁ : IsHom φ₁) (φ₂ : Var I P) (r : ℝ) : (distrib hφ₁ φ₂).apply r = ⟨(φ₂.apply r).fst, (φ₁ r, (φ₂.apply r).snd)⟩

instance QuasiBorelSpace.Sigma.instSigma {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] : QuasiBorelSpace ((i : I) × P i)

Equations

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

theorem QuasiBorelSpace.Sigma.isHom_def {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (φ : ℝ → (i : I) × P i) : IsHom φ ↔ ∃ (ψ : Var I P), ∀ (r : ℝ), φ r = ψ.apply r

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_mk {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] (i : I) : IsHom fun (x : P i) => ⟨i, x⟩

theorem QuasiBorelSpace.Sigma.isHom_mk' {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} [QuasiBorelSpace A] {i : I} {f : A → P i} (hf : IsHom f) : IsHom fun (x : A) => ⟨i, f x⟩

theorem QuasiBorelSpace.Sigma.isHom_elim {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} [QuasiBorelSpace A] {f : Sigma P → A} (hf : ∀ (i : I), IsHom fun (x : P i) => f ⟨i, x⟩) : IsHom f

theorem QuasiBorelSpace.Sigma.isHom_elim' {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} {B : Type u_6} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : (i : I) → P i → B} (hf : ∀ (i : I), IsHom (f i)) {g : A → (i : I) × P i} (hg : IsHom g) : IsHom fun (x : A) => f (g x).fst (g x).snd

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_fst {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] [QuasiBorelSpace I] : IsHom Sigma.fst

theorem QuasiBorelSpace.Sigma.isHom_snd {I : Type u_1} {A : Type u_5} [QuasiBorelSpace A] : IsHom Sigma.snd

theorem QuasiBorelSpace.Sigma.isHom_distrib {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} [QuasiBorelSpace A] : IsHom fun (x : A × Sigma P) => ⟨x.2.fst, (x.1, x.2.snd)⟩

theorem QuasiBorelSpace.Sigma.isHom_distrib' {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_5} {B : Type u_6} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A × Sigma P → B} (hf : IsHom fun (x : (i : I) × A × P i) => f (x.snd.1, ⟨x.fst, x.snd.2⟩)) : IsHom f

theorem QuasiBorelSpace.Sigma.isHom_map {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {J : Type u_3} {Q : J → Type u_4} [(j : J) → QuasiBorelSpace (Q j)] {f : I → J} {g : (i : I) → P i → Q (f i)} (hg : ∀ (i : I), IsHom (g i)) : IsHom (Sigma.map f g)

instance QuasiBorelSpace.Sigma.instMeasurableQuasiBorelSpaceSigmaOfCountable {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] [Countable I] [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] : MeasurableQuasiBorelSpace (Sigma P)