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.
References #
- Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.
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) μ