Extended $L^2$ Norm Comparison From Squared Integrals

This auxiliary lemma converts a comparison of squared integrals into an extended $L^2$ seminorm comparison.

Let $\alpha$ be a measurable space, $\mu$ any measure on it, and $u,v:\alpha\to\mathbb R$. Assume $u,v\in L^2(\mu)$ (MemLp) and

Then, writing $\|\cdot\|_{2,\mu}^{\mathrm{ext}}$ for eLpNorm at exponent $2$,

This provides a bridge from real integral estimates to norm estimates. The conclusion is an inequality in $[0,\infty]$ (ENNReal), not an inequality between toReal coercions, and no finiteness assumption on $\mu$ is required.

Original Lean declaration header

Within namespace FunctionalInequalities.L2. Shown in its original module context. Proof omitted.

theorem eLpNorm_le_eLpNorm_of_integral_sq_le {α : Type*} [MeasurableSpace α] {μ : Measure α}
    {u v : α → ℝ} (hu : MemLp u 2 μ) (hv : MemLp v 2 μ)
    (h : ∫ x, u x ^ 2 ∂μ ≤ ∫ x, v x ^ 2 ∂μ) :
    eLpNorm u 2 μ ≤ eLpNorm v 2 μ

Module navigation

Module: L2/AffineDecomposition.

Next: integral_affineOrthPart.

Source excerpt, lines 115–118 · Frozen source 408915f.