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 [VKS19]).

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.

class OmegaQuasiBorelSpace (A : Type u_1) extends OmegaCompletePartialOrder A, QuasiBorelSpace A : Type u_1

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

  Compatibility axiom (Definition 3.5 in [VKS19]): variables are closed under pointwise ω-suprema of ω-chains.

theorem OmegaQuasiBorelSpace.isHom_ωSup' {A : Type u_1} {B : Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : OmegaQuasiBorelSpace B} (f : A → OmegaCompletePartialOrder.Chain B) (hc : QuasiBorelSpace.IsHom f) : QuasiBorelSpace.IsHom fun (x : A) => OmegaCompletePartialOrder.ωSup (f x)

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 OmegaQuasiBorelSpace.instOfQuasiBorelSpaceOfOmegaCompletePartialOrderOfSubsingleton {A : Type u_1} [QuasiBorelSpace A] [OmegaCompletePartialOrder A] [Subsingleton A] : OmegaQuasiBorelSpace A

Equations

• OmegaQuasiBorelSpace.instOfQuasiBorelSpaceOfOmegaCompletePartialOrderOfSubsingleton = { toOmegaCompletePartialOrder := inst✝¹, toQuasiBorelSpace := inst✝², isHom_ωSup := ⋯ }