StepSevenSandwich

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

t.regularity Step 7a: the sandwich centres z', z''

The target

  We may find a pair z', z'' ∈ □_m such that, for each (y', k') ∈ {(z',m'), (z'',n')},
      (z + □_{k'-1}) ∩ □_m  ⊆  y' + □_{k'-1}  ⊆  (z + □_{k'}) ∩ □_m .

The construction

Write a := ½·3^{k'-1} (the half-side of the inner cube) and A := ½·3^m (the half-side of □_m). The centre is the coordinatewise of z into the inset box [-A+a, A-a]^d:

  y'_i := max( -A + a , min( z_i , A - a ) ) .

Three elementary facts do everything, and each is a two-line max/min manipulation (clamp_mem, clamp_capture, clamp_dist below):

• -A + a ≤ y'_i ≤ A - a, so y' + □_{k'-1} ⊆ □_m — this is the inclusion the identity choice y' := z at a boundary centre;
• min(z_i, A-a) ≤ y'_i ≤ max(-A+a, z_i), which captures every point of (z + □_{k'-1}) ∩ □_m (a point of the window is within a of z_i AND within A of the origin, so it is within a of the clamp);
• |y'_i - z_i| ≤ 2a, so y' + □_{k'-1} ⊆ z + □_{k'} (the outer cube has half side 3a).

Only a ≤ A (i.e. k' - 1 ≤ m) and z ∈ □_m are used; no lattice structure of z is needed, matching(c).

What is delivered

• exists_sandwich_centre — the sandwich at a general inner index k: (z + □_k) ∩ □_m ⊆ y + □_k ⊆ (z + □_{k+1}) ∩ □_m with y ∈ □_m.
• exists_stepSevenSandwich — the same in the printed indexing (k'-1, k').

References

• ABK26, t.regularity Step 7, (the sandwich).

1. The scalar clamp

2. The sandwich

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

  (z + □_k) ∩ □_m  ⊆  y + □_k  ⊆  (z + □_{k+1}) ∩ □_m .

The witness is the coordinatewise clamp of z into the inset box; see the module docstring.

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

The Step-7a sandwich in the printed indexing: at the selected scale k',

  (z + □_{k'-1}) ∩ □_m  ⊆  y' + □_{k'-1}  ⊆  (z + □_{k'}) ∩ □_m ,     y' ∈ □_m .