BoundaryLaneWindows

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

The truncated comparison windows of the boundary lane, and the choice y := x

The §4.3 boundary regime works on the truncated windows

  W_j := (x + □_{n-j}) ∩ □_m ,        V := W_2 = (x + □_{n-2}) ∩ □_m ,

which are the windows of l.excess.decay.good.scales read through the replacement draft's item 2 (the lemma l.comparison.reduction). This module proves their geometry and the one statement the draft calls the window choice.

The window choice

The printed proof asks for a point y ∈ □_m with both

  y + □_{n-2} ⊆ (z + □_n) ∩ □_m       and      (x + □_{n-2}) ∩ □_m ⊆ y + □_{n-2} ,

and the graph records the gap: "the existence of y with BOTH inclusions is asserted with no construction, and in the boundary case the two requirements pull against each other" — indeed the first inclusion is false at a boundary point x, because the full cube y + □_{n-2} then leaves □_m.

The draft's correction is y := x together with the move of the comparison function onto the truncated window: the pair of requirements becomes

  V = (x + □_{n-2}) ∩ □_m ⊆ (z + □_n) ∩ □_m       and      W_2 = V ,

and both are then immediate from x ∈ (z + □_{n-3}) ∩ □_m. That is truncatedWindow_subset_of_windowChoice and truncatedWindow_two_eq_V below; windowChoice_y_eq_x packages the pair.

What is not done here

Nothing analytic: no harmonic function, no excess, no Caccioppoli estimate. In particular this module does not provide the volume-ratio (window sandwich) constant K_vol of the draft's §0 — only the qualitative positivity of the window volume, which is what the excess normalizers need to be finite.

References

• ABK26, l.excess.decay.good.scales, (windows).

1. A general inclusion for translated origin cubes

2. The truncated windows

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

The truncated window (x + □_k) ∩ □_m of the §4.3 boundary regime, in the frozen theorem's own carrier shape (a translation image of an origin cube, intersected with the domain cube).

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_eq_inter_openCubeAtScale {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : truncatedWindow x m k = HCPolySupport.Book.Ch03.openCubeAtScale x k ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_subset_translate {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : truncatedWindow x m k ⊆ (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_mono {d : ℕ} (x : HCPolySupport.Vec d) (m : ℤ) {k l : ℤ} (hkl : k ≤ l) : truncatedWindow x m k ⊆ truncatedWindow x m l

The truncated windows are nested in the scale.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_truncatedWindow_self {d : ℕ} {x : HCPolySupport.Vec d} {m : ℤ} (k : ℤ) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : x ∈ truncatedWindow x m k

The centre of a truncated window lies in it, as soon as it lies in the domain cube.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_nonempty {d : ℕ} {x : HCPolySupport.Vec d} {m : ℤ} (k : ℤ) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : (truncatedWindow x m k).Nonempty

3. The windows are open bounded convex domains

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpenBoundedConvexDomain_inter {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) : HCPolySupport.IsOpenBoundedConvexDomain (U ∩ V)

The intersection of two open bounded convex domains is one.

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

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

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_truncatedWindow_lt_top {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasureTheory.volume (truncatedWindow x m k) < ⊤

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_truncatedWindow_pos {d : ℕ} {x : HCPolySupport.Vec d} {m : ℤ} (k : ℤ) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : 0 < MeasureTheory.volume (truncatedWindow x m k)

A truncated window centred in the domain cube has positive volume: it is a nonempty open set.

4. The window choice y := x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_mem_openCubeSet_of_mem_truncatedWindow {d : ℕ} {j m : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ truncatedWindow z m j) : x - z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d j)

The printed hypothesis x ∈ (z + □_j) ∩ □_m in its difference form.