BoundaryCoveringGeometry

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

The well-placed cube of the boundary covering step

ABK26's Step 2 applies the boundary coarse-grained Caccioppoli inequality on a truncated window (x+□_{n+1}) ∩ □_m and concludes an energy bound on (x+□_n) ∩ □_m, "after a simple covering argument". CoarseGraining's theorem, however, lives on a cube: an outer triadic cube Q, a Dirichlet patch openCubeAtScale x (Q.scale-1), and the core caccioppoliCoreSet Q x = □_Q ∩ openCubeAtScale x (Q.scale-2).

This module constructs that cube and proves the three inclusions the application needs.

The construction

With hm := 3^m/2, hk := 3^k/2 and the gap A := hm - hk ≥ 0 (this is where k ≤ m enters), the centre is the coordinatewise clamp

  c_i := max (-A) (min A (x_i)) ,        c := wellPlacedCentre x m k .

Clamping is exactly "anchor on the met faces": in a coordinate where the window stays well inside □_m the cube is centred at x_i, and in a coordinate where the window reaches a face the cube slides until its own face coincides with that face of □_m. Consequently

• c + □_k ⊆ □_m — the cube never leaves the domain (so the equation holds on it, and the Dirichlet locus of the application is contained in ∂□_m);
• (x+□_j) ∩ □_m ⊆ c + □_k for every j ≤ k — the cube covers the window, patch included;
• (x+□_j) ∩ □_m ⊆ c + caccioppoliCoreSet (□_k^{origin}) (x-c) for j ≤ k-2 — in the translated frame (A4: the sample is translated, every cube is an origin cube) the anchor's window sits inside CoarseGraining's Caccioppoli core.

What is not done here

No measure theory (that is BoundaryCoveringVolume) and no analysis: this module contains only inclusions of sets.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; boundary application.

1. Membership in a translated set

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_image_add_iff {d : ℕ} {c p : HCPolySupport.Vec d} {S : Set (HCPolySupport.Vec d)} : p ∈ (fun (y : HCPolySupport.Vec d) => c + y) '' S ↔ p - c ∈ S

A point lies in the translate c + S exactly when its back-translate lies in S.

2. The well-placed centre

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedHalfGap (m k : ℤ) : ℝ

The clamping gap 3^m/2 - 3^k/2 of the well-placed cube.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedHalfGap m k = 1 / 2 * 3 ^ m - 1 / 2 * 3 ^ k

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

The centre of the well-placed cube: the coordinatewise clamp of x into the set of centres whose cube of side 3^k still fits inside □_m.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedHalfGap_nonneg {m k : ℤ} (hkm : k ≤ m) : 0 ≤ wellPlacedHalfGap m k

theorem Algsuperdiff.Section4.Provider.ExcessDecay.neg_wellPlacedHalfGap_le_wellPlacedCentre {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : -wellPlacedHalfGap m k ≤ wellPlacedCentre x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedCentre_le_wellPlacedHalfGap {d : ℕ} {m k : ℤ} (hkm : k ≤ m) (x : HCPolySupport.Vec d) (i : Fin d) : wellPlacedCentre x m k i ≤ wellPlacedHalfGap m k

3. The cube stays inside the domain

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

The well-placed cube never leaves □_m. This is what makes the printed "the equation holds on the covering cube" legitimate, and it forces the Dirichlet locus of the Caccioppoli application into ∂□_m.

4. The cube covers the truncated window

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

The well-placed cube covers the truncated window.

For every scale j ≤ k the anchor's window (x+□_j) ∩ □_m lies inside the translated cube c + □_k. At j = k-1 this is the covering of the Caccioppoli Dirichlet patch; at j = k-2 it is the covering of the energy window.

5. The window sits in CoarseGraining's Caccioppoli core

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scale_originCube (d : ℕ) (k : ℤ) : (HCPolySupport.originCube d k).scale = k

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_subset_image_add_caccioppoliCoreSet {d : ℕ} {m k j : ℤ} (x : HCPolySupport.Vec d) (hkm : k ≤ m) (hjk : j ≤ k - 2) : truncatedWindow x m j ⊆ (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k)

The covering inclusion in CoarseGraining's own window shape.

In the translated frame the anchor's window (x+□_j) ∩ □_m with j ≤ k-2 is contained in caccioppoliCoreSet (□_k) (x-c), the core of CoarseGraining's boundary coarse Caccioppoli inequality at the outer cube □_k and centre x-c. Together with image_add_wellPlacedCentre_subset_openCubeSet this is the geometric content of the printed "simple covering argument".