This file provides basic facts about quasi-Borel spaces.

IsVar lemmas

theorem QuasiBorelSpace.isVar_cases {A : Type u_1} {x✝ : QuasiBorelSpace A} {I : Type u_5} [Countable I] {ix : ℝ → I} {φ : I → ℝ → A} (hix : Measurable ix) (hφ : ∀ (n : I), IsVar (φ n)) : IsVar fun (r : ℝ) => φ (ix r) r

@[simp]

theorem QuasiBorelSpace.isVar_iff_isHom {A : Type u_1} {x✝ : QuasiBorelSpace A} (f : ℝ → A) : IsVar f ↔ IsHom f

MeasurableQuasiBorelSpaces

instance QuasiBorelSpace.instMeasurableQuasiBorelSpace {A : Type u_1} {hA : MeasurableSpace A} : MeasurableQuasiBorelSpace A

theorem QuasiBorelSpace.isHom_of_measurable {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} {x✝³ : MeasurableSpace B} [MeasurableQuasiBorelSpace A] [MeasurableQuasiBorelSpace B] {f : A → B} (hf : Measurable f) : IsHom f

@[simp]

theorem QuasiBorelSpace.measurableSet_toMeasurableSpace {A : Type u_1} {x✝ : QuasiBorelSpace A} (X : Set A) : MeasurableSet X ↔ ∀ {φ : ℝ → A}, IsHom φ → MeasurableSet (φ ⁻¹' X)

theorem QuasiBorelSpace.measurable_of_isHom {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] {x✝³ : MeasurableSpace B} [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] {f : A → B} (hf : IsHom f) : Measurable f

@[simp]

theorem QuasiBorelSpace.isHom_iff_measurable {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] {x✝³ : MeasurableSpace B} [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] (f : A → B) : IsHom f ↔ Measurable f

@[simp]

theorem QuasiBorelSpace.toMeasurableSpace_ofMeasurableSpace {A : Type u_5} {hA : MeasurableSpace A} [StandardBorelSpace A] : toMeasurableSpace = hA

IsHom lemmas

theorem QuasiBorelSpace.isHom_def {A : Type u_5} {x✝ : QuasiBorelSpace A} {B : Type u_6} {x✝¹ : QuasiBorelSpace B} (f : A → B) : IsHom f ↔ ∀ ⦃φ : ℝ → A⦄, IsHom φ → IsHom fun (x : ℝ) => f (φ x)

@[instance_reducible]

instance QuasiBorelSpace.IsHom.instCoeFunForallForallReal {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → B} : CoeFun (IsHom f) fun (x : IsHom f) => ∀ ⦃φ : ℝ → A⦄, IsHom φ → IsHom fun (x : ℝ) => f (φ x)

Equations

• QuasiBorelSpace.IsHom.instCoeFunForallForallReal = { coe := ⋯ }

@[simp]

theorem QuasiBorelSpace.IsHom.id {A : Type u_1} {x✝ : QuasiBorelSpace A} : IsHom _root_.id

@[simp]

theorem QuasiBorelSpace.IsHom.fun_id {A : Type u_1} {x✝ : QuasiBorelSpace A} : IsHom fun (x : A) => x

Eta-expanded form of QuasiBorelSpace.IsHom.id

theorem QuasiBorelSpace.IsHom.comp {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} {f : B → C} (hf : IsHom f) {g : A → B} (hg : IsHom g) : IsHom (f ∘ g)

theorem QuasiBorelSpace.IsHom.fun_comp {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : QuasiBorelSpace C} {f : B → C} (hf : IsHom f) {g : A → B} (hg : IsHom g) : IsHom fun (x : A) => f (g x)

Eta-expanded form of QuasiBorelSpace.IsHom.comp

@[simp]

theorem QuasiBorelSpace.IsHom.const {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (x : B) : IsHom (Function.const A x)

@[simp]

theorem QuasiBorelSpace.IsHom.fun_const {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (x : B) : IsHom fun (x_1 : A) => x

Eta-expanded form of QuasiBorelSpace.IsHom.const

theorem QuasiBorelSpace.isHom_cases {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {I : Type u_5} [Countable I] {ix : A → I} {f : I → A → B} (hix : IsHom ix) (hf : ∀ (n : I), IsHom (f n)) : IsHom fun (x : A) => f (ix x) x

Subsingleton lemmas

@[simp]

theorem QuasiBorelSpace.isHom_to_subsingleton {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} [Subsingleton B] (f : A → B) : IsHom f

@[simp]

theorem QuasiBorelSpace.isHom_of_subsingleton {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} [Subsingleton A] (f : A → B) : IsHom f

lift lemmas

theorem QuasiBorelSpace.isHom_of_lift {B : Type u_2} {x✝ : QuasiBorelSpace B} {A : Type u_5} (f : A → B) : IsHom f

theorem QuasiBorelSpace.isHom_to_lift {B : Type u_2} {x✝ : QuasiBorelSpace B} {C : Type u_3} {x✝¹ : QuasiBorelSpace C} {A : Type u_5} (f : A → B) (g : C → A) : IsHom g ↔ IsHom fun (x : C) => f (g x)

ULift lemmas

@[simp]

theorem QuasiBorelSpace.ULift.isHom_def {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {φ : A → ULift.{u_5, u_2} B} : IsHom φ ↔ IsHom fun (x : A) => (φ x).down

theorem QuasiBorelSpace.ULift.isHom_up {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => { down := f x }

theorem QuasiBorelSpace.ULift.isHom_down {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → ULift.{u_5, u_2} B} (hf : IsHom f) : IsHom fun (x : A) => (f x).down

PLift lemmas

@[simp]

theorem QuasiBorelSpace.PLift.isHom_def {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {φ : A → PLift B} : IsHom φ ↔ IsHom fun (x : A) => (φ x).down

theorem QuasiBorelSpace.PLift.isHom_up {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => { down := f x }

theorem QuasiBorelSpace.PLift.isHom_down {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {f : A → PLift B} (hf : IsHom f) : IsHom fun (x : A) => (f x).down

DiscreteQuasiBorelSpaces

@[simp]

theorem QuasiBorelSpace.isHom_of_discrete_countable {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} [DiscreteQuasiBorelSpace A] [Countable A] (f : A → B) : IsHom f

Subtype Lemmas

@[simp]

theorem QuasiBorelSpace.Subtype.isHom_def {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {P : B → Prop} (f : A → Subtype P) : IsHom f ↔ IsHom fun (x : A) => ↑(f x)

theorem QuasiBorelSpace.Subtype.isHom_mk {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {P : B → Prop} {f : A → B} (hf₁ : IsHom f) (hf₂ : ∀ (x : A), P (f x)) : IsHom fun (x : A) => ⟨f x, ⋯⟩

theorem QuasiBorelSpace.Subtype.isHom_val {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {P : B → Prop} {f : A → Subtype P} (hf : IsHom f) : IsHom fun (x : A) => ↑(f x)

instance QuasiBorelSpace.Subtype.instMeasurableQuasiBorelSpaceSubtype {A : Type u_1} {x✝ : QuasiBorelSpace A} [MeasurableSpace A] [MeasurableQuasiBorelSpace A] {P : A → Prop} : MeasurableQuasiBorelSpace (Subtype P)

Prod Lemmas

@[simp]

theorem QuasiBorelSpace.Prod.isHom_fst {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Prod.fst

@[simp]

theorem QuasiBorelSpace.Prod.isHom_snd {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} : IsHom Prod.snd

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) : IsHom fun (x : A) => (f x, g x)

@[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) : IsHom f ↔ (IsHom fun (x : A) => (f x).1) ∧ IsHom fun (x : A) => (f x).2

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) : IsHom (Prod.map f g)

theorem QuasiBorelSpace.Pi.isHom_apply {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] (i : I) : IsHom fun (f : (i : I) → P i) => f i

theorem QuasiBorelSpace.Pi.isHom_pi {A : Type u_1} {x✝ : QuasiBorelSpace A} {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] {f : A → (i : I) → P i} (hf : ∀ (i : I), IsHom fun (x : A) => f x i) : IsHom f

@[simp]

theorem QuasiBorelSpace.Pi.isHom_iff {A : Type u_1} {x✝ : QuasiBorelSpace A} {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] {f : A → (i : I) → P i} : IsHom f ↔ ∀ (i : I), IsHom fun (x : A) => f x i

@[simp]

theorem QuasiBorelSpace.Pi.isHom_eval {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] (i : I) : IsHom (Function.eval i)

instance QuasiBorelSpace.Pi.instMeasurableQuasiBorelSpaceForall {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] : MeasurableQuasiBorelSpace ((i : I) → P i)

Prop Lemmas

theorem QuasiBorelSpace.Prop.isHom_ite {A : Type u_5} {x✝ : QuasiBorelSpace A} {B : Type u_6} {x✝¹ : QuasiBorelSpace B} {p : A → Prop} (hp : IsHom p) [inst : DecidablePred p] {f : A → B} (hf : IsHom f) {g : A → B} (hg : IsHom g) : IsHom fun (x : A) => if p x then f x else g x

theorem QuasiBorelSpace.Prop.isHom_not {A : Type u_5} {x✝ : QuasiBorelSpace A} {f : A → Prop} (hf : IsHom f) : IsHom fun (x : A) => ¬f x

theorem QuasiBorelSpace.Prop.isHom_and {A : Type u_5} {x✝ : QuasiBorelSpace A} {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ∧ g x

theorem QuasiBorelSpace.Prop.isHom_or {A : Type u_5} {x✝ : QuasiBorelSpace A} {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ∨ g x

theorem QuasiBorelSpace.Prop.isHom_imp {A : Type u_5} {x✝ : QuasiBorelSpace A} {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x → g x

theorem QuasiBorelSpace.Prop.isHom_iff {A : Type u_5} {x✝ : QuasiBorelSpace A} {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ↔ g x

theorem QuasiBorelSpace.Prop.isHom_forall {A : Type u_5} {x✝ : QuasiBorelSpace A} {I : Sort u_7} [Countable I] {f : I → A → Prop} (hf : ∀ (i : I), IsHom (f i)) : IsHom fun (x : A) => ∀ (i : I), f i x

theorem QuasiBorelSpace.Prop.isHom_exists {A : Type u_5} {x✝ : QuasiBorelSpace A} {I : Sort u_7} [Countable I] {f : I → A → Prop} (hf : ∀ (i : I), IsHom (f i)) : IsHom fun (x : A) => ∃ (i : I), f i x

theorem QuasiBorelSpace.Prop.isHom_decide {A : Type u_5} {x✝ : QuasiBorelSpace A} {p : A → Prop} [inst : DecidablePred p] (hp : IsHom p) : IsHom fun (x : A) => decide (p x)

theorem QuasiBorelSpace.Prop.isHom_dite {A : Type u_5} {x✝ : QuasiBorelSpace A} {B : Type u_6} {x✝¹ : QuasiBorelSpace B} {p : A → Prop} (hp : IsHom p) [inst : DecidablePred p] {f : (x : A) → p x → B} (hf : IsHom fun (x : Subtype p) => f ↑x ⋯) {g : (x : A) → ¬p x → B} (hg : IsHom fun (x : { x : A // ¬p x }) => g ↑x ⋯) : IsHom fun (x : A) => if h : p x then f x h else g x h

IsHomAdd/IsHomMul

instance QuasiBorelSpace.instIsHomMulOfIsHomMul₂ {A : Type u_1} [QuasiBorelSpace A] [Mul A] [IsHomMul₂ A] : IsHomMul A

instance QuasiBorelSpace.instIsHomAddOfIsHomMul₂ {A : Type u_1} [QuasiBorelSpace A] [Add A] [IsHomAdd₂ A] : IsHomAdd A

instance QuasiBorelSpace.instIsHomMulOfMeasurableQuasiBorelSpaceOfMeasurableMul₂ {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [Mul A] [MeasurableQuasiBorelSpace A] [MeasurableMul₂ A] : IsHomMul A

instance QuasiBorelSpace.instIsHomAddOfMeasurableQuasiBorelSpaceOfMeasurableMul₂ {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [Add A] [MeasurableQuasiBorelSpace A] [MeasurableAdd₂ A] : IsHomAdd A

instance QuasiBorelSpace.instIsHomMul₂OfMeasurableQuasiBorelSpaceOfMeasurableMul₂ {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [Mul A] [MeasurableQuasiBorelSpace A] [MeasurableMul₂ A] : IsHomMul₂ A

instance QuasiBorelSpace.instIsHomAdd₂OfMeasurableQuasiBorelSpace {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [Add A] [MeasurableQuasiBorelSpace A] [MeasurableAdd₂ A] : IsHomAdd₂ A

instance QuasiBorelSpace.instIsHomMulForall {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → Mul (P i)] [∀ (i : I), IsHomMul (P i)] : IsHomMul ((x : I) → P x)

instance QuasiBorelSpace.instIsHomAddForall {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → Add (P i)] [∀ (i : I), IsHomAdd (P i)] : IsHomAdd ((x : I) → P x)

instance QuasiBorelSpace.instIsHomMul₂Forall {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → Mul (P i)] [∀ (i : I), IsHomMul₂ (P i)] : IsHomMul₂ ((x : I) → P x)

instance QuasiBorelSpace.instIsHomAdd₂Forall {I : Type u_5} {P : I → Type u_6} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → Add (P i)] [∀ (i : I), IsHomAdd₂ (P i)] : IsHomAdd₂ ((x : I) → P x)

ℝ Lemmas

@[simp]

theorem QuasiBorelSpace.isHom_unpack {A : Type u_1} {x✝ : QuasiBorelSpace A} [Nonempty A] {x✝¹ : MeasurableSpace A} [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] : IsHom MeasureTheory.unpack

@[simp]

theorem QuasiBorelSpace.isHom_pack {A : Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : MeasurableSpace A} [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] : IsHom MeasureTheory.pack

@[simp]

theorem QuasiBorelSpace.isHom_split : IsHom MeasureTheory.split

theorem QuasiBorelSpace.isHom_lintegral {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace B} [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] {f : A → B → ENNReal} (hf : IsHom fun (x : A × B) => f x.1 x.2) (μ : MeasureTheory.Measure B) [MeasureTheory.SFinite μ] : IsHom fun (x : A) => MeasureTheory.lintegral μ (f x)