Coproduct Variables

This file defines a structure representing coproduct variables.

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

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.

• mk' :: (
• index : ℝ → ℕ

  Countably partitions ℝ.

• measurable_index : Measurable self.index

  Each partition is measurable.

• embed : ℕ → I

  Each partition has an index in I.

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

  Each partition has a variable.

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

  Each variable is a morphism.

• )

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

Equations

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

@[instance_reducible]

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

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

Equations

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

def QuasiBorelSpace.Sigma.Var.mk {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {Index : Type u_6} [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.

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.

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 = QuasiBorelSpace.Sigma.Var.mk x.embed (fun (r : ℝ) => x.index (f r)) (fun (i : ℕ) (r : ℝ) => x.var i (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.

def QuasiBorelSpace.Sigma.Var.distrib {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] {A : Type u_3} [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φ₁ φ₂ = QuasiBorelSpace.Sigma.Var.mk φ₂.embed φ₂.index (fun (i : ℕ) (r : ℝ) => (φ₁ r, φ₂.var i r)) ⋯ ⋯

noncomputable def QuasiBorelSpace.Sigma.Var.ofMeasurable {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] [Countable I] {φ : ℝ → Sigma P} (hφ : Measurable φ) : Var I P

Equations

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