OneStepWindows

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

The one-step window family U_j = (x+□_{n-j}) ∩ □_m and its geometry

l.excess.decay.good.scales runs on the truncated family

  U_j := (x + □_{n-j}) ∩ □_m ,     j ∈ ℕ₀ ,

which is BoundaryLaneWindows.truncatedWindow x m (n-j). This module proves the geometry every later leg of the one-step contraction reads off:

• exists_axisCube_sandwich_truncatedWindow — the aspect-1/9 sandwich axisCube zin 3^{k-2} ⊆ (x+□_k) ∩ □_m ⊆ axisCube zout 3^k, obtained from the proved inscribed cube (image_add_wellPlacedCentre_subset_truncatedWindow, which sits at scale k-1) and the proved outer inclusion. This is the slot every …_of_axisCubeSandwich producer of the excess layer consumes, and it is what makes the |W|^{-1/d} normalizer comparable to 3^{-k} on a truncated window.
• the volume bounds, the normalizer bounds, positivity, measurability, the MemLp/IntegrableOn slots, and the explicit volume ratio of two nested windows of the family;
• affineExcess_truncatedWindow_le — excess quasi-monotonicity on the family, at the explicit ratio constant;
• image_add_wellPlacedCentre_subset_windowChoice — the window choice at the clamped centre.

The window choice

The source asserts the existence of y ∈ □_m with both y+□_{n-2} ⊆ (z+□_n) ∩ □_m and (x+□_{n-2}) ∩ □_m ⊆ y+□_{n-2} and exhibits no construction; and the harmonic lemma instantiated at index n-2 in fact demands the stronger inclusion y+□_{n-2} ⊆ (z+□_{n-1}) ∩ □_m, which the printed window choice does not supply.

Both are supplied here at the explicit witness

  y := wellPlacedCentre x m (n-2)          (the coordinatewise clamp of x)

image_add_wellPlacedCentre_subset_windowChoice proves the stronger inclusion y + □_{n-2} ⊆ (z+□_{n-1}) ∩ □_m from x ∈ (z+□_{n-3}) ∩ □_m and n-2 ≤ m alone, and the second requirement is the proved truncatedWindow_subset_image_add_wellPlacedCentre at j = k = n-2. The half-width budget is 3^{n-2}/2 + 3^{n-2}/2 + 3^{n-3}/2 = 3.5·3^{n-3} against the target 3^{n-1}/2 = 4.5·3^{n-3}: slack 3^{n-3}, so the witness is not borderline. Note the clamp y is a full cube centre — the boundary-regime obstruction described in BoundaryLaneWindows concerns the window (x+□_k) ∩ □_m itself, not the enclosing full cube, and the two are compatible.

1. Measurability and the sandwich

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableSet_truncatedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasurableSet (truncatedWindow x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_axisCube_sandwich_truncatedWindow {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) : ∃ (zin : HCPolySupport.Vec d) (zout : HCPolySupport.Vec d), HCPolySupport.axisCube zin (3 ^ (k - 2)) ⊆ truncatedWindow x m k ∧ truncatedWindow x m k ⊆ HCPolySupport.axisCube zout (3 ^ k)

The aspect-1/9 sandwich of a truncated window.

The proved inscribed cube sits at scale k-1; shrinking it to k-2 and reading both inclusions in axisCube shape gives exactly the sandwich slot the excess layer's …_of_axisCubeSandwich producers consume.

2. Volumes, normalizers and the analytic slots

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_truncatedWindow_bounds {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) : (3 ^ (k - 2)) ^ d ≤ (MeasureTheory.volume (truncatedWindow x m k)).toReal ∧ (MeasureTheory.volume (truncatedWindow x m k)).toReal ≤ (3 ^ k) ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_truncatedWindow_pos {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) : 0 < (MeasureTheory.volume (truncatedWindow x m k)).toReal

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_volume_truncatedWindow_bounds {d : ℕ} (hd : d ≠ 0) {m k : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) : 3 ^ (-k) ≤ (MeasureTheory.volume (truncatedWindow x m k)).toReal ^ (-(↑d)⁻¹) ∧ (MeasureTheory.volume (truncatedWindow x m k)).toReal ^ (-(↑d)⁻¹) ≤ 9 * 3 ^ (-k)

The two-sided comparison of the |W|^{-1/d} normalizer with the cube normalizer 3^{-k} on a truncated window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_sub_affineEval_sq_truncatedWindow {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => (u p - Support.affineEval c g p) ^ 2) (truncatedWindow x m k) MeasureTheory.volume

3. The volume ratio of two nested windows of the family

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.windowRatioConst (d : ℕ) (j : ℤ) : ℝ

The explicit ratio constant of the family: |U_l| / |U_k| ≤ 3^{(l-k+2)d} for k ≤ l, raised to the excess exponent 1/d + 1/2.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.windowRatioConst d j = ((3 ^ (j + 2)) ^ d) ^ ((↑d)⁻¹ + 1 / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowRatioConst_nonneg (d : ℕ) (j : ℤ) : 0 ≤ windowRatioConst d j

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_ratio_truncatedWindow_le {d : ℕ} {m k l : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hlm : l - 1 ≤ m) : (MeasureTheory.volume (truncatedWindow x m l)).toReal / (MeasureTheory.volume (truncatedWindow x m k)).toReal ≤ (3 ^ (l - k + 2)) ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcess_truncatedWindow_le {d : ℕ} {m k l : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hlm : l - 1 ≤ m) (hkl : k ≤ l) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m l))) : Support.affineExcess (truncatedWindow x m k) u ≤ windowRatioConst d (l - k) * Support.affineExcess (truncatedWindow x m l) u

Excess quasi-monotonicity on the one-step family, at the explicit ratio constant. This is the E(u,U_2) ≲ E(u,U_0) move of the triangle assembly.

4. The window choice at the clamped centre

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_subset_windowChoice {d : ℕ} {m n : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ truncatedWindow z m (n - 3)) (hnm : n - 2 ≤ m) : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ truncatedWindow z m (n - 1)

The window choice at the clamped centre.

With y := wellPlacedCentre x m (n-2) the full cube y + □_{n-2} lies inside (z + □_{n-1}) ∩ □_m — one triadic scale sharper than the printed requirement ⊆ (z + □_n) ∩ □_m, and exactly the inclusion the harmonic-approximation anchor demands at its index n-2.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_subset_image_add_windowChoice {d : ℕ} {m n : ℤ} (x : HCPolySupport.Vec d) (hnm : n - 2 ≤ m) : truncatedWindow x m (n - 2) ⊆ (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))

The second requirement of the printed window choice, at the same witness: the truncated window sits inside the full clamped cube.