OscillationNestedFamily

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

Scale bookkeeping for the nested-recentring telescope

The nested-recentring route of OscillationTelescope compares normalized mean-square quantities across the concentric cube family U_j = z + cu_{n+j}. Two conversions occur over and over in that comparison and are isolated here.

• The volume-ratio step. A harmonic replacement born at scale n+j is controlled only on its own cube, while the telescope needs its size on every finer cube. Restricting a normalized mean-square deviation from U_{j+i} to U_j costs exactly the volume ratio 3^{id}, hence the factor rho^i after taking square roots, where rho = sqrt (3^d). This single geometric constant is the rho of OscillationTelescope, and it is also what makes the small-gap branch of the assembly affordable.
• The recentring step. Passing from an oscillation (deviation from the cube average) to a deviation from an arbitrary centre is free in the right direction, and the L^2 hypotheses under which it is legal are exactly L^2 membership of the field on the cube.

The remaining two lemmas are the elementary sqrt/pow interchange used to write the volume-ratio factor as rho^i, and the invariance of the mean-square deviation from the origin under a sign change, which is how a difference of two replacements is split by the triangle inequality.

Contents

• instIsFiniteMeasureVolumeMeasureOnOpenCubeAtScale -- the finiteness instance for concentric cubes, so that the L^2 A applies without local haveIs.
• sqrt_pow_natCast -- sqrt (x^i) = (sqrt x)^i for 0 <= x.
• meanSquareDeviationVecOn_neg -- sign invariance of the deviation from 0.
• sqrt_meanSquareOscillationVecOn_le_sqrt_meanSquareDeviationVecOn_of_memVectorL2 -- the recentring step under L^2 membership.
• sqrt_meanSquareDeviationVecOn_le_pow_mul_of_le -- the volume-ratio step on the concentric family, with the factor rho^i.

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).

instance Algsuperdiff.Section3.Provider.Diffusivity.Corrector.instIsFiniteMeasureVolumeMeasureOnOpenCubeAtScale {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) : MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch03.openCubeAtScale z m))

A concentric cube has finite volume, so the L^2 A applies on it.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_pow_natCast {x : ℝ} (hx : 0 ≤ x) (i : ℕ) : √(x ^ i) = √x ^ i

sqrt (x ^ i) = (sqrt x) ^ i for a nonnegative base. Used to write the triadic volume ratio 3^{id} as the i-th power of the single constant rho = sqrt (3^d).

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

The mean-square deviation from the origin does not see a sign change. This is what lets the triangle inequality split the difference of two harmonic replacements into their two individual sizes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareOscillationVecOn_le_sqrt_meanSquareDeviationVecOn_of_memVectorL2 {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hfin : MeasureTheory.volume V ≠ ⊤) (hpos : 0 < (MeasureTheory.volume V).toReal) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) (c : HCPolySupport.Vec d) : √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn V f) ≤ √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn V f c)

Recentring under L^2 membership.

The normalized L^2 oscillation of a square-integrable field is at most its normalized L^2 deviation from any centre.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareDeviationVecOn_le_pow_mul_of_le {d : ℕ} (z : HCPolySupport.Vec d) {m m' : ℤ} {i : ℕ} (hi : m + ↑i = m') {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale z m') f) (c : HCPolySupport.Vec d) : √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m) f c) ≤ √(3 ^ d) ^ i * √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m') f c)

The volume-ratio step on the concentric family.

If the coarse cube z + cu_{m'} sits i triadic scales above the fine cube z + cu_m, then restricting the normalized L^2 deviation from the coarse cube to the fine one costs exactly rho^i, where rho = sqrt (3^d) is the square root of the one-step volume ratio.