Exponentials for ω-quasi-borel spaces

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

structure OmegaQuasiBorelHom (X : Type u_1) (Y : Type u_2) [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : Type (max u_1 u_2)

Exponential objects: functions that are both Scott-Continuous and Measurable (QBS Morphisms)

• toFun : X → Y
• isHom' : QuasiBorelSpace.IsHom (OmegaQuasiBorelHom.toFun✝ self)
• ωScottContinuous' : OmegaCompletePartialOrder.ωScottContinuous (OmegaQuasiBorelHom.toFun✝ self)

def «term_→ω𝒒_» : Lean.TrailingParserDescr

Exponential objects: functions that are both Scott-Continuous and Measurable (QBS Morphisms)

Equations

• «term_→ω𝒒_» = Lean.ParserDescr.trailingNode `«term_→ω𝒒_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ω𝒒 ") (Lean.ParserDescr.cat `term 25))

instance OmegaQuasiBorelHom.instFunLike {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : FunLike (X →ω𝒒 Y) X Y

Equations

• OmegaQuasiBorelHom.instFunLike = { coe := fun (f : X →ω𝒒 Y) => OmegaQuasiBorelHom.toFun✝ f, coe_injective' := ⋯ }

def OmegaQuasiBorelHom.Simps.coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : X → Y

A simps projection for function coercion.

Equations

• OmegaQuasiBorelHom.Simps.coe f = ⇑f

theorem OmegaQuasiBorelHom.ext {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] {f g : X →ω𝒒 Y} (h : ∀ (x : X), f x = g x) : f = g

theorem OmegaQuasiBorelHom.ext_iff {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] {f g : X →ω𝒒 Y} : f = g ↔ ∀ (x : X), f x = g x

def OmegaQuasiBorelHom.copy {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) (f' : X → Y) (h : f' = ⇑f) : X →ω𝒒 Y

Copy of a OmegaQuasiBorelHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toFun := f', isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.coe_mk {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] {f : X → Y} (hf₁ : QuasiBorelSpace.IsHom f) (hf₂ : OmegaCompletePartialOrder.ωScottContinuous f) : ⇑{ toFun := f, isHom' := hf₁, ωScottContinuous' := hf₂ } = f

@[simp]

theorem OmegaQuasiBorelHom.eta {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : { toFun := ⇑f, isHom' := ⋯, ωScottContinuous' := ⋯ } = f

@[simp]

theorem OmegaQuasiBorelHom.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : OmegaQuasiBorelHom.toFun✝ f = ⇑f

@[simp]

theorem OmegaQuasiBorelHom.isHom_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : QuasiBorelSpace.IsHom ⇑f

@[simp]

theorem OmegaQuasiBorelHom.ωScottContinuous_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : OmegaCompletePartialOrder.ωScottContinuous ⇑f

@[simp]

theorem OmegaQuasiBorelHom.monotone_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : Monotone ⇑f

instance OmegaQuasiBorelHom.instPartialOrder {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : PartialOrder (X →ω𝒒 Y)

Equations

• OmegaQuasiBorelHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯

def OmegaQuasiBorelHom.toOrderHom {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : X →o Y

Converts an ωQBS Hom to a Poset Hom.

Equations

• ↑f = { toFun := ⇑f, monotone' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.toOrderHom_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) (a : X) : ↑f a = f a

def OmegaQuasiBorelHom.toContinuousHom {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : X →𝒄 Y

Converts a ωQBS Hom to an ωCPO Hom.

Equations

• ↑f = { toFun := ⇑f, monotone' := ⋯, map_ωSup' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.toContinuousHom_apply {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) (a : X) : ↑f a = f a

def OmegaQuasiBorelHom.toQuasiBorelHom {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) : X →𝒒 Y

Converts a ωQBS Hom to a quasi-Borel Hom.

Equations

• ↑f = { toFun := ⇑f, property := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.toQuasiBorelHom_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (f : X →ω𝒒 Y) (a : X) : ↑f a = f a

instance OmegaQuasiBorelHom.instOmegaCompletePartialOrder {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : OmegaCompletePartialOrder (X →ω𝒒 Y)

The ωCPO structure on the exponential is the pointwise order.

Equations

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

@[simp]

theorem OmegaQuasiBorelHom.ωSup_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (c : OmegaCompletePartialOrder.Chain (X →ω𝒒 Y)) (a✝ : X) : (OmegaCompletePartialOrder.ωSup c) a✝ = OmegaCompletePartialOrder.ωSup (c.map { toFun := DFunLike.coe, monotone' := ⋯ }) a✝

@[simp]

theorem OmegaQuasiBorelHom.lt_def {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (a b : X →ω𝒒 Y) : (a < b) = (⇑a < ⇑b)

@[simp]

theorem OmegaQuasiBorelHom.le_def {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (a b : X →ω𝒒 Y) : (a ≤ b) = (⇑a ≤ ⇑b)

instance OmegaQuasiBorelHom.instQuasiBorelSpace {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : QuasiBorelSpace (X →ω𝒒 Y)

The QBS structure on the ωHoms is identical to normal QBS Homs.

Equations

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

instance OmegaQuasiBorelHom.instMeasurableSpace {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : MeasurableSpace (X →ω𝒒 Y)

Equations

• OmegaQuasiBorelHom.instMeasurableSpace = QuasiBorelSpace.toMeasurableSpace

theorem OmegaQuasiBorelHom.isHom_def {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (φ : ℝ → X →ω𝒒 Y) : QuasiBorelSpace.IsHom φ ↔ QuasiBorelSpace.IsHom fun (x : ℝ × X) => (φ x.1) x.2

@[simp]

theorem OmegaQuasiBorelHom.isHom_eval {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : QuasiBorelSpace.IsHom fun (p : (X →ω𝒒 Y) × X) => p.1 p.2

@[simp]

theorem OmegaQuasiBorelHom.ωScottContinuous_eval {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : OmegaCompletePartialOrder.ωScottContinuous fun (p : (X →ω𝒒 Y) × X) => p.1 p.2

theorem OmegaQuasiBorelHom.isHom_eval' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] [QuasiBorelSpace X] {f : X → Y →ω𝒒 Z} (hf : QuasiBorelSpace.IsHom f) {g : X → Y} (hg : QuasiBorelSpace.IsHom g) : QuasiBorelSpace.IsHom fun (x : X) => (f x) (g x)

theorem OmegaQuasiBorelHom.ωScottContinuous_eval' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] {f : X → Y →ω𝒒 Z} (hf : OmegaCompletePartialOrder.ωScottContinuous f) {g : X → Y} (hg : OmegaCompletePartialOrder.ωScottContinuous g) : OmegaCompletePartialOrder.ωScottContinuous fun (x : X) => (f x) (g x)

@[simp]

theorem OmegaQuasiBorelHom.isHom_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] [QuasiBorelSpace X] (f : X → Y →ω𝒒 Z) : QuasiBorelSpace.IsHom f ↔ QuasiBorelSpace.IsHom fun (x : X × Y) => (f x.1) x.2

theorem OmegaQuasiBorelHom.isHom_mk {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] {f : X → Y → Z} (h₁ : QuasiBorelSpace.IsHom fun (x : X × Y) => f x.1 x.2) (h₂ : ∀ (x : X), OmegaCompletePartialOrder.ωScottContinuous (f x)) : QuasiBorelSpace.IsHom fun (x : X) => { toFun := f x, isHom' := ⋯, ωScottContinuous' := ⋯ }

theorem OmegaQuasiBorelHom.ωScottContinuous_mk {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] {f : X → Y → Z} (h₁ : ∀ (x : X), QuasiBorelSpace.IsHom (f x)) (h₂ : OmegaCompletePartialOrder.ωScottContinuous fun (x : X × Y) => f x.1 x.2) : OmegaCompletePartialOrder.ωScottContinuous fun (x : X) => { toFun := f x, isHom' := ⋯, ωScottContinuous' := ⋯ }

instance OmegaQuasiBorelHom.instOmegaQuasiBorelSpace {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : OmegaQuasiBorelSpace (X →ω𝒒 Y)

The exponential object is an ωQBS.

Equations

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

Operations

def OmegaQuasiBorelHom.id {X : Type u_1} [OmegaQuasiBorelSpace X] : X →ω𝒒 X

Identity OmegaQuasiBorelHoms.

Equations

• OmegaQuasiBorelHom.id = { toFun := fun (x : X) => x, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.id_coe {X : Type u_1} [OmegaQuasiBorelSpace X] (x : X) : id x = x

def OmegaQuasiBorelHom.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Y →ω𝒒 Z) (g : X →ω𝒒 Y) : X →ω𝒒 Z

Function composition for OmegaQuasiBorelHoms.

Equations

• f.comp g = { toFun := fun (x : X) => f (g x), isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.comp_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Y →ω𝒒 Z) (g : X →ω𝒒 Y) (x : X) : (f.comp g) x = f (g x)

def OmegaQuasiBorelHom.Prod.mk {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : X →ω𝒒 Y) (g : X →ω𝒒 Z) : X →ω𝒒 Y × Z

Product construction as an OmegaQuasiBorelHom.

Equations

• OmegaQuasiBorelHom.Prod.mk f g = { toFun := fun (x : X) => (f x, g x), isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.Prod.mk_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : X →ω𝒒 Y) (g : X →ω𝒒 Z) (x : X) : (mk f g) x = (f x, g x)

def OmegaQuasiBorelHom.Prod.fst {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : X × Y →ω𝒒 X

First product projection.

Equations

• OmegaQuasiBorelHom.Prod.fst = { toFun := fun (x : X × Y) => x.1, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.Prod.fst_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (x : X × Y) : fst x = x.1

def OmegaQuasiBorelHom.Prod.snd {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : X × Y →ω𝒒 Y

Second product projection.

Equations

• OmegaQuasiBorelHom.Prod.snd = { toFun := fun (x : X × Y) => x.2, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.Prod.snd_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (x : X × Y) : snd x = x.2

def OmegaQuasiBorelHom.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z × X →ω𝒒 Y) : Z →ω𝒒 X →ω𝒒 Y

Currying for OmegaQuasiBorelHoms.

Equations

• f.curry = { toFun := fun (x : Z) => { toFun := fun (y : X) => f (x, y), isHom' := ⋯, ωScottContinuous' := ⋯ }, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.curry_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z × X →ω𝒒 Y) (x : Z) : f.curry x = { toFun := fun (y : X) => f (x, y), isHom' := ⋯, ωScottContinuous' := ⋯ }

def OmegaQuasiBorelHom.eval {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] : (X →ω𝒒 Y) × X →ω𝒒 Y

Function application is an OmegaQuasiBorelHom.

Equations

• OmegaQuasiBorelHom.eval = { toFun := fun (x : (X →ω𝒒 Y) × X) => x.1 x.2, isHom' := ⋯, ωScottContinuous' := ⋯ }

@[simp]

theorem OmegaQuasiBorelHom.eval_coe {X : Type u_1} {Y : Type u_2} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] (x : (X →ω𝒒 Y) × X) : eval x = x.1 x.2

def OmegaQuasiBorelHom.uncurry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : X →ω𝒒 Y →ω𝒒 Z) : X × Y →ω𝒒 Z

Uncurrying for OmegaQuasiBorelHoms.

Equations

• f.uncurry = OmegaQuasiBorelHom.eval.comp (OmegaQuasiBorelHom.Prod.mk (f.comp OmegaQuasiBorelHom.Prod.fst) OmegaQuasiBorelHom.Prod.snd)

@[simp]

theorem OmegaQuasiBorelHom.uncurry_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : X →ω𝒒 Y →ω𝒒 Z) (x : X × Y) : f.uncurry x = (f x.1) x.2

@[simp]

theorem OmegaQuasiBorelHom.curry_uncurry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z →ω𝒒 X →ω𝒒 Y) : f.uncurry.curry = f

@[simp]

theorem OmegaQuasiBorelHom.uncurry_curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [OmegaQuasiBorelSpace X] [OmegaQuasiBorelSpace Y] [OmegaQuasiBorelSpace Z] (f : Z × X →ω𝒒 Y) : f.curry.uncurry = f