Exponentials for ω-quasi-borel spaces #

This file defines the function space OmegaHom X Y (written X →ω𝒒 Y) of Scott-continuous QBS morphisms. It proves that this space is itself an ωQBS.

source

def QuasiBorelSpaces.OmegaHom (X : Type u) (Y : Type v) [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

Type (max 0 u v)

the type of the Exponential Object: Functions that are both Scott-Continuous and Measurable (QBS Morphisms)

Equations

(X →ω𝒒 Y) = { f : X →𝒄 Y // QuasiBorelSpace.IsHom ⇑f }

Instances For

source

def QuasiBorelSpaces.«term_→ω𝒒_» :

Lean.TrailingParserDescr

the type of the Exponential Object: Functions that are both Scott-Continuous and Measurable (QBS Morphisms)

Equations

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

Instances For

source

instance QuasiBorelSpaces.OmegaHom.instFunLike {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

FunLike (X →ω𝒒 Y) X Y

Equations

QuasiBorelSpaces.OmegaHom.instFunLike = { coe := fun (f : X →ω𝒒 Y) => ⇑↑f, coe_injective' := ⋯ }

source

theorem QuasiBorelSpaces.OmegaHom.ext {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] {f g : X →ω𝒒 Y} (h : ∀ (x : X), f x = g x) :

f = g

source

theorem QuasiBorelSpaces.OmegaHom.ext_iff {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] {f g : X →ω𝒒 Y} :

f = g ↔ ∀ (x : X), f x = g x

source

@[simp]

theorem QuasiBorelSpaces.OmegaHom.isHom_coe {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) :

QuasiBorelSpace.IsHom ⇑f

source

@[simp]

theorem QuasiBorelSpaces.OmegaHom.monotone {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) :

Monotone ⇑f

source

instance QuasiBorelSpaces.OmegaHom.instOmegaCompletePartialOrder {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

OmegaCompletePartialOrder (X →ω𝒒 Y)

the ωCPO structure on the exponential is the pointwise order

Equations

QuasiBorelSpaces.OmegaHom.instOmegaCompletePartialOrder = OmegaCompletePartialOrder.subtype (fun (f : X →𝒄 Y) => QuasiBorelSpace.IsHom ⇑f) ⋯

source

instance QuasiBorelSpaces.OmegaHom.instQuasiBorelSpace {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

QuasiBorelSpace (X →ω𝒒 Y)

the QBS structure on the exponential (the standard Function Space definition)

Equations

QuasiBorelSpaces.OmegaHom.instQuasiBorelSpace = { IsVar := fun (φ : ℝ → X →ω𝒒 Y) => QuasiBorelSpace.IsHom fun (x : ℝ × X) => (φ x.1) x.2, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

source

theorem QuasiBorelSpaces.OmegaHom.isHom_def {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (φ : ℝ → X →ω𝒒 Y) :

QuasiBorelSpace.IsHom φ ↔ QuasiBorelSpace.IsHom fun (x : ℝ × X) => (φ x.1) x.2

uncurried random variables correspond to morphisms

source

@[simp]

theorem QuasiBorelSpaces.OmegaHom.isHom_eval {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

QuasiBorelSpace.IsHom fun (p : (X →ω𝒒 Y) × X) => p.1 p.2

OmegaQuasiBorelSpace Instance #

source

instance QuasiBorelSpaces.OmegaHom.instOmegaQuasiBorelSpace {X : Type u} {Y : Type v} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] :

OmegaQuasiBorelSpace (X →ω𝒒 Y)

the exponential object is an ωQBS, we must show that the ω-supremum operation is measurable

Equations

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

Currying Operations #

source

def QuasiBorelSpaces.OmegaHom.curry {X : Type u} {Y : Type v} {Z : Type w} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z × X →ω𝒒 Y) :

Z →ω𝒒 X →ω𝒒 Y

currying map: (Z × X → Y) → (Z → (X → Y)) constructed using explicit ContinuousHom records to match fields monotone' and map_ωSup'.

Equations

f.curry = ⟨{ toFun := fun (z : Z) => ⟨{ toFun := fun (x : X) => f (z, x), monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

Instances For

source

def QuasiBorelSpaces.OmegaHom.uncurry {X : Type u} {Y : Type v} {Z : Type w} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z →ω𝒒 X →ω𝒒 Y) :

Z × X →ω𝒒 Y

uncurrying map: (Z → (X → Y)) → (Z × X → Y)

Equations

f.uncurry = ⟨{ toFun := fun (p : Z × X) => (f p.1) p.2, monotone' := ⋯, map_ωSup' := ⋯ }, ⋯⟩

Instances For

source

@[simp]

theorem QuasiBorelSpaces.OmegaHom.curry_uncurry {X : Type u} {Y : Type v} {Z : Type w} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z →ω𝒒 X →ω𝒒 Y) :

f.uncurry.curry = f

source

@[simp]

theorem QuasiBorelSpaces.OmegaHom.uncurry_curry {X : Type u} {Y : Type v} {Z : Type w} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z × X →ω𝒒 Y) :

f.curry.uncurry = f