Lp Norm Helper Lemmas

This file contains helper lemmas about Lp norms and their relationship to integrals, suitable for contribution to mathlib. All lemmas are self-contained with minimal dependencies.

Main Results

• eLpNorm_two_sq_eq_integral_sq: For real functions in L², eLpNorm² equals integral of square
• eLpNorm_lt_of_integral_sq_lt: If ∫ f² < r², then eLpNorm f 2 < r
• memLp_of_abs_le_const: Bounded functions are in Lp on finite measures

These lemmas bridge the gap between the ENNReal-valued eLpNorm and Real-valued integrals, which is essential for applying analysis results in probability theory.

Notes

These results are standard in probability theory but not currently in mathlib in this exact form. They eliminate boilerplate in proofs involving L² convergence.

L² Norm and Integral Relationship

theorem MeasureTheory.eLpNorm_two_sq_eq_integral_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → ℝ} (hf : MemLp f 2 μ) : (eLpNorm f 2 μ).toReal ^ 2 = ∫ (ω : Ω), f ω ^ 2 ∂μ

L² norm squared equals integral of square for real functions.

For a real-valued function f in L²(μ), the square of its L² norm equals the integral of f²:

(eLpNorm f 2 μ)² = ∫ f² dμ

This is a fundamental relationship used throughout probability theory, bridging the gap between ENNReal-valued Lp norms and Real-valued integrals.

Proof strategy: Use the definition of eLpNorm for p = 2, which involves lintegral of ‖f‖^2, and convert via toReal.

theorem MeasureTheory.eLpNorm_lt_of_integral_sq_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → ℝ} {r : ℝ} (hf : MemLp f 2 μ) (hr : 0 < r) (h : ∫ (ω : Ω), f ω ^ 2 ∂μ < r ^ 2) : eLpNorm f 2 μ < ENNReal.ofReal r

L² norm bound from integral bound.

If the integral of f² is less than r², then the L² norm of f is less than r. This is the standard way to convert integral bounds to Lp norm bounds.

Application: Used when we have ∫ f² < ε² and want eLpNorm f 2 < ε.

Membership in Lp Spaces

theorem MeasureTheory.memLp_of_abs_le_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) (hf_bdd : ∀ᵐ (ω : Ω) ∂μ, |f ω| ≤ M) (p : ENNReal) : 1 ≤ p → p ≠ ⊤ → MemLp f p μ

Functions bounded by a constant are in Lp.

If |f| ≤ M almost everywhere, then f ∈ Lp for any p ∈ [1, ∞) on a finite measure space.

This is a standard result used to show block averages of bounded functions are in L².

theorem MeasureTheory.memLp_two_of_bounded {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {f : Ω → ℝ} {M : ℝ} (hf_meas : Measurable f) (hf_bdd : ∀ (ω : Ω), |f ω| ≤ M) : MemLp f 2 μ

Block average of bounded function is in L².

Special case: If f is bounded by M, then f is in L² on a probability space. This is used repeatedly in Cesàro convergence proofs.