Strongly measurable and finitely strongly measurable functions

This file contains some further development of strongly measurable and finitely strongly measurable functions, started in Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean.

References

• [Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.][Hytonen_VanNeerven_Veraar_Wies_2016]

theorem aestronglyMeasurable_dirac {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] [MeasurableSingletonClass α] {a : α} {f : α → β} : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.dirac a)

theorem MeasureTheory.AEStronglyMeasurable.comp_measurePreserving {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_4} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace α} {f : γ → α} {μ : Measure γ} {ν : Measure α} (hg : AEStronglyMeasurable g ν) (hf : MeasurePreserving f μ ν) : AEStronglyMeasurable (g ∘ f) μ

theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff {α : Type u_1} {γ : Type u_3} [TopologicalSpace γ] {β : Type u_4} {f : α → β} {mα : MeasurableSpace α} {μa : Measure α} {mβ : MeasurableSpace β} {μb : Measure β} (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) {g : β → γ} : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

theorem aestronglyMeasurable_smul_const_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → 𝕜} {c : E} (hc : c ≠ 0) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x • c) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem StronglyMeasurable.apply_continuousLinearMap {α : Type u_1} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {_m : MeasurableSpace α} {φ : α → F →L[𝕜] E} (hφ : MeasureTheory.StronglyMeasurable φ) (v : F) : MeasureTheory.StronglyMeasurable fun (a : α) => (φ a) v

theorem MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E} (hφ : AEStronglyMeasurable φ μ) (v : F) : AEStronglyMeasurable (fun (a : α) => (φ a) v) μ

theorem ContinuousLinearMap.aestronglyMeasurable_comp₂ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => (L (f x)) (g x)) μ

theorem aestronglyMeasurable_withDensity_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : Measurable f) {g : α → E} : MeasureTheory.AEStronglyMeasurable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ MeasureTheory.AEStronglyMeasurable (fun (x : α) => ↑(f x) • g x) μ