Exact conversion between scalar quadratic energy and the L2 norm.

theorem AVenhance.Infra.Section4.amnr_scalar_eLpNorm_two_eq_sqrt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfsq : MeasureTheory.Integrable (fun (z : α) => f z ^ 2) μ) : MeasureTheory.eLpNorm f 2 μ = ENNReal.ofReal √(∫ (z : α), f z ^ 2 ∂μ)

theorem AVenhance.Infra.Section4.amnr_scalar_eLpNorm_two_le_of_square {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfsq : MeasureTheory.Integrable (fun (z : α) => f z ^ 2) μ) {B : ℝ} (hB : 0 ≤ B) (hbound : ∫ (z : α), f z ^ 2 ∂μ ≤ B ^ 2) : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal B

A nonnegative quadratic energy bound gives the corresponding scalar L2 bound without weakening it to a pointwise estimate.

theorem AVenhance.Infra.Section4.amnr_scalar_square_le_of_eLpNorm_two {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {B : ℝ} (hB : 0 ≤ B) (hbound : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal B) : ∫ (z : α), f z ^ 2 ∂μ ≤ B ^ 2

Conversely, finite scalar L2 control bounds the actual quadratic integral.