StepThreeWindows

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

t.regularity Step 3: the window family U_j := (z + □_j) ∩ □_m

The target

U_j := (z + □_j) ∩ □_m       for the (possibly truncated) cube at scale j ∈ ℤ.

The carrier is the development's existing truncatedWindow of ExcessDecay/BoundaryLaneWindows.lean — (x + □_k) ∩ □_m, a translation image of an origin cube intersected with the domain cube — read at the lattice centre x := z. It matches the Step-3 display literally, so no new carrier is introduced; stepThreeWindow is only the scale-indexed family the iteration lemma's binder U : ℤ → Set (Vec d) wants.

What is delivered

IterationWindowFamily U m is the three-fold hypothesis block of the proved anchor Algsuperdiff.Frozen.Section4.iteration_lemma transcribed verbatim: measurability at every j ≤ m, the nesting U (j-1) ⊆ U j, and the sandwich ∃ x y, x + □_{j-2} ⊆ U j ⊆ y + □_j. iterationWindowFamily_stepThreeWindow discharges it for the Step-3 family from the single fact z ∈ □_m (the lattice centre lies in the domain cube) and nothing else — the sandwich holds at every j ≤ m, including the truncated ones.

The sandwich, and why the lattice plays no role

The common construction first produces an inner cube at scale j-1; the iteration interface obtains scale j-2 by cube inclusion.

Coordinatewise U_j is the interval (max(z_i - h, -H), min(z_i + h, H)) with h = 3^j/2, H = 3^m/2. Its length is at least h in all four truncation cases (width_le): 2h when the cube is interior, H - z_i + h > h and z_i + H + h > h at a single face — because |z_i| < H — and 2H ≥ h when the cube overflows both faces, which forces j = m. Since 3^{j-1} = 3^j/3 ≤ h, the centre of the truncated interval is a legal inner centre x, and the outer centre is y := z outright. No lattice-gap estimate on z is used, so the family is admissible for every centre in □_m, not only the triadic ones, although the Step-3 text only ever needs the triadic centres.

References

• ABK26, t.regularity Step 3, (the window family).
• ABK26, l.iteration.lemma, (the sandwich hypothesis).

1. The family

def Algsuperdiff.Section4.Provider.Regularity.stepThreeWindow {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) : ℤ → Set (HCPolySupport.Vec d)

The Step-3 window family U_j := (z + □_j) ∩ □_m, as the scale-indexed family the iteration lemma's U-binder consumes.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepThreeWindow z m j = Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow z m j

theorem Algsuperdiff.Section4.Provider.Regularity.measurableSet_stepThreeWindow {d : ℕ} (z : HCPolySupport.Vec d) (m j : ℤ) : MeasurableSet (stepThreeWindow z m j)

Each window is measurable (it is open).

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeWindow_sub_one_subset {d : ℕ} (z : HCPolySupport.Vec d) (m j : ℤ) : stepThreeWindow z m (j - 1) ⊆ stepThreeWindow z m j

The family is nested: U_{j-1} ⊆ U_j.

2. The sandwich

theorem Algsuperdiff.Section4.Provider.Regularity.exists_inner_cube_subset_truncatedWindow {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) : ∃ (y : HCPolySupport.Vec d), (fun (v : HCPolySupport.Vec d) => y + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (k - 1)) ⊆ ExcessDecay.truncatedWindow x m k

Every truncated window with its centre in the domain cube contains a translated origin cube one scale down. The coordinatewise midpoint gives the common construction.

theorem Algsuperdiff.Section4.Provider.Regularity.exists_inner_cube_subset_stepThreeWindow {d : ℕ} (z : HCPolySupport.Vec d) {m j : ℤ} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hjm : j ≤ m) : ∃ (x : HCPolySupport.Vec d), (fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (j - 2)) ⊆ stepThreeWindow z m j

The inner half of the window sandwich (the iteration lemma's hypothesis): for every j ≤ m there is a centre x with x + □_{j-2} ⊆ (z + □_j) ∩ □_m. The witness is the centre of the truncated window, coordinate by coordinate.

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeWindow_subset_outer_cube {d : ℕ} (z : HCPolySupport.Vec d) (m j : ℤ) : stepThreeWindow z m j ⊆ (fun (v : HCPolySupport.Vec d) => z + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j)

The outer half of the window sandwich: U_j ⊆ z + □_j outright.

3. The iteration lemma's window binder block

def Algsuperdiff.Section4.Provider.Regularity.IterationWindowFamily {d : ℕ} (U : ℤ → Set (HCPolySupport.Vec d)) (m : ℤ) : Prop

Measurable nested windows with inner and outer translated cube bounds.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Regularity.iterationWindowFamily_stepThreeWindow {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : IterationWindowFamily (stepThreeWindow z m) m

The Step-3 windows are an admissible iteration family. The only input is z ∈ □_m, which is half of the Step-3 hypothesis z ∈ 3^n ℤ^d ∩ □_m.