BoundaryCoveringVolume

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

The covering inequality of the boundary lane

BoundaryCoveringGeometry places a cube of side 3^k so that it stays inside □_m and covers the truncated window (x+□_j) ∩ □_m. This module supplies the quantitative half of the printed "simple covering argument": a normalized quantity on the anchor's window is controlled by the same normalized quantity on CoarseGraining's Caccioppoli core, at the dimension-only cost

  |core| / |(x+□_{k-2}) ∩ □_m|  ≤  3^d .

Where the 3^d comes from (disclosed)

The lower bound on the window volume is obtained by inscribing a cube: the well-placed cube of side 3^{k-3} centred at wellPlacedCentre x m (k-3) fits inside (x+□_{k-2}) ∩ □_m (a clamped centre moves by less than half a side, so the inscribed cube stays within 3^{k-3} of x, and 3^{k-3} < 3^{k-2}/2). The core is contained in a cube of side 3^{k-2} = 3·3^{k-3}, whence 3^d.

The sharp constant for this geometry is 2^d (each coordinate interval of the truncated window has length at least 3^{k-2}/2), obtained by computing the volume of the window as a product of intervals. The inscribed-cube route is taken here because it reuses the cube volume A verbatim; the loss is a (3/2)^d factor inside a C(d) and is recorded, not hidden.

Main results

• image_add_wellPlacedCentre_subset_truncatedWindow — the inscribed cube.
• volume_toReal_image_add_openCubeSet_originCube — a translated origin cube has volume (3^n)^d.
• volume_toReal_wellPlacedCore_le_three_pow_mul_truncatedWindow — the ratio.
• normalizedSetAverage_le_mul_of_subset — the general covering inequality for a nonnegative integrand.
• normalizedSetAverage_truncatedWindow_le_three_pow_mul_wellPlacedCore — the covering step, in the anchor's own frame.

What is not done here

The covering is proved for normalized set averages of a nonnegative integrand, which is the shape of every quantity on the right of the printed display (localizedCoeffEnergyValue is such an average of the coefficient energy density, normalizedL2SqOnSet of a square).

References

• ABK26, ("after a simple covering argument").
• CoarseGraining, Geometry/CubeMeasure.lean, Geometry/Translation.lean.

1. The inscribed cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_subset_truncatedWindow {d : ℕ} {m j : ℤ} (x : HCPolySupport.Vec d) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hjm : j - 1 ≤ m) : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (j - 1) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (j - 1)) ⊆ truncatedWindow x m j

The inscribed cube. The well-placed cube of side 3^{j-1} sits inside the truncated window (x+□_j) ∩ □_m: it stays in □_m by construction, and its centre is within 3^{j-1}/2 of x, so the whole cube is within 3^{j-1} of x, which is less than the half-side 3^j/2.

2. Volumes of translated origin cubes

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_eq_preimage {d : ℕ} (c : HCPolySupport.Vec d) (S : Set (HCPolySupport.Vec d)) : (fun (y : HCPolySupport.Vec d) => c + y) '' S = (fun (y : HCPolySupport.Vec d) => -c + y) ⁻¹' S

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_image_add {d : ℕ} (c : HCPolySupport.Vec d) (S : Set (HCPolySupport.Vec d)) : MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c + y) '' S) = MeasureTheory.volume S

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_openCubeSet_originCube_ne_top (d : ℕ) (n : ℤ) : MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ≠ ⊤

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_openCubeSet_originCube (d : ℕ) (n : ℤ) : (MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))).toReal = (3 ^ n) ^ d

3. The volume ratio

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_wellPlacedCore_le_three_pow_mul_truncatedWindow {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) : (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k))).toReal ≤ 3 ^ d * (MeasureTheory.volume (truncatedWindow x m (k - 2))).toReal

The covering ratio. The translated Caccioppoli core is at most 3^d times the anchor's window in volume.

4. The covering inequality

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_le_mul_of_subset {d : ℕ} {S T : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {K : ℝ} (hST : S ⊆ T) (hSpos : 0 < MeasureTheory.volume S) (hTtop : MeasureTheory.volume T < ⊤) (hTmeas : MeasurableSet T) (hf : ∀ y ∈ T, 0 ≤ f y) (hint : MeasureTheory.IntegrableOn f T MeasureTheory.volume) (hK : (MeasureTheory.volume T).toReal ≤ K * (MeasureTheory.volume S).toReal) : HCPolySupport.Book.Ch03.normalizedSetAverage S f ≤ K * HCPolySupport.Book.Ch03.normalizedSetAverage T f

The covering inequality. A normalized average over a subset is bounded by the volume ratio times the normalized average over the ambient set, for a nonnegative integrable integrand. This is CoarseGraining's 18^d argument abstracted from its geometry.

5. The covering step of the boundary lane

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_image_add_caccioppoliCoreSet {d : ℕ} (c : HCPolySupport.Vec d) (Q : HCPolySupport.TriadicCube d) (w : HCPolySupport.Vec d) : IsOpen ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet Q w)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedSetAverage_truncatedWindow_le_three_pow_mul_wellPlacedCore {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) {f : HCPolySupport.Vec d → ℝ} (hf : ∀ y ∈ (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k), 0 ≤ f y) (hint : MeasureTheory.IntegrableOn f ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k)) MeasureTheory.volume) : HCPolySupport.Book.Ch03.normalizedSetAverage (truncatedWindow x m (k - 2)) f ≤ 3 ^ d * HCPolySupport.Book.Ch03.normalizedSetAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d k) (x - wellPlacedCentre x m k)) f

The covering step.

The normalized average of a nonnegative integrand over the anchor's window (x+□_{k-2}) ∩ □_m is at most 3^d times its normalized average over the translated Caccioppoli core of the well-placed cube — the set on which CoarseGraining's boundary Caccioppoli inequality delivers an estimate. With the integrand the coefficient energy density this is exactly the printed covering conversion.