IterationLemmaProviderGeometry

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

Window geometry for the iteration-lemma provider: translates, the cap, the normalizers

The frozen iteration anchor states its window family with arbitrary real translates of the centred triadic cubes,

x + □_{j−2} ⊆ U_j ⊆ y + □_j        (for every j ≤ m),

which is the paper's own hypothesis: x and y are unconstrained points of ℝ^d, so x + □_{j−2} is in general not a triadic cube. The proved producers come in two flavours --- axisCube-based (arbitrary corner, arbitrary side) and TriadicCube-based --- and only the first applies here. This module proves the three adapters the provider needs:

• the translate bridge (axisCube_sandwich_of_translateSandwich): a translate of a centred origin cube is an axis cube, so the anchor's hypothesis yields an axisCube sandwich of aspect ratio 1/9 at every scale;
• the j ≤ m cap (cappedWindows): the proved engine and the proved producers quantify their interface over all k : ℤ, while the anchor supplies window data only for j ≤ m (the binding adjudication). The honest adapter is the capped family U_tilde_k = U_{min(k,m)}, which agrees with U on (−∞, m], is nested everywhere, and carries the sandwich at every k because the cap re-uses the scale-m cubes;
• the normalizer bridges at the axisCube sandwich: 3^{−j}-normalized oscillation versus the |W|^{−1/d}-normalized one, at the printed aspect ratio 3^{−2}, obtained from the proved arithmetic lemma rpow_normalizer_bounds.

Nothing here is an estimate: every statement is geometry or measure bookkeeping.

References

• ABK26, l.iteration.lemma statement (the window hypothesis).

The translate bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.openCubeSet_originCube_eq_axisCube (d : ℕ) (j : ℤ) : HCPolySupport.openCubeSet (HCPolySupport.originCube d j) = HCPolySupport.axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ j) (3 ^ j)

The centred origin cube □_j = (−3^j/2, 3^j/2)^d is the axis cube with corner −3^j/2 and side 3^j.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_axisCube {d : ℕ} (x z : HCPolySupport.Vec d) (L : ℝ) : (fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.axisCube z L = HCPolySupport.axisCube (x + z) L

Translating an axis cube translates its corner.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.axisCube_sandwich_of_translateSandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {x y : HCPolySupport.Vec d} {j : ℤ} (hin : (fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (j - 2)) ⊆ W) (hout : W ⊆ (fun (v : HCPolySupport.Vec d) => y + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j)) : ∃ (zin : HCPolySupport.Vec d) (zout : HCPolySupport.Vec d), HCPolySupport.axisCube zin (3 ^ (j - 2)) ⊆ W ∧ W ⊆ HCPolySupport.axisCube zout (3 ^ j)

The translate bridge. The anchor's window hypothesis at a scale j --- an arbitrary translate of □_{j−2} inside W, and W inside an arbitrary translate of □_j --- is an axisCube sandwich with sides 3^{j−2} and 3^j, i.e. of aspect ratio 1/9.

The j ≤ m cap

def Algsuperdiff.Section4.Provider.ExcessDecay.cappedWindows {d : ℕ} (U : ℤ → Set (HCPolySupport.Vec d)) (m k : ℤ) : Set (HCPolySupport.Vec d)

The capped window family U_tilde_k = U_{min(k,m)}: the honest adapter from the anchor's j ≤ m window data to the ∀ k : ℤ interface of the proved engine and the proved producers. Nothing is invented above m: the family is constant there.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.cappedWindows U m k = U (min k m)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cappedWindows_of_le {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {m k : ℤ} (hk : k ≤ m) : cappedWindows U m k = U k

theorem Algsuperdiff.Section4.Provider.ExcessDecay.subset_of_le_of_nest {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {m : ℤ} (hnest : ∀ j ≤ m, U (j - 1) ⊆ U j) {a b : ℤ} (hab : a ≤ b) (hbm : b ≤ m) : U a ⊆ U b

A family nested one scale at a time below m is monotone below m.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cappedWindows_nest {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {m : ℤ} (hnest : ∀ j ≤ m, U (j - 1) ⊆ U j) (k : ℤ) : cappedWindows U m k ⊆ cappedWindows U m (k + 1)

The capped family is nested at every scale.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cappedWindows_subset_top {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {m : ℤ} (hnest : ∀ j ≤ m, U (j - 1) ⊆ U j) (k : ℤ) : cappedWindows U m k ⊆ U m

Every capped window sits inside the top window.

Measure-theoretic slots at an axisCube sandwich

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_sub_affineEval_sq_of_axisCubeSandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} {zout : HCPolySupport.Vec d} {Lout : ℝ} (hLout : 0 < Lout) (hmeas : MeasurableSet W) (hout : W ⊆ HCPolySupport.axisCube zout Lout) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict W)) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (u x - Support.affineEval c g x) ^ 2) W MeasureTheory.volume

The square of every affine deviation of u is integrable on a window contained in an axis cube. This is the hint slot of affineExcess_quasiMonotone_of_nested.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volumeRatio_le_of_axisCubeSandwich {d : ℕ} {W : ℤ → Set (HCPolySupport.Vec d)} {zin zout : ℤ → HCPolySupport.Vec d} {s : ℤ → ℤ} (hs1 : ∀ (k : ℤ), s (k + 1) ≤ s k + 1) (hin : ∀ (k : ℤ), HCPolySupport.axisCube (zin k) (3 ^ (s k - 2)) ⊆ W k) (hout : ∀ (k : ℤ), W k ⊆ HCPolySupport.axisCube (zout k) (3 ^ s k)) (k : ℤ) : ((MeasureTheory.volume (W (k + 1))).toReal / (MeasureTheory.volume (W k)).toReal) ^ ((↑d)⁻¹ + 1 / 2) ≤ volumeRatioConstTriadic d

The volume ratio of an axisCube sandwich family with a slowly growing scale.

If W_k is sandwiched between axis cubes of sides 3^{s k − 2} and 3^{s k} and the scale function s increases by at most one per step, the one-step volume ratio is at most 3^{3d}, so the exponent 1/d + 1/2 of the excess normalizers gives the same constant volumeRatioConstTriadic d the triadic producer runs at. This is the hratio slot.

The normalizer bridges at an axisCube sandwich

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_bounds_of_axisCubeSandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {j : ℤ} (hin : HCPolySupport.axisCube zin (3 ^ (j - 2)) ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout (3 ^ j)) : (3 ^ (j - 2)) ^ d ≤ (MeasureTheory.volume W).toReal ∧ (MeasureTheory.volume W).toReal ≤ (3 ^ j) ^ d

The two volume bounds an axisCube sandwich of aspect ratio 1/9 gives, in the shape the proved normalizer arithmetic consumes.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oscillationScaled_le_oscillationOn_of_axisCubeSandwich {d : ℕ} (hd : d ≠ 0) {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {j : ℤ} (hin : HCPolySupport.axisCube zin (3 ^ (j - 2)) ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout (3 ^ j)) (u : HCPolySupport.Vec d → ℝ) : oscillationScaled j W u ≤ oscillationOn W u

The 3^{−j}-normalized oscillation is below the |W|^{−1/d}-normalized one, on a window sandwiched at aspect ratio 1/9.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oscillationOn_le_oscillationScaled_of_axisCubeSandwich {d : ℕ} (hd : d ≠ 0) {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {j : ℤ} (hin : HCPolySupport.axisCube zin (3 ^ (j - 2)) ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout (3 ^ j)) (u : HCPolySupport.Vec d → ℝ) : oscillationOn W u ≤ 9 * oscillationScaled j W u

The reverse normalizer comparison, at the printed aspect ratio 3^{−2}: the general normalizer costs at most the factor 9.