OscillationMeanSquare

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

Mean-square oscillation algebra for e.nablaw.oscillations

The quantity compared in e.nablaw.oscillations is the normalized mean-square gradient oscillation on a cube. CoarseGraining already defines its squared carrier,

  meanSquareDeviationOn V u c    = avg_V (u - c)^2 ,
  meanSquareDeviationVecOn V h c = sum_k meanSquareDeviationOn V (h . k) (c k) ,
  meanSquareOscillationVecOn V h = meanSquareDeviationVecOn V h (avg_V h) ,

in Homogenization.Book.Ch01 (MeanSquareDeviation.lean), but supplies no lemma at all about meanSquareOscillationVecOn: a repository sweep of CoarseGraining finds the definition and no consumer. The three facts proved here are the ones the nested-recentring route consumes at every scale.

• Nonnegativity, needed to feed any of the accumulation arithmetic.
• The weighted splitting inequality |a + b|^2 <= (1 + 1/k)|a|^2 + (1 + k)|b|^2. With k chosen as the number of telescope pieces this is what turns a finite sum of harmonic increments into a bound that grows linearly, not geometrically, in the number of scales -- the squared-form counterpart of the cancellation in OscillationTelescope. Using the crude k = 1 form instead would produce a factor 2^N and destroy the estimate.
• The volume-ratio comparison: restricting a mean-square deviation from a cube to a subcube costs exactly the volume ratio. For one triadic step that ratio is 3^d (see OscillationCubeFamily), and it is the factor rho of OscillationTelescope.sum_zpow_neg_mul_le_nsmul_of_triadic_bound.

References

• ABK26, e.nablaw.oscillations.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationOn_nonneg {d : ℕ} (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) (c : ℝ) : 0 ≤ HCPolySupport.Book.Ch01.meanSquareDeviationOn V u c

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_nonneg {d : ℕ} (V : Set (HCPolySupport.Vec d)) (h : HCPolySupport.Vec d → HCPolySupport.Vec d) (c : HCPolySupport.Vec d) : 0 ≤ HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V h c

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareOscillationVecOn_nonneg {d : ℕ} (V : Set (HCPolySupport.Vec d)) (h : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V h

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationOn_le_volume_ratio_mul {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hVU : V ⊆ U) (hvolV : 0 < (MeasureTheory.volume V).toReal) (hvolU : 0 < (MeasureTheory.volume U).toReal) {u : HCPolySupport.Vec d → ℝ} {c : ℝ} (hint : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => (u y - c) ^ 2) U MeasureTheory.volume) : HCPolySupport.Book.Ch01.meanSquareDeviationOn V u c ≤ (MeasureTheory.volume U).toReal / (MeasureTheory.volume V).toReal * HCPolySupport.Book.Ch01.meanSquareDeviationOn U u c

The scalar volume-ratio comparison.

Restricting a mean-square deviation from U to a measurable subset V costs exactly the volume ratio |U| / |V|. Note the hypothesis is integrability on the larger set only.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_le_volume_ratio_mul {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hVU : V ⊆ U) (hvolV : 0 < (MeasureTheory.volume V).toReal) (hvolU : 0 < (MeasureTheory.volume U).toReal) {h : HCPolySupport.Vec d → HCPolySupport.Vec d} {c : HCPolySupport.Vec d} (hint : ∀ (k : Fin d), MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => (h y k - c k) ^ 2) U MeasureTheory.volume) : HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V h c ≤ (MeasureTheory.volume U).toReal / (MeasureTheory.volume V).toReal * HCPolySupport.Book.Ch01.meanSquareDeviationVecOn U h c

The vector volume-ratio comparison.

The form actually consumed: passing the mean-square gradient deviation from the cube U to a subcube V costs the volume ratio. For one triadic step of the concentric family this ratio is 3^d, whose square root is the factor rho weighting the E (j+1) term in OscillationTelescope.