NormalizedL2

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The volume-normalized L²(W) seminorm and its eLpNorm dictionary

ABK26, §4.3. The excess of e.excess.def is built on the volume-normalized norm ‖·‖_{L²(W)}, which the manuscript writes as an average:

‖f‖_{L²(W)} = (⨍_W f²)^{1/2} .

This module proves that object (normalizedL2On) over CoarseGraining's volumeAverage, and the two-way dictionary to the ℝ≥0∞-valued MeasureTheory.eLpNorm in which the Section-4 frozen surface is written:

• normalizedL2On_eq_toReal_eLpNorm_div --- ‖f‖_{L²(W)} = ‖f‖_{L²(volume|_W)} / |W|^{1/2}, with no hypothesis on W (at volume W ∈ {0, ∞} both sides are 0);
• normalizedL2On_eq_toReal_eLpNorm_normalizedVolumeMeasureOn --- the same object read as an honest eLpNorm against Support.normalizedVolumeMeasureOn W, i.e. the exact carrier of the frozen harmonic anchor's left-hand side.

Everything else here is the seminorm calculus the excess layer consumes. Minkowski (normalizedL2On_add_le) is obtained through the dictionary from mathlib's eLpNorm_add_le rather than by a hand-rolled Cauchy--Schwarz on volumeAverage: that is the single reason the dictionary is proved first.

Why the ℝ-valued object at all

The iteration lemma and the discrete Grönwall lemma are inequalities between real numbers, with subtractions and an exponential; the Section-3 harmonic/oscillation layer is real-valued as well. The frozen Section-4 surface is ℝ≥0∞-valued. Both languages are therefore needed, and this module is the seam. The MemLp side conditions are the honest "f ∈ L²(W)" hypotheses; they are not needed for well-definedness (the sqrt of a possibly-0 average is total) but they are needed for the arithmetic, exactly as in the source.

Scope

Like Section4/Support/Dirichlet.lean, this module serves frozen statements and is importable anywhere in the Section-4 tree.

References

• ABK26, e.excess.def.
• Algsuperdiff/Section4/Support/Dirichlet.lean (normalizedVolumeMeasureOn).

The object

noncomputable def Algsuperdiff.Section4.Support.normalizedL2On {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : ℝ

The volume-normalized L²(W) seminorm ‖f‖_{L²(W)} = (⨍_W f²)^{1/2} of ABK26.

Equations

• Algsuperdiff.Section4.Support.normalizedL2On W f = √(HCPolySupport.volumeAverage W fun (x : HCPolySupport.Vec d) => f x ^ 2)

theorem Algsuperdiff.Section4.Support.normalizedL2On_nonneg {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : 0 ≤ normalizedL2On W f

theorem Algsuperdiff.Section4.Support.volumeAverage_sq_nonneg {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : 0 ≤ HCPolySupport.volumeAverage W fun (x : HCPolySupport.Vec d) => f x ^ 2

The volume average of a square is nonnegative. No measurability of W is needed: the integrand is globally nonnegative.

theorem Algsuperdiff.Section4.Support.normalizedL2On_sq {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : normalizedL2On W f ^ 2 = HCPolySupport.volumeAverage W fun (x : HCPolySupport.Vec d) => f x ^ 2

‖f‖²_{L²(W)} = ⨍_W f².

theorem Algsuperdiff.Section4.Support.normalizedL2On_le_of_sq_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {M : ℝ} (hM : 0 ≤ M) (h : (HCPolySupport.volumeAverage W fun (x : HCPolySupport.Vec d) => f x ^ 2) ≤ M ^ 2) : normalizedL2On W f ≤ M

A bound on the average of the square is a bound on the seminorm.

The eLpNorm dictionary

theorem Algsuperdiff.Section4.Support.normalizedL2On_eq_toReal_eLpNorm_div {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) : normalizedL2On W f = (MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict W)).toReal / √(MeasureTheory.volume W).toReal

The dictionary. The volume-normalized L²(W) seminorm is the unnormalized L²(volume|_W) norm divided by |W|^{1/2}.

No measurability of W and no positivity of |W| is required: when volume W is 0 or ∞ the real number (volume W).toReal is 0 and both sides degenerate to 0.

theorem Algsuperdiff.Section4.Support.toReal_eLpNorm_eq_sqrt_volume_mul_normalizedL2On {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hWpos : 0 < (MeasureTheory.volume W).toReal) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) : (MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict W)).toReal = √(MeasureTheory.volume W).toReal * normalizedL2On W f

The reciprocal form of the dictionary.

theorem Algsuperdiff.Section4.Support.normalizedL2On_eq_toReal_eLpNorm_normalizedVolumeMeasureOn {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hWpos : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) : normalizedL2On W f = (MeasureTheory.eLpNorm f 2 (normalizedVolumeMeasureOn W)).toReal

The ℝ≥0∞ reading of the same object. On a window of positive finite volume, ‖f‖_{L²(W)} is exactly the toReal of the eLpNorm of f against the normalized volume measure Support.normalizedVolumeMeasureOn W --- the carrier in which the frozen Section-4 surface is written.

The seminorm calculus

theorem Algsuperdiff.Section4.Support.normalizedL2On_add_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)) : (normalizedL2On W fun (x : HCPolySupport.Vec d) => f x + g x) ≤ normalizedL2On W f + normalizedL2On W g

Minkowski for ‖·‖_{L²(W)}, obtained through the dictionary from mathlib's eLpNorm_add_le.

theorem Algsuperdiff.Section4.Support.normalizedL2On_const_mul {d : ℕ} (W : Set (HCPolySupport.Vec d)) (t : ℝ) (f : HCPolySupport.Vec d → ℝ) : (normalizedL2On W fun (x : HCPolySupport.Vec d) => t * f x) = |t| * normalizedL2On W f

Absolute homogeneity. No hypotheses: the scalar pull-out of volumeAverage is unconditional.

theorem Algsuperdiff.Section4.Support.normalizedL2On_neg {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : (normalizedL2On W fun (x : HCPolySupport.Vec d) => -f x) = normalizedL2On W f

theorem Algsuperdiff.Section4.Support.normalizedL2On_sub_comm {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f g : HCPolySupport.Vec d → ℝ) : (normalizedL2On W fun (x : HCPolySupport.Vec d) => f x - g x) = normalizedL2On W fun (x : HCPolySupport.Vec d) => g x - f x

The volume-ratio comparison on nested windows

theorem Algsuperdiff.Section4.Support.volumeAverage_le_of_subset {d : ℕ} {W W' : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hsub : W' ⊆ W) (hW : 0 < (MeasureTheory.volume W).toReal) (hW' : 0 < (MeasureTheory.volume W').toReal) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hint : MeasureTheory.IntegrableOn f W MeasureTheory.volume) : HCPolySupport.volumeAverage W' f ≤ (MeasureTheory.volume W).toReal / (MeasureTheory.volume W').toReal * HCPolySupport.volumeAverage W f

Passing to a subwindow multiplies the average of a nonnegative function by at most the volume ratio.

theorem Algsuperdiff.Section4.Support.normalizedL2On_le_of_subset {d : ℕ} {W W' : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hsub : W' ⊆ W) (hW : 0 < (MeasureTheory.volume W).toReal) (hW' : 0 < (MeasureTheory.volume W').toReal) (hint : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x ^ 2) W MeasureTheory.volume) : normalizedL2On W' f ≤ √((MeasureTheory.volume W).toReal / (MeasureTheory.volume W').toReal) * normalizedL2On W f

Volume-ratio comparison of the normalized seminorms on nested windows. For W' ⊆ W, ‖f‖_{L²(W')} ≤ (|W|/|W'|)^{1/2} ‖f‖_{L²(W)}. This is the geometric engine of excess quasi-monotonicity.