Mathlib.Measure­Theory.Function.Lp­Seminorm

LpSeminorm — Mathlib-shaped helpers: Measurable.

Measurable 2 core · 0 supporting This file proves that the parameter map sending a jointly measurable integrand to its finite nonzero Lp norm under a fixed measure is measurable. ★ measurable_eLpNorm_toReal_of_uncurry★ measurable_eLpNorm_toReal_of_uncurry_of_factor

Measurability of Parametric Lp Norms

This file proves that the parameter map sending a jointly measurable integrand to its finite nonzero Lp norm under a fixed measure is measurable. It supplies a Tonelli-based measurability tool for parameterized families of functions.

The top-σ-algebra lemma is measurable_eLpNorm_toReal_of_uncurry; the sub-σ-algebra version, where joint measurability factors through mΩ × MeasurableSpace X, is measurable_eLpNorm_toReal_of_uncurry_of_factor.

lemma measurable_eLpNorm_toReal_of_uncurry reviewed
Causalean.Mathlib.MeasureTheory.Function.LpSeminorm

Lp-norm measurable from joint measurability (top σ-algebra). For a σ-finite base measure P and an exponent p that is neither zero nor infinite, if the map (ω, x) ↦ g ω x is jointly measurable on the product of Ω and X, then the real-valued Lp norm ω ↦ ‖g ω‖_{Lp(P)} is measurable as a function of ω.

Formal statement
hypotheses
Ω :
Type u_1
shared
X :
Type u_2
shared
MeasurableSpace Ω
P :
Measure X
SFinite P
E :
Type*
MeasurableSpace E
TopologicalSpace E
ContinuousENorm E
OpensMeasurableSpace E
Ω → X → E
p :
ℝ≥0∞
hp_zero :
p ≠ 0
hp_top :
p ≠ ⊤
hg :
Measurable (uncurry g)
conclusion
Measurable (fun ω => (eLpNorm (g ω) p P).toReal)
Proof (Lean source)
@[fun_prop] lemma measurable_eLpNorm_toReal_of_uncurry [MeasurableSpace Ω] {P : Measure X} [SFinite P] {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E] [OpensMeasurableSpace E] {g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) (hg : Measurable (uncurry g)) : Measurable (fun ω => (eLpNorm (g ω) p P).toReal) := by have h_int : Measurable (fun ω => ∫⁻ x, ‖g ω x‖ₑ ^ p.toReal ∂P) := by exact Measurable.lintegral_prod_right' ((hg.enorm).pow_const p.toReal) have h_norm : Measurable (fun ω => eLpNorm (g ω) p P) := by simpa [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top] using (h_int.pow_const (1 / p.toReal)) exact ENNReal.measurable_toReal.comp h_norm
Causalean.Mathlib.MeasureTheory.Function.LpSeminorm.measurable_eLpNorm_toReal_of_uncurry · Causalean/Mathlib/MeasureTheory/Function/LpSeminorm/Measurable.lean:51
lemma measurable_eLpNorm_toReal_of_uncurry_of_factor reviewed
Causalean.Mathlib.MeasureTheory.Function.LpSeminorm

Lp-norm measurable with respect to a sub-σ-algebra. For a σ-finite base measure P and an exponent p that is neither zero nor infinite, if the map (ω, x) ↦ g ω x is jointly measurable with respect to the product of a sub-σ-algebra mΩ on Ω and the σ-algebra on X, then the real-valued Lp norm ω ↦ ‖g ω‖_{Lp(P)} is measurable with respect to mΩ.

Formal statement
hypotheses
Ω :
Type u_1
shared
X :
Type u_2
shared
mΩ :
MeasurableSpace Ω
P :
Measure X
SFinite P
E :
Type*
MeasurableSpace E
TopologicalSpace E
ContinuousENorm E
OpensMeasurableSpace E
Ω → X → E
p :
ℝ≥0∞
hp_zero :
p ≠ 0
hp_top :
p ≠ ⊤
hg_uncurry :
@Measurable (Ω × X) E (@instMeasurableSpace Ω X mΩ inferInstance) inferInstance (uncurry g)
conclusion
Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal)
Proof (Lean source)
@[fun_prop] lemma measurable_eLpNorm_toReal_of_uncurry_of_factor {mΩ : MeasurableSpace Ω} {P : Measure X} [SFinite P] {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E] [OpensMeasurableSpace E] {g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) (hg_uncurry : @Measurable (Ω × X) E (@instMeasurableSpace Ω X mΩ inferInstance) inferInstance (uncurry g)) : Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal) := by have h_int : Measurable[mΩ] (fun ω => ∫⁻ x, ‖g ω x‖ₑ ^ p.toReal ∂P) := by exact Measurable.lintegral_prod_right' ((hg_uncurry.enorm).pow_const p.toReal) have h_norm : Measurable[mΩ] (fun ω => eLpNorm (g ω) p P) := by simpa [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top] using (h_int.pow_const (1 / p.toReal)) exact ENNReal.measurable_toReal.comp h_norm
Causalean.Mathlib.MeasureTheory.Function.LpSeminorm.measurable_eLpNorm_toReal_of_uncurry_of_factor · Causalean/Mathlib/MeasureTheory/Function/LpSeminorm/Measurable.lean:79