OddReflectionWindow

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

The partially reflected window of the §4.3 boundary lane

This module proves the geometry of that construction.

The met faces are pairwise orthogonal, one per coordinate

V is the coordinate box ∏ᵢ (windowLo i, windowHi i) with

  windowLo x m k i = max (xᵢ - ½·3^k) (-½·3^m) ,
  windowHi x m k i = min (xᵢ + ½·3^k) ( ½·3^m) .

The i-th upper face of ∂□_m meets closure V exactly when ½·3^m ≤ xᵢ + ½·3^k (MeetsUpperFace), the lower one exactly when xᵢ - ½·3^k ≤ -½·3^m (MeetsLowerFace). For k < m the two are mutually exclusive (not_meetsLowerFace_of_meetsUpperFace), so at most one face per coordinate is met and the met faces are pairwise orthogonal, as the draft asserts. Consequently the group generated by the corresponding reflections is (ℤ/2)^S for the met set S ⊆ Fin d, of order 2^{#S} ≤ 2^d.

The reflected window is again a box

Because each reflection acts in a single coordinate and the reflected face is an endpoint of that coordinate's interval, the union of the images of V under the group, together with the interface hyperplanes, is again an open coordinate box: reflectedWindow, with

  reflectedLo i = if lower met then -3^m - windowHi i else windowLo i ,
  reflectedHi i = if upper met then  3^m - windowLo i else windowHi i .

This is the cube-adapted substitute for the draft's "open set containing closure W₃", and it is cheaper: no interface bookkeeping is needed, because the box already contains the relatively open faces.

The interior distance (the draft's c(d)·3ⁿ ball)

The draft's key geometric claim — the reflected set "contains a ball of radius c(d)3^n around every point of W₃" — is proved here in the sharper triadic form

  p ∈ W₃ = (x + □_{n-3}) ∩ □_m   ⟹   p + □_{n-3} ⊆ reflectedWindow x m (n-2)

(image_add_openCubeSet_subset_reflectedWindow), i.e. with c(d) = 1/54, uniformly in d, and with the cube p + □_{n-3} rather than a ball, which is the shape CoarseGraining's interior estimates consume.

What is not done here

Nothing analytic. No function is reflected, no H¹ statement is made, and no Hessian estimate is proved.

References

• ABK26, l.excess.decay.good.scales; the odd-reflection step replaced.
• CoarseGraining Homogenization.Sobolev.Foundations.CubeReflection.Reflections (coordFaceReflection, the single-face reflection map adapted downstream).

1. Open coordinate boxes

def Algsuperdiff.Section4.Provider.ExcessDecay.coordBox {d : ℕ} (lo hi : Fin d → ℝ) : Set (HCPolySupport.Vec d)

The open coordinate box ∏ i (lo i, hi i) of Vec d.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.coordBox lo hi = Set.univ.pi fun (i : Fin d) => Set.Ioo (lo i) (hi i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_coordBox_iff {d : ℕ} {lo hi : Fin d → ℝ} {y : HCPolySupport.Vec d} : y ∈ coordBox lo hi ↔ ∀ (i : Fin d), lo i < y i ∧ y i < hi i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_coordBox {d : ℕ} (lo hi : Fin d → ℝ) : IsOpen (coordBox lo hi)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.convex_coordBox {d : ℕ} (lo hi : Fin d → ℝ) : Convex ℝ (coordBox lo hi)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordBox_subset_coordBox {d : ℕ} {lo hi lo' hi' : Fin d → ℝ} (hlo : ∀ (i : Fin d), lo' i ≤ lo i) (hhi : ∀ (i : Fin d), hi i ≤ hi' i) : coordBox lo hi ⊆ coordBox lo' hi'

Widening every coordinate interval enlarges the box.

2. The truncated window as a box

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.windowLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : ℝ

The lower endpoint of the i-th edge of (x + □_k) ∩ □_m.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.windowLo x m k i = max (x i - 1 / 2 * 3 ^ k) (-(1 / 2) * 3 ^ m)

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.windowHi {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : ℝ

The upper endpoint of the i-th edge of (x + □_k) ∩ □_m.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.windowHi x m k i = min (x i + 1 / 2 * 3 ^ k) (1 / 2 * 3 ^ m)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.neg_half_zpow_le_windowLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : -(1 / 2) * 3 ^ m ≤ windowLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowHi_le_half_zpow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : windowHi x m k i ≤ 1 / 2 * 3 ^ m

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_eq_coordBox {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : truncatedWindow x m k = coordBox (windowLo x m k) (windowHi x m k)

The truncated window (x + □_k) ∩ □_m is the coordinate box cut out by windowLo and windowHi.

3. The met faces

def Algsuperdiff.Section4.Provider.ExcessDecay.MeetsUpperFace {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : Prop

The upper i-face of ∂□_m meets the closure of (x + □_k) ∩ □_m.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.MeetsUpperFace x m k i = (1 / 2 * 3 ^ m ≤ x i + 1 / 2 * 3 ^ k)

def Algsuperdiff.Section4.Provider.ExcessDecay.MeetsLowerFace {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : Prop

The lower i-face of ∂□_m meets the closure of (x + □_k) ∩ □_m.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.MeetsLowerFace x m k i = (x i - 1 / 2 * 3 ^ k ≤ -(1 / 2) * 3 ^ m)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.not_meetsLowerFace_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hkm : k < m) (h : MeetsUpperFace x m k i) : ¬MeetsLowerFace x m k i

At most one face per coordinate. A window strictly smaller than the domain cube cannot meet both the upper and the lower i-face; this is what makes the met faces pairwise orthogonal and the reflection group (ℤ/2)^S.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowHi_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsUpperFace x m k i) : windowHi x m k i = 1 / 2 * 3 ^ m

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowHi_of_not_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : ¬MeetsUpperFace x m k i) : windowHi x m k i = x i + 1 / 2 * 3 ^ k

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowLo_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsLowerFace x m k i) : windowLo x m k i = -(1 / 2) * 3 ^ m

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowLo_of_not_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : ¬MeetsLowerFace x m k i) : windowLo x m k i = x i - 1 / 2 * 3 ^ k

4. The partially reflected window

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.reflectedLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : ℝ

The lower endpoint of the i-th edge of the partially reflected window: unchanged unless the lower i-face of ∂□_m is met, in which case the edge is reflected through that face.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : ℝ

The upper endpoint of the i-th edge of the partially reflected window.

Equations

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

def Algsuperdiff.Section4.Provider.ExcessDecay.reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : Set (HCPolySupport.Vec d)

The partially reflected window. The union of the images of V = (x + □_k) ∩ □_m under the reflection group generated by the met faces of ∂□_m, together with the interface hyperplanes: again an open box.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedLo_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsLowerFace x m k i) : reflectedLo x m k i = -3 ^ m - windowHi x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedLo_of_not_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : ¬MeetsLowerFace x m k i) : reflectedLo x m k i = windowLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsUpperFace x m k i) : reflectedHi x m k i = 3 ^ m - windowLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_of_not_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : ¬MeetsUpperFace x m k i) : reflectedHi x m k i = windowHi x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_reflectedWindow_iff {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {y : HCPolySupport.Vec d} : y ∈ reflectedWindow x m k ↔ ∀ (i : Fin d), reflectedLo x m k i < y i ∧ y i < reflectedHi x m k i

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

The window sits inside its own partial reflection.

Note that the endpoint comparisons reflectedLo ≤ windowLo and windowHi ≤ reflectedHi are false for degenerate (empty) windows — reflecting an empty edge through a face moves it — so the inclusion is proved pointwise instead, using only the two-sided bounds a genuine point of the window carries.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : IsOpen (reflectedWindow x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.convex_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : Convex ℝ (reflectedWindow x m k)

5. The reflected window is bounded, and stays inside □_{m+2}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_le {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : reflectedHi x m k i ≤ 3 / 2 * 3 ^ m

theorem Algsuperdiff.Section4.Provider.ExcessDecay.le_reflectedLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : -(3 / 2) * 3 ^ m ≤ reflectedLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedWindow_subset_openCubeSet {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : reflectedWindow x m k ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m + 2))

The partial reflection of a window of □_m never leaves □_{m+2}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isBoundedDomain_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : HCPolySupport.IsBoundedDomain (reflectedWindow x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpenBoundedConvexDomain_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : HCPolySupport.IsOpenBoundedConvexDomain (reflectedWindow x m k)

6. Edge lengths: the reflection doubles exactly the met coordinates

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_sub_reflectedLo_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hkm : k < m) (hup : MeetsUpperFace x m k i) : reflectedHi x m k i - reflectedLo x m k i = 2 * (windowHi x m k i - windowLo x m k i)

On a met coordinate the reflected edge has exactly twice the original length; on an unmet coordinate it is unchanged. This is the per-coordinate form of |reflectedWindow| = 2^{#S} · |V|, the volume identity that makes the odd extension's normalized L² norm equal to the original's.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_sub_reflectedLo_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (hlow : MeetsLowerFace x m k i) : reflectedHi x m k i - reflectedLo x m k i = 2 * (windowHi x m k i - windowLo x m k i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_sub_reflectedLo_of_unmet {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (hlow : ¬MeetsLowerFace x m k i) : reflectedHi x m k i - reflectedLo x m k i = windowHi x m k i - windowLo x m k i

7. The interior distance: the draft's c(d)·3ⁿ ball at c(d) = 1/54

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_openCubeSet_subset_reflectedWindow {d : ℕ} {m n : ℤ} {x p : HCPolySupport.Vec d} (hmn : n - 2 < m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hp : p ∈ truncatedWindow x m (n - 3)) : (fun (y : HCPolySupport.Vec d) => p + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 3)) ⊆ reflectedWindow x m (n - 2)

The draft's key geometric claim, in triadic form.

Every point p of W₃ = (x + □_{n-3}) ∩ □_m carries a full cube p + □_{n-3} inside the partially reflected window of V = (x + □_{n-2}) ∩ □_m. Since p + □_{n-3} contains the sup-ball of radius ½·3^{n-3} = 3ⁿ/54, this is the draft's "ball of radius c(d)3ⁿ around every point of W₃" with the explicit, dimension-free constant c = 1/54.

Only x ∈ □_m and n - 2 < m are used (the anchor's m ≥ n + 5 is far stronger).