StepNineOffGridGeometry

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

t.regularity off-grid transfer: the geometry

The gap

The whole §4.4 proof runs at a lattice centre z ∈ 3^n ℤ^d ∩ □_m and ends on the window (z + □_{n+1}) ∩ □_m, while t.regularity claims the estimate at an arbitrary x ∈ □_m on (x + □_n) ∩ □_m. The manuscript performs the transfer nowhere: it is asserted in a single sentence.

The construction: round toward the origin, not to the nearest lattice point

The admissible set of lattice centres is larger than the manuscript's implicit "nearest point". x + □_n ⊆ z + □_{n+1} asks only

  |x_i − z_i| ≤ (3^{n+1} − 3^n)/2 = 3^n ,

an interval of length 2·3^n around x_i, which contains BOTH 3^n⌊x_i/3^n⌋ and 3^n⌈x_i/3^n⌉. Choosing between them by the SIGN of x_i — i.e. rounding toward the origin — gives simultaneously

  |x_i − z_i| < 3^n        and        |z_i| ≤ |x_i| .

The second inequality is what the nearest-point route does not have, and it is exactly what needs: z inherits origin-cube membership of x. In particular x ∈ □_m ⟹ z ∈ □_m (the manuscript's own z ∈ 3^nℤ^d ∩ □_m) and x ∈ □_{m−1} ⟹ z ∈ □_{m−1} (the boundary indicator, see StepNineOffGridIndicator). No band enlargement is needed at any scale.

What is delivered

• offGridLatticeIndex, offGridCentre — the integer index and the lattice point 3^n·v, in Support.triadicLatticePoint's own carrier;
• abs_sub_offGridCentre_lt, abs_offGridCentre_le — the two scalar facts;
• offGridCentre_mem_openCubeSet — x ∈ □_k → z ∈ □_k scale k;
• offGridLatticeIndex_mem_latticeCubeSet — z is a member of the Step-3 lattice index set Support.latticeCubeSet d n m;
• truncatedWindow_subset_offGrid — (x + □_n) ∩ □_m ⊆ (z + □_{n+1}) ∩ □_m;
• exists_inner_cube_subset_truncatedWindow — the common inscribed cube from StepThreeWindows, used for the volume bound in StepNineOffGridTransfer.

References

• ABK26, t.regularity, (the claim at every x ∈ □_m) (the lattice-centre endpoint and the asserted transfer).

1. The scalar rounding toward the origin

noncomputable def Algsuperdiff.Section4.Provider.Regularity.truncIndex (a t : ℝ) : ℤ

The scale-a rounding of t toward the origin, as an integer.

Equations

• Algsuperdiff.Section4.Provider.Regularity.truncIndex a t = if 0 ≤ t then ⌊t / a⌋ else ⌈t / a⌉

2. The off-grid lattice centre

noncomputable def Algsuperdiff.Section4.Provider.Regularity.offGridLatticeIndex {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : Fin d → ℤ

The off-grid lattice index. The integer vector v with 3^n v the coordinatewise rounding of x toward the origin at spacing 3^n.

Equations

• Algsuperdiff.Section4.Provider.Regularity.offGridLatticeIndex n x i = Algsuperdiff.Section4.Provider.Regularity.truncIndex (3 ^ n) (x i)

noncomputable def Algsuperdiff.Section4.Provider.Regularity.offGridCentre {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

The off-grid lattice centre z ∈ 3^n ℤ^d, in the Step-3 carrier Support.triadicLatticePoint.

Equations

• Algsuperdiff.Section4.Provider.Regularity.offGridCentre n x = Algsuperdiff.Section4.Support.triadicLatticePoint n (Algsuperdiff.Section4.Provider.Regularity.offGridLatticeIndex n x)

theorem Algsuperdiff.Section4.Provider.Regularity.abs_sub_offGridCentre_lt {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) : |x i - offGridCentre n x i| < 3 ^ n

The displacement bound: |x_i − z_i| < 3^n, one full lattice spacing — the slack the nearest-point route throws away.

theorem Algsuperdiff.Section4.Provider.Regularity.abs_offGridCentre_le {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) : |offGridCentre n x i| ≤ |x i|

The origin-monotonicity: |z_i| ≤ |x_i|. This is the fact the manuscript's implicit nearest-point choice does not have, and the one that makes the boundary indicator transfer without a band enlargement.

theorem Algsuperdiff.Section4.Provider.Regularity.offGridCentre_mem_openCubeSet {d : ℕ} {k : ℤ} (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) : offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d k)

Every origin-cube membership of x passes to z, at every scale k and for every n.

theorem Algsuperdiff.Section4.Provider.Regularity.offGridLatticeIndex_mem_latticeCubeSet {d : ℕ} {m : ℤ} (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : offGridLatticeIndex n x ∈ Support.latticeCubeSet d n m

z is a Step-3 lattice centre: its index lies in Support.latticeCubeSet d n m, i.e. z ∈ 3^n ℤ^d ∩ □_m.

3. The window inclusion

theorem Algsuperdiff.Section4.Provider.Regularity.image_add_subset_offGridCentre {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : (fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (v : HCPolySupport.Vec d) => offGridCentre n x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1))

The cube inclusion x + □_n ⊆ z + □_{n+1}: the centred cube at an arbitrary point sits inside the ONE-S cube at its toward-origin lattice point.

theorem Algsuperdiff.Section4.Provider.Regularity.truncatedWindow_subset_offGrid {d : ℕ} (n m : ℤ) (x : HCPolySupport.Vec d) : ExcessDecay.truncatedWindow x m n ⊆ ExcessDecay.truncatedWindow (offGridCentre n x) m (n + 1)

The truncated-window inclusion (the shape t.regularity consumes):

  (x + □_n) ∩ □_m  ⊆  (z + □_{n+1}) ∩ □_m ,        z = offGridCentre n x .