OscillationDecayMinkowski

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

The triangle inequality for the normalized L^2 deviation on a cube

The nested-recentring assembly of OscillationTelescope opens with a splitting step: the fine-scale gradient is written as a finite sum of harmonic increments plus an approximation defect, and the normalized L^2 oscillation of the sum is bounded by the sum of the normalized L^2 deviations of the summands. That is the hypothesis hsplit of le_zpow_mul_add_nsmul_of_nested_decomposition, and it is the Minkowski inequality for the seminorm

  N (h, c) = || h - c ||_{L2bar (V)} = sqrt (sum_i avg_V (h_i - c_i)^2) .

CoarseGraining supplies no lemma about meanSquareDeviationVecOn at all, so the inequality is proved from scratch, and elementarily: the cross term is controlled by the Cauchy--Schwarz inequality, which is obtained from the nonnegativity of the quadratic t -> sum_i int_V (t (f_i - a_i) - (g_i - b_i))^2 through Mathlib's discrim_le_zero. No L^p duality, no MemLp bookkeeping and no transfer to EuclideanSpace is used.

This module carries the two ingredients of that argument, at an arbitrary set V and with the integrability of the three moments as explicit binders. The triangle inequality itself is assembled from them in HarmonicReplaceMinkowski.sqrt_meanSquareDeviationVecOn_add_le_of_memVectorL2 and, in the oscillation form hsplit consumes, in Closure.GammaTenInteriorMinkowski.sqrt_meanSquareOscillationVecOn_add_le_of_memVectorL2; there the binders are square integrability of the two fields, with no continuity hypothesis.

Contents

• setIntegral_sub_sq_expand -- the expansion of int_V (t p - q)^2.
• sq_sum_setIntegral_mul_le -- Cauchy--Schwarz for the coordinate-summed bilinear form.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.setIntegral_sub_sq_expand {d : ℕ} {V : Set (HCPolySupport.Vec d)} {p q : HCPolySupport.Vec d → ℝ} (hp2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => p x ^ 2) V MeasureTheory.volume) (hq2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => q x ^ 2) V MeasureTheory.volume) (hpq : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => p x * q x) V MeasureTheory.volume) (t : ℝ) : ∫ (x : HCPolySupport.Vec d) in V, (t * p x - q x) ^ 2 = (∫ (x : HCPolySupport.Vec d) in V, p x ^ 2) * (t * t) + -(2 * ∫ (x : HCPolySupport.Vec d) in V, p x * q x) * t + ∫ (x : HCPolySupport.Vec d) in V, q x ^ 2

Expansion of the quadratic int_V (t p - q)^2 in the three moments.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sq_sum_setIntegral_mul_le {d : ℕ} {V : Set (HCPolySupport.Vec d)} {p q : Fin d → HCPolySupport.Vec d → ℝ} (hp2 : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => p i x ^ 2) V MeasureTheory.volume) (hq2 : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => q i x ^ 2) V MeasureTheory.volume) (hpq : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => p i x * q i x) V MeasureTheory.volume) : (∑ i : Fin d, ∫ (x : HCPolySupport.Vec d) in V, p i x * q i x) ^ 2 ≤ (∑ i : Fin d, ∫ (x : HCPolySupport.Vec d) in V, p i x ^ 2) * ∑ i : Fin d, ∫ (x : HCPolySupport.Vec d) in V, q i x ^ 2

Cauchy--Schwarz for the coordinate-summed bilinear form.