HarmonicReplaceMinkowski

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

The L^2 triangle inequality for normalized mean-square deviation

OscillationDecayMinkowski proves the two-term triangle inequality for the normalized L^2 deviation on a cube under continuity of the two fields, which is what a smooth Weyl representative supplies. The nested-recentring telescope, however, splits the fine-scale gradient into finitely many harmonic increments whose gradients are only L^2: continuity is unavailable, and the number of terms is the number of scales, not two.

This module supplies both generalizations. The quadratic core -- OscillationDecayMinkowski.sq_sum_setIntegral_mul_le, the Cauchy-Schwarz inequality for the coordinate-summed bilinear form -- is already stated with integrability hypotheses rather than continuity ones, so it is reused verbatim; only the integrability side conditions have to be re-derived from L^2 membership, and the finite-sum form is a routine induction on top of the two-term form.

Contents

• memScalarL2_coord_sub_const, memVectorL2_finsetSum -- the L^2 bookkeeping.
• meanSquareDeviationVecOn_zero -- the base case of the induction.
• sqrt_meanSquareDeviationVecOn_add_le_of_memVectorL2 -- the two-term triangle inequality on an arbitrary finite-measure set, for L^2 fields.
• sqrt_meanSquareDeviationVecOn_finsetSum_le_of_memVectorL2 -- the finite-sum triangle inequality.
• sqrt_meanSquareOscillationVecOn_finsetSum_le_of_memVectorL2 -- the form the telescope consumes as its hsplit hypothesis: the oscillation of a finite sum on the fine set is bounded by the sum of the deviations of the summands from arbitrary centres.

Portability

This file depends only on Mathlib, on CoarseGraining (Homogenization.*) and on the oscillation layer of this same directory. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector, no sigmaBar. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.memScalarL2_coord_sub_const {d : ℕ} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) (a : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.MemScalarL2 V fun (x : HCPolySupport.Vec d) => f x i - a i

A coordinate of a recentred L^2 vector field is a scalar L^2 function.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.memVectorL2_finsetSum {d : ℕ} {ι : Type u_1} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (s : Finset ι) {F : ι → HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ j ∈ s, HCPolySupport.MemVectorL2 V (F j)) : HCPolySupport.MemVectorL2 V fun (x : HCPolySupport.Vec d) => ∑ j ∈ s, F j x

A finite sum of L^2 vector fields is L^2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_zero {d : ℕ} (V : Set (HCPolySupport.Vec d)) : HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V (fun (x : HCPolySupport.Vec d) => 0) 0 = 0

The mean-square deviation of the zero field from zero vanishes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareDeviationVecOn_add_le_of_memVectorL2 {d : ℕ} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) (hg : HCPolySupport.MemVectorL2 V g) (a b : HCPolySupport.Vec d) : √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V (fun (x : HCPolySupport.Vec d) => f x + g x) (a + b)) ≤ √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V f a) + √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V g b)

The two-term triangle inequality for L^2 fields.

|| (f + g) - (a + b) ||_{L2bar (V)} <= || f - a ||_{L2bar (V)} + || g - b ||_{L2bar (V)} on any finite-measure set, with no continuity hypothesis: square integrability of the two fields is enough. The proof is the expansion of the normalized square together with Cauchy-Schwarz for the coordinate-summed bilinear form.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareDeviationVecOn_finsetSum_le_of_memVectorL2 {d : ℕ} {ι : Type u_1} {V : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (s : Finset ι) {F : ι → HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ j ∈ s, HCPolySupport.MemVectorL2 V (F j)) (a : ι → HCPolySupport.Vec d) : √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V (fun (x : HCPolySupport.Vec d) => ∑ j ∈ s, F j x) (∑ j ∈ s, a j)) ≤ ∑ j ∈ s, √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V (F j) (a j))

The finite-sum triangle inequality for L^2 fields.

The normalized L^2 deviation of a finite sum of L^2 fields from the sum of arbitrary centres is at most the sum of the individual deviations. This is the N-term form the nested-recentring telescope needs, N being the number of scales; the proved two-term form is its N = 2 case.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareOscillationVecOn_finsetSum_le_of_memVectorL2 {d : ℕ} {ι : Type u_1} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (s : Finset ι) {F : ι → HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ j ∈ s, HCPolySupport.MemVectorL2 V (F j)) (a : ι → HCPolySupport.Vec d) : √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V fun (x : HCPolySupport.Vec d) => ∑ j ∈ s, F j x) ≤ ∑ j ∈ s, √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V (F j) (a j))

The splitting inequality in oscillation form, for L^2 fields.

This is the shape consumed as hsplit by OscillationTelescope.le_zpow_mul_add_nsmul_of_nested_decomposition once the summands are the harmonic increments of the nested-recentring decomposition, whose gradients are only square integrable.