OffGridStabilityGrid

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

The triadic grid as a tiling: the addressing lemmas for the covering geometry

The printed proof of l.lambdas.stability (ABK26) decomposes an off-grid cube x + □_k by grid triadic cubes, using the greedy family

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

Everything about that family rests on three facts about CoarseGraining's triadic cubes which CoarseGraining itself only records relative to a fixed root cube (descendantsAtDepth, pairwiseDisjoint_descendantsAtDepth.):

• at each scale the half-open cubes tile ℝ^d — every point lies in exactly one, and its address is a floor;
• every cube sits inside its parentCube;
• two arbitrary half-open triadic cubes are nested or disjoint, with no common root assumed.

This module proves those three, which is the addressing half of the covering geometry. Nothing here mentions the homogenization error, coefficients, or measures of anything but cubes: it is pure grid combinatorics on Vec d = Fin d → ℝ.

Why CoarseGraining's lemmas do not already give this

Homogenization.pairwiseDisjoint_descendantsAtDepth and Homogenization.cubeSet_eq_iUnion_descendantsAtDepth are indexed by a root cube Q and describe only the sub-tree below it. The greedy family of an off-grid cube contains cubes of unboundedly many scales that have no common triadic ancestor inside the off-grid cube, so the sub-tree A cannot express its disjointness. cubeAt below supplies the missing global address map.

Main results

• mem_cubeSet_cubeAt, eq_cubeAt_of_mem_cubeSet — the tiling and its address.
• cubeSet_subset_cubeSet_parentCube — a cube sits in its parent.
• cubeSet_subset_of_le_of_mem_of_mem — nested-or-disjoint, root-free.

References

• ABK26, l.lambdas.stability, (the greedy family 𝒢_n(U)).
• ABK26, e.mathcalE.stability.applied, (the consumer).
• CoarseGraining, Homogenization/Geometry/TriadicCube.lean, Homogenization/Geometry/TriadicPartition.lean.

1. The scale factor

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeScaleFactor_pos' {d : ℕ} (Q : HCPolySupport.TriadicCube d) : 0 < HCPolySupport.cubeScaleFactor Q

2. The address map

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

The triadic address of a point at a given scale. This is the unique half-open triadic cube of scale m containing x; its index is the floor ⌊x i / 3^m + 1/2⌋.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.cubeAt m x = { scale := m, index := fun (i : Fin d) => ⌊x i / 3 ^ m + 1 / 2⌋ }

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeAt_scale {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) : (cubeAt m x).scale = m

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeScaleFactor_cubeAt {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) : HCPolySupport.cubeScaleFactor (cubeAt m x) = 3 ^ m

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_cubeSet_cubeAt {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) : x ∈ HCPolySupport.cubeSet (cubeAt m x)

The grid covers.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eq_cubeAt_of_mem_cubeSet {d : ℕ} {Q : HCPolySupport.TriadicCube d} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) : Q = cubeAt Q.scale x

The grid is a tiling: membership determines the address.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eq_of_scale_eq_of_mem_of_mem {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {x : HCPolySupport.Vec d} (hscale : Q.scale = R.scale) (hQ : x ∈ HCPolySupport.cubeSet Q) (hR : x ∈ HCPolySupport.cubeSet R) : Q = R

Two triadic cubes of the same scale sharing a point are equal.

3. The parent inclusion

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeScaleFactor_parentCube {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeScaleFactor (HCPolySupport.parentCube Q) = 3 * HCPolySupport.cubeScaleFactor Q

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeSet_subset_cubeSet_parentCube {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet (HCPolySupport.parentCube Q)

A triadic cube sits inside its parent.

Proved directly from the coordinate description: with r i = (Q.index i + 1) % 3 ∈ {0, 1, 2} one has 3 * (parentCube Q).index i = Q.index i + 1 - r i, so the parent's coordinate window [(p - 1/2)·3^{m+1}, (p + 1/2)·3^{m+1}) contains [(q - 1/2)·3^m, (q + 1/2)·3^m).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.parentCube_cubeAt {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) : HCPolySupport.parentCube (cubeAt m x) = cubeAt (m + 1) x

The parent of the address cube at scale m is the address cube at m + 1.

4. Iterated parents and the nested-or-disjoint dichotomy

def Algsuperdiff.Section4.Provider.ExcessDecay.ancestorCube {d : ℕ} (j : ℕ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.TriadicCube d

The j-fold parent of a cube.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.ancestorCube j Q = HCPolySupport.parentCube^[j] Q

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ancestorCube_zero {d : ℕ} (Q : HCPolySupport.TriadicCube d) : ancestorCube 0 Q = Q

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ancestorCube_succ {d : ℕ} (j : ℕ) (Q : HCPolySupport.TriadicCube d) : ancestorCube (j + 1) Q = HCPolySupport.parentCube (ancestorCube j Q)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ancestorCube_scale {d : ℕ} (j : ℕ) (Q : HCPolySupport.TriadicCube d) : (ancestorCube j Q).scale = Q.scale + ↑j

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeSet_subset_cubeSet_ancestorCube {d : ℕ} (j : ℕ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet (ancestorCube j Q)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeSet_subset_of_le_of_mem_of_mem {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {x : HCPolySupport.Vec d} (hle : Q.scale ≤ R.scale) (hQ : x ∈ HCPolySupport.cubeSet Q) (hR : x ∈ HCPolySupport.cubeSet R) : HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet R

Nested or disjoint, without a common root.

If a point lies in two half-open triadic cubes and the first has the smaller scale, then the first is contained in the second. This is the root-free replacement for CoarseGraining's pairwiseDisjoint_descendantsAtDepth.