Omega quasi-borel spaces

This file defines omega quasi-borel spaces (ωQBS), which combine QuasiBorelSpace and OmegaCompletePartialOrder structures with a compatibility axiom stating that pointwise ω-suprema of ω-chains of morphisms are morphisms (Definition 3.5 in [Vákár–Staton, 2019]).

We prove that products and coproducts preserve the ωQBS structure (Lemma 3.9).

See [VKS19].

Definitions

• OmegaQuasiBorelSpace: A type with both an OmegaCompletePartialOrder and a QuasiBorelSpace, satisfying the compatibility axiom.

Instances

• instOmegaQuasiBorelSpaceProd: Products of ωQBSs are ωQBSs.
• instOmegaQuasiBorelSpaceSum: Coproducts of ωQBSs are ωQBSs.

class QuasiBorelSpaces.OmegaQuasiBorelSpace (α : Type u) extends OmegaCompletePartialOrder α, QuasiBorelSpace α : Type u

An ωQBS (Omega quasi-borel space) is a type equipped with both a QuasiBorelSpace and an OmegaCompletePartialOrder, satisfying the compatibility axiom: variables are closed under pointwise ω-suprema of ω-chains.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• ωSup : Chain α → α
• le_ωSup (c : Chain α) (i : ℕ) : c i ≤ ωSup c
• ωSup_le (c : Chain α) (x : α) : (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x
• IsVar : (ℝ → α) → Prop
• isVar_const (x : α) : IsVar fun (x_1 : ℝ) => x
• isVar_comp {f : ℝ → ℝ} {φ : ℝ → α} : Measurable f → IsVar φ → IsVar fun (r : ℝ) => φ (f r)
• isVar_cases' {ix : ℝ → ℕ} {φ : ℕ → ℝ → α} : Measurable ix → (∀ (n : ℕ), IsVar (φ n)) → IsVar fun (r : ℝ) => φ (ix r) r
• isHom_ωSup (c : OmegaCompletePartialOrder.Chain (ℝ → α)) : (∀ (n : ℕ), QuasiBorelSpace.IsHom (c n)) → QuasiBorelSpace.IsHom (OmegaCompletePartialOrder.ωSup c)

  Compatibility axiom (Definition 3.5 in [Vákár–Staton, 2019]): variables are closed under pointwise ω-suprema of ω-chains.

Helpers

theorem QuasiBorelSpaces.OmegaQuasiBorelSpace.IsHom.congrArg {γ : Type u_1} [QuasiBorelSpace γ] {f g : ℝ → γ} (h : ∀ (x : ℝ), f x = g x) : QuasiBorelSpace.IsHom f → QuasiBorelSpace.IsHom g

congruence for IsHom: equal functions preserve IsHom

theorem QuasiBorelSpaces.OmegaQuasiBorelSpace.IsHom.caseLeft {α : Type u} {γ : Type u_1} [QuasiBorelSpace α] [QuasiBorelSpace γ] {f : ℝ → α ⊕ γ} (hf : QuasiBorelSpace.IsHom f) (a₀ : α) : QuasiBorelSpace.IsHom fun (r : ℝ) => match f r with | Sum.inl a => a | Sum.inr val => a₀

extracting left component from sum variable with default

theorem QuasiBorelSpaces.OmegaQuasiBorelSpace.IsHom.caseRight {α : Type u} {γ : Type u_1} [QuasiBorelSpace α] [QuasiBorelSpace γ] {f : ℝ → α ⊕ γ} (hf : QuasiBorelSpace.IsHom f) (b₀ : γ) : QuasiBorelSpace.IsHom fun (r : ℝ) => match f r with | Sum.inr b => b | Sum.inl val => b₀

extracting right component from sum variable with default

theorem QuasiBorelSpaces.OmegaQuasiBorelSpace.isHom_ωSup_of_chain {X : Type u} {Y : Type v} [QuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (c : OmegaCompletePartialOrder.Chain (X → Y)) (hc : ∀ (n : ℕ), QuasiBorelSpace.IsHom (c n)) : QuasiBorelSpace.IsHom (OmegaCompletePartialOrder.ωSup c)

pointwise supremum of a chain of QBS morphisms is a QBS morphism (also known as the "Compatibility Axiom" for the exponential to be an ωQBS)

instance QuasiBorelSpaces.OmegaQuasiBorelSpace.instOmegaQuasiBorelSpaceProd {α : Type u} {β : Type v} [hα : OmegaQuasiBorelSpace α] [hβ : OmegaQuasiBorelSpace β] : OmegaQuasiBorelSpace (α × β)

Product of omega quasi-borel spaces is again an omega quasi-borel space.

Equations

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

noncomputable instance QuasiBorelSpaces.OmegaQuasiBorelSpace.instOmegaQuasiBorelSpaceSum {α : Type u} {β : Type v} [OmegaQuasiBorelSpace α] [OmegaQuasiBorelSpace β] : OmegaQuasiBorelSpace (α ⊕ β)

Coproduct of omega quasi-borel spaces is again an omega quasi-borel space.

Equations

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