OneStepOddClassCornerGeometry

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

Corner geometry: window-hugging slabs at a met face, any met configuration

's residue (2) needs the near-face slab apparatus of OneStepEvenBoundSlab without the one-met-face hypothesis hother: at an edge or corner window two or more faces are met, and the proved slabs (transversally concentric with the centre x at half the triadic side) can poke through a second met face.

The device is per-coordinate window hugging: every box built here uses, in each coordinate that is not the active face, the middle half (hugLo, hugHi) = (windowLo + e/4, windowHi − e/4) of the window's own edge e = windowHi − windowLo. Since every window edge exceeds half the triadic side (half_zpow_lt_window_edge, proved here for all met configurations), the hugged edge exceeds a quarter of the triadic side, and all containments hold with no assumption on the met set beyond the active face itself.

Boxes (active met upper face i, and for the corner a second met upper face j ≠ i; depth delta with 16·delta ≤ 3^k):

• cornerFaceSlab i delta — the near-face slab (a−delta, a) at i, hugged transversally; and its inward delta-translate.
• cornerFaceTaylor i delta — the Taylor box (a−2delta, a+delta) at i, hugged transversally.
• cornerPairSlab i j delta — the corner slab, deep at both i and j.
• cornerPairTaylor i j delta — (a−delta, a) at i, (a−2delta, a+delta) at j, hugged transversally: the Taylor box of the face-j step run on the corner slab.

Containments proved: each slab in the window and in its Taylor box; the reflected and pushed points in the Taylor box; sup-balls of radius 3^k/16 around Taylor points inside the doubled window reflectedWindow (hence the Taylor boxes are inside it); the crude volume lower bound delta^d for the slabs.

1. Window edges at an arbitrary met configuration

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.windowLo_lt_windowHi_of_mem {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : windowLo x m k l < windowHi x m k l

Every window edge is positive, at any met configuration.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.half_zpow_lt_window_edge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : 1 / 2 * 3 ^ k < windowHi x m k l - windowLo x m k l

Every window edge exceeds half the triadic side, at any met configuration: an unmet edge is the full side, and a met edge keeps more than half of it because the centre is inside □_m.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.reflectedLo_le_windowLo {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : reflectedLo x m k l ≤ windowLo x m k l

The partial reflection never raises a lower endpoint (nondegenerate windows).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.windowHi_le_reflectedHi {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : windowHi x m k l ≤ reflectedHi x m k l

The partial reflection never lowers an upper endpoint (nondegenerate windows).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.reflectedHi_eq_add_edge_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : MeetsUpperFace x m k i) : reflectedHi x m k i = 1 / 2 * 3 ^ m + (windowHi x m k i - windowLo x m k i)

On a met upper face the reflected upper endpoint is the face plus the full edge.

2. The hugged transversal edges

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

The lower endpoint of the middle half of the window's l-edge.

Equations

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

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

The upper endpoint of the middle half of the window's l-edge.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugLo_lt_hugHi {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : hugLo x m k l < hugHi x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.windowLo_lt_hugLo {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : windowLo x m k l < hugLo x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugHi_lt_windowHi {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : hugHi x m k l < windowHi x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugHi_sub_hugLo {d : ℕ} {x : HCPolySupport.Vec d} (m k : ℤ) (l : Fin d) : hugHi x m k l - hugLo x m k l = (windowHi x m k l - windowLo x m k l) / 2

The hugged edge is exactly half the window edge.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugLo_add_hugHi {d : ℕ} {x : HCPolySupport.Vec d} (m k : ℤ) (l : Fin d) : hugLo x m k l + hugHi x m k l = windowLo x m k l + windowHi x m k l

The hugged edge is concentric with the window edge.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.quarter_zpow_lt_hug_edge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : 1 / 4 * 3 ^ k < hugHi x m k l - hugLo x m k l

The hugged edge exceeds a quarter of the triadic side.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.eighth_zpow_lt_hug_margin {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : 1 / 8 * 3 ^ k < (windowHi x m k l - windowLo x m k l) / 4

The hug margin exceeds an eighth of the triadic side.

3. The four corner boxes

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

The near-face slab at the met upper i-face, window-hugged transversally.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceSlabLo x m k i delta l = if l = i then 1 / 2 * 3 ^ m - delta else Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugLo x m k l

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

Upper coordinates of the slab meeting one upper cube face.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceSlabHi x m k i l = if l = i then 1 / 2 * 3 ^ m else Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugHi x m k l

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

The Taylor box at the met upper i-face, window-hugged transversally.

Equations

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

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

Upper coordinates of the Taylor box extending across one upper cube face.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceTaylorHi x m k i delta l = if l = i then 1 / 2 * 3 ^ m + delta else Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugHi x m k l

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairSlabLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i j : Fin d) (delta : ℝ) : Fin d → ℝ

The corner slab: deep at both met upper faces i and j.

Equations

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

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

Upper coordinates of the slab meeting two upper cube faces.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairSlabHi x m k i j l = if l = i ∨ l = j then 1 / 2 * 3 ^ m else Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hugHi x m k l

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairTaylorLo {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i j : Fin d) (delta : ℝ) : Fin d → ℝ

The Taylor box of the face-j step run on the corner slab: still deep at i, extended across the j-face.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairTaylorHi {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i j : Fin d) (delta : ℝ) : Fin d → ℝ

Upper coordinates of the Taylor box for the second face of a corner step.

Equations

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

4. Nondegeneracy

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceSlabLo_lt_hi {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hdelta : 0 < delta) (l : Fin d) : cornerFaceSlabLo x m k i delta l < cornerFaceSlabHi x m k i l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairSlabLo_lt_hi {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hdelta : 0 < delta) (l : Fin d) : cornerPairSlabLo x m k i j delta l < cornerPairSlabHi x m k i j l

5. The slabs sit inside the window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hug_subset_window {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (l : Fin d) : windowLo x m k l ≤ hugLo x m k l ∧ hugHi x m k l ≤ windowHi x m k l

The hugged interval is inside the window's edge.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerFaceSlab_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hup : MeetsUpperFace x m k i) (hdelta16 : 16 * delta ≤ 3 ^ k) : coordBox (cornerFaceSlabLo x m k i delta) (cornerFaceSlabHi x m k i) ⊆ truncatedWindow x m k

The face slab is inside the window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerFaceSlab_pushed_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hup : MeetsUpperFace x m k i) (hdelta : 0 < delta) (hdelta16 : 16 * delta ≤ 3 ^ k) : (coordBox (fun (l : Fin d) => cornerFaceSlabLo x m k i delta l - (delta • HCPolySupport.basisVec i) l) fun (l : Fin d) => cornerFaceSlabHi x m k i l - (delta • HCPolySupport.basisVec i) l) ⊆ truncatedWindow x m k

The pushed face slab is inside the window. The inward translate by delta·eᵢ.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerPairSlab_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hupi : MeetsUpperFace x m k i) (hupj : MeetsUpperFace x m k j) (hdelta16 : 16 * delta ≤ 3 ^ k) : coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j) ⊆ truncatedWindow x m k

The corner slab is inside the window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerPairSlab_pushed_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hupi : MeetsUpperFace x m k i) (hupj : MeetsUpperFace x m k j) (hdelta : 0 < delta) (hdelta16 : 16 * delta ≤ 3 ^ k) : (coordBox (fun (l : Fin d) => cornerPairSlabLo x m k i j delta l - (delta • HCPolySupport.basisVec j) l) fun (l : Fin d) => cornerPairSlabHi x m k i j l - (delta • HCPolySupport.basisVec j) l) ⊆ truncatedWindow x m k

The pushed corner slab is inside the window. The inward translate by delta·eⱼ.

6. Memberships in the Taylor boxes

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerFaceSlab_subset_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hdelta : 0 < delta) : coordBox (cornerFaceSlabLo x m k i delta) (cornerFaceSlabHi x m k i) ⊆ coordBox (cornerFaceTaylorLo x m k i delta) (cornerFaceTaylorHi x m k i delta)

The face slab is inside its Taylor box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.reflection_cornerFaceSlab_mem_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hdelta : 0 < delta) {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerFaceSlabLo x m k i delta) (cornerFaceSlabHi x m k i)) : HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y ∈ coordBox (cornerFaceTaylorLo x m k i delta) (cornerFaceTaylorHi x m k i delta)

The reflected face slab is inside the Taylor box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.pushed_cornerFaceSlab_mem_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hdelta : 0 < delta) {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerFaceSlabLo x m k i delta) (cornerFaceSlabHi x m k i)) : y - delta • HCPolySupport.basisVec i ∈ coordBox (cornerFaceTaylorLo x m k i delta) (cornerFaceTaylorHi x m k i delta)

The pushed face slab is inside the Taylor box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerPairSlab_subset_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hdelta : 0 < delta) : coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j) ⊆ coordBox (cornerPairTaylorLo x m k i j delta) (cornerPairTaylorHi x m k i j delta)

The corner slab is inside the pair Taylor box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.reflection_cornerPairSlab_mem_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hij : i ≠ j) (hdelta : 0 < delta) {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j)) : HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) j y ∈ coordBox (cornerPairTaylorLo x m k i j delta) (cornerPairTaylorHi x m k i j delta)

The j-reflected corner slab is inside the pair Taylor box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.pushed_cornerPairSlab_mem_taylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hij : i ≠ j) (hdelta : 0 < delta) {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j)) : y - delta • HCPolySupport.basisVec j ∈ coordBox (cornerPairTaylorLo x m k i j delta) (cornerPairTaylorHi x m k i j delta)

The j-pushed corner slab is inside the pair Taylor box.

7. Sup-balls around the Taylor boxes inside the doubled window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.metricBall_subset_reflectedWindow_of_mem_cornerFaceTaylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hup : MeetsUpperFace x m k i) (hdelta16 : 16 * delta ≤ 3 ^ k) {p : HCPolySupport.Vec d} (hp : p ∈ coordBox (cornerFaceTaylorLo x m k i delta) (cornerFaceTaylorHi x m k i delta)) : Metric.ball p (3 ^ k / 16) ⊆ reflectedWindow x m k

Sup-balls of radius 3^k/16 around the face Taylor box are inside the doubled window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.metricBall_subset_reflectedWindow_of_mem_cornerPairTaylor {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hupi : MeetsUpperFace x m k i) (hupj : MeetsUpperFace x m k j) (hdelta16 : 16 * delta ≤ 3 ^ k) {p : HCPolySupport.Vec d} (hp : p ∈ coordBox (cornerPairTaylorLo x m k i j delta) (cornerPairTaylorHi x m k i j delta)) : Metric.ball p (3 ^ k / 16) ⊆ reflectedWindow x m k

Sup-balls of radius 3^k/16 around the pair Taylor box are inside the doubled window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerFaceTaylor_subset_reflectedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hup : MeetsUpperFace x m k i) (hdelta16 : 16 * delta ≤ 3 ^ k) : coordBox (cornerFaceTaylorLo x m k i delta) (cornerFaceTaylorHi x m k i delta) ⊆ reflectedWindow x m k

The face Taylor box is inside the doubled window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordBox_cornerPairTaylor_subset_reflectedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hupi : MeetsUpperFace x m k i) (hupj : MeetsUpperFace x m k j) (hdelta16 : 16 * delta ≤ 3 ^ k) : coordBox (cornerPairTaylorLo x m k i j delta) (cornerPairTaylorHi x m k i j delta) ⊆ reflectedWindow x m k

The pair Taylor box is inside the doubled window.