Binary Products of Quasi-Borel Spaces #
This file defines binary products of quasi-borel spaces by giving a
QuasiBorelSpace instance for the · × · type.
See [HKSY17], Proposition 16.
instance
QuasiBorelSpace.Prod.instProd
{A : Type u_1}
{B : Type u_2}
[QuasiBorelSpace A]
[QuasiBorelSpace B]
:
QuasiBorelSpace (A × B)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
QuasiBorelSpace.Prod.isHom_fst
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
:
theorem
QuasiBorelSpace.Prod.isHom_fst'
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
{f : A → B × C}
(hf : IsHom f)
:
IsHom fun (x : A) => (f x).1
@[simp]
theorem
QuasiBorelSpace.Prod.isHom_snd
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
:
theorem
QuasiBorelSpace.Prod.isHom_snd'
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
{f : A → B × C}
(hf : IsHom f)
:
IsHom fun (x : A) => (f x).2
theorem
QuasiBorelSpace.Prod.isHom_mk
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
{f : A → B}
(hf : IsHom f)
{g : A → C}
(hg : IsHom g)
:
@[simp]
theorem
QuasiBorelSpace.Prod.isHom_iff
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
(f : A → B × C)
:
instance
QuasiBorelSpace.Prod.instMeasurableQuasiBorelSpaceProd
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
[MeasurableSpace A]
[MeasurableSpace B]
[MeasurableQuasiBorelSpace A]
[MeasurableQuasiBorelSpace B]
:
MeasurableQuasiBorelSpace (A × B)
theorem
QuasiBorelSpace.Prod.isHom_map
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
{D : Type u_4}
{x✝³ : QuasiBorelSpace D}
{f : A → B}
{g : C → D}
(hf : IsHom f)
(hg : IsHom g)
:
theorem
QuasiBorelSpace.Prod.isHom_of_uncurry
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{C : Type u_3}
{x✝² : QuasiBorelSpace C}
{D : Type u_4}
{x✝³ : QuasiBorelSpace D}
{f : A → B → C}
(hf : IsHom (Function.uncurry f))
{g : D → A}
(hg : IsHom g)
{h : D → B}
(hh : IsHom h)
:
IsHom fun (x : D) => f (g x) (h x)
instance
OmegaQuasiBorelSpace.Prod.instProd
{A : Type u_1}
{B : Type u_2}
[OmegaQuasiBorelSpace A]
[OmegaQuasiBorelSpace B]
:
OmegaQuasiBorelSpace (A × B)
Equations
- OmegaQuasiBorelSpace.Prod.instProd = { toOmegaCompletePartialOrder := Prod.instOmegaCompletePartialOrder, toQuasiBorelSpace := QuasiBorelSpace.Prod.instProd, isHom_ωSup := ⋯ }
theorem
QuasiBorelSpace.Measure.isHom_lintegral
{A : Type u_1}
{B : Type u_2}
[QuasiBorelSpace A]
[QuasiBorelSpace B]
[MeasurableSpace A]
[MeasurableSpace B]
[StandardBorelSpace B]
[MeasurableQuasiBorelSpace B]
{f : A → B → ENNReal}
(hf : IsHom fun (x : A × B) => f x.1 x.2)
(μ : MeasureTheory.Measure B)
[MeasureTheory.SFinite μ]
: