BoundaryWindowPoincare

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

The translated open cube as an axis cube

The boundary branch of the general clause works on the anchor's own window W' = (z + □_{n+3}) ∩ □_m, under the gate

  (z + □_{n+2}) ∩ ∂□_m ≠ ∅ .

Every geometric reading of that window goes through one normal form, proved here: a translated open triadic cube is the axis-parallel box of its own corner and side, and membership in either description is the coordinatewise strict inequality.

1. The translated open cube as an axis cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_image_add_openCubeSet_iff {d : ℕ} {j : ℤ} {z y : HCPolySupport.Vec d} : y ∈ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ j < y i - z i ∧ y i - z i < 1 / 2 * 3 ^ j

Membership in a translated open triadic cube, coordinatewise.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_axisCube_iff {d : ℕ} {c : HCPolySupport.Vec d} {L : ℝ} {y : HCPolySupport.Vec d} : y ∈ HCPolySupport.axisCube c L ↔ ∀ (j : Fin d), c j < y j ∧ y j < c j + L

Membership in an axis cube, coordinatewise.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_openCubeSet_eq_axisCube {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) = HCPolySupport.axisCube (fun (i : Fin d) => z i - 1 / 2 * 3 ^ j) (3 ^ j)