OffGridStabilityGeometry

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

The covering geometry of an off-grid cube

The printed proof of l.lambdas.stability (ABK26) controls a coarse-grained quantity on an off-grid cube x + □_k by the same quantity on grid cubes, through a greedy family

𝒢_n(U) = { z ∈ 3^n ℤ^d ∖ (already covered) : z + □_{n+1} ⊆ U }

together with the packing count ∑_{z ∈ 𝒢_n(y+□_k)} |□_n| / |□_k| ≤^{n-k}.

This module proves that geometry. The family used here is the equivalent maximal-cube description

Q is selected for V  ↔  Q ⊆ V  and  parent(Q) ⊄ V,

which for the half-open realizations is an exact countable partition of any bounded open V — no null set is discarded anywhere. For V an arbitrary real translate of a triadic cube the packing count is proved with the explicit constant 2d:

|⋃ {Q selected, scale Q = m}|  ≤  2 d · 3^{m + 1 - k} · |V| .

What is proved and what is not

Only geometry. No coefficient field, no response functional, no homogenization error appears below; in particular nothing here is an instance of, or a fraction of, any source node. The analytic half of the off-grid stability estimate — countable subadditivity of the response functional across this family — is proved in OffGridStabilitySubadditivity.lean and lives in OffGridStabilitySubadditivity.lean.

Deviation from the printed family (recorded)

The printed 𝒢_n(U) selects z with z + □_{n+1} ⊆ U and then removes cubes already covered at coarser scales. The maximal-cube family below selects Q with Q ⊆ V and parent(Q) ⊄ V. The two differ by at most one scale (the printed family's selection test is the parent's containment, so its cubes are one generation finer where both are nonempty), which changes the packing constant by a factor 3 and nothing else; the printed count C 3^{n-k} is matched with C = 2d for the maximal family. The maximal family is used because it partitions V exactly rather than up to a null set, which is what the countable subadditivity consumes.

Main results

• exists_maximalCubeIn_mem — every point of a bounded open set lies in a maximal grid cube of that set.
• iUnion_maximalCubes_eq — the exact partition.
• scale_le_of_maximalCubeIn_offGridCube — the selected scales are ≤ k.
• volume_iUnion_maximalCubesAtScale_toReal_le — the packing count with the explicit constant 2d.

References

• ABK26, l.lambdas.stability.
• ABK26, e.mathcalE.stability.applied.
• CoarseGraining, Homogenization/Geometry/BoundaryLayer.lean, Homogenization/Geometry/CubeMeasure.lean, Homogenization/Geometry/Translation.lean.

1. The off-grid cube and the maximal-cube family

def Algsuperdiff.Section4.Provider.ExcessDecay.offGridCube {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : Set (HCPolySupport.Vec d)

The off-grid cube w + □_k, as the real translate of an open triadic cube. No integrality is assumed of w.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.offGridCube w P = HCPolySupport.translateSet w (HCPolySupport.openCubeSet P)

def Algsuperdiff.Section4.Provider.ExcessDecay.MaximalCubeIn {d : ℕ} (V : Set (HCPolySupport.Vec d)) (Q : HCPolySupport.TriadicCube d) : Prop

Q is a maximal grid cube of V: it fits inside V, its parent does not.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.MaximalCubeIn V Q = (HCPolySupport.cubeSet Q ⊆ V ∧ ¬HCPolySupport.cubeSet (HCPolySupport.parentCube Q) ⊆ V)

def Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubes {d : ℕ} (V : Set (HCPolySupport.Vec d)) : Set (HCPolySupport.TriadicCube d)

The set of maximal grid cubes of V.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubes V = {Q : HCPolySupport.TriadicCube d | Algsuperdiff.Section4.Provider.ExcessDecay.MaximalCubeIn V Q}

def Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubesAtScale {d : ℕ} (V : Set (HCPolySupport.Vec d)) (m : ℤ) : Set (HCPolySupport.TriadicCube d)

The maximal grid cubes of V of one fixed scale.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubesAtScale V m = {Q : HCPolySupport.TriadicCube d | Algsuperdiff.Section4.Provider.ExcessDecay.MaximalCubeIn V Q ∧ Q.scale = m}

2. The off-grid cube is open, and has the volume of its shape cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_offGridCube {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : IsOpen (offGridCube w P)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_offGridCube {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : MeasureTheory.volume (offGridCube w P) = MeasureTheory.volume (HCPolySupport.openCubeSet P)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_offGridCube_toReal {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : (MeasureTheory.volume (offGridCube w P)).toReal = HCPolySupport.cubeVolume P

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_offGridCube_ne_top {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : MeasureTheory.volume (offGridCube w P) ≠ ⊤

3. Existence of a maximal cube through every point

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scale_le_of_cubeSet_subset_offGridCube {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P Q : HCPolySupport.TriadicCube d} (h : HCPolySupport.cubeSet Q ⊆ offGridCube w P) : Q.scale ≤ P.scale

A grid cube contained in the off-grid cube has scale at most the shape cube's scale: its volume cannot exceed the volume of the off-grid cube.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_maximalCubeIn_mem {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P : HCPolySupport.TriadicCube d} {x : HCPolySupport.Vec d} (hx : x ∈ offGridCube w P) : ∃ (Q : HCPolySupport.TriadicCube d), MaximalCubeIn (offGridCube w P) Q ∧ x ∈ HCPolySupport.cubeSet Q

Every point of a bounded open set lies in a maximal grid cube of it.

The set of scales whose address cube fits inside V is downward closed, nonempty because V is open, and bounded above because V has finite volume; its greatest element gives the maximal cube.

4. The family is an exact partition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.disjoint_cubeSet_of_maximalCubeIn {d : ℕ} {V : Set (HCPolySupport.Vec d)} {Q R : HCPolySupport.TriadicCube d} (hQ : MaximalCubeIn V Q) (hR : MaximalCubeIn V R) (hne : Q ≠ R) : Disjoint (HCPolySupport.cubeSet Q) (HCPolySupport.cubeSet R)

Distinct maximal cubes of V are disjoint.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.iUnion_maximalCubes_eq {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : ⋃ Q ∈ maximalCubes (offGridCube w P), HCPolySupport.cubeSet Q = offGridCube w P

The maximal cubes tile the off-grid cube exactly — not merely up to a null set.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scale_le_of_maximalCubeIn_offGridCube {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P Q : HCPolySupport.TriadicCube d} (hQ : MaximalCubeIn (offGridCube w P) Q) : Q.scale ≤ P.scale

5. The packing count

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_iUnion_maximalCubesAtScale_toReal_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (m : ℤ) : (MeasureTheory.volume (⋃ Q ∈ maximalCubesAtScale (offGridCube w P) m, HCPolySupport.cubeSet Q)).toReal ≤ 2 * ↑d * 3 ^ (m + 1 - P.scale) * HCPolySupport.cubeVolume P

The packing count.

The maximal cubes of one scale m all sit in the 3^{m+1}-boundary layer of the off-grid cube, so their total volume is at most 2d·3^{m+1-k} times the volume of the off-grid cube. This is the formalized ∑_{z ∈ 𝒢_n(y+□_k)} |□_n|/|□_k| ≤^{n-k} of the printed proof, with the explicit constant C = 2d.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_iUnion_maximalCubesAtScale_ne_top {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (m : ℤ) : MeasureTheory.volume (⋃ Q ∈ maximalCubesAtScale (offGridCube w P) m, HCPolySupport.cubeSet Q) ≠ ⊤

Each scale-m union is finite in measure.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tsum_volume_maximalCubesAtScale {d : ℕ} (V : Set (HCPolySupport.Vec d)) (m : ℤ) : MeasureTheory.volume (⋃ Q ∈ maximalCubesAtScale V m, HCPolySupport.cubeSet Q) = ∑' (Q : ↑(maximalCubesAtScale V m)), MeasureTheory.volume (HCPolySupport.cubeSet ↑Q)

The scale-m union, as a genuinely countable sum of cube volumes.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.tsum_volume_maximalCubesAtScale_toReal_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (m : ℤ) : (∑' (Q : ↑(maximalCubesAtScale (offGridCube w P) m)), MeasureTheory.volume (HCPolySupport.cubeSet ↑Q)).toReal ≤ 2 * ↑d * 3 ^ (m + 1 - P.scale) * HCPolySupport.cubeVolume P

The packing count in summed form, the shape the countable subadditivity consumes.