OffGridComposeDepth

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

The depth reindexing: the packing count into the geometric sum

The printed proof of l.lambdas.stability (ABK26) sums the per-cube cap 3^{2s·depth} against the packing count of the greedy family. The two halves are proved: the covering geometry gives, for each scale, the packing count

∑_{Q maximal, scale Q = k − n} |Q|  ≤  2d·3^{1−n}·|w + □_k| ,

and the exponent bookkeeping gives the geometric sum ∑_n W(n)·3^{2un} ≤ 2C/(1−2u) for W(n) ≤ C·3^{−n}. What is missing is the reindexing: the covering is one countable family of cubes of unboundedly many scales, while the arithmetic is a series over the depth n.

This module supplies it, by fibering the maximal-cube family over maximalCubeDepth (Equiv.sigmaFiberEquiv), identifying each fibre with maximalCubesAtScale (maximalCubesFiberEquiv), and applying summable_sigma_of_nonneg / Summable.tsum_sigma. Summability is not assumed: it is produced here, and it is exactly what the countable subadditivity and the covering step need as their majorant obligation. (The trivial cardinality bound 3^{dn} on the depth-n cubes would make the series diverge; only the covering geometry's boundary-layer packing count 6d·3^{−n} makes it converge. Summability is therefore genuine content, not bookkeeping.)

The volume sums are done in ℝ≥0∞, where the fibre volumes need no summability side condition, and converted at the end through ENNReal.summable_toReal and ENNReal.tsum_toReal_eq.

Main results

• maximalCubeDepth — the depth of a maximal cube below the shape cube.
• summable_and_tsum_maximalCubes_depth_le — the reindexed geometric sum, with the explicit constant 12d/(1−2u).
• summable_and_tsum_maximalCubes_cap_le — the same with the constant factor the per-cube cap carries.

References

• ABK26, l.lambdas.stability, (the double sum).
• Repo, Provider/ExcessDecay/OffGridStabilityGeometry.lean, Provider/ExcessDecay/OffGridStabilityArith.lean.

1. The depth fibration of the maximal-cube family

def Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubeDepth {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (Q : ↑(maximalCubes (offGridCube w R))) : ℕ

The depth of a maximal grid cube of the off-grid cube w + R below the shape cube R. Well-defined as a natural number because every maximal cube has scale at most R.scale (scale_le_of_maximalCubeIn_offGridCube).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubeDepth w R Q = (R.scale - (↑Q).scale).toNat

def Algsuperdiff.Section4.Provider.ExcessDecay.maximalCubesFiberEquiv {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (n : ℕ) : { Q : ↑(maximalCubes (offGridCube w R)) // maximalCubeDepth w R Q = n } ≃ ↑(maximalCubesAtScale (offGridCube w R) (R.scale - ↑n))

The depth-n fibre of the maximal-cube family is the scale-(k − n) part of it. Pure bookkeeping: the two subtypes have the same underlying cubes.

Equations

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

2. The shell volumes

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.shellVolume {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (n : ℕ) : ℝ

The total volume of the depth-n maximal cubes of w + R.

Equations

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

3. The reindexed sum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.summable_and_tsum_maximalCubes_depth_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) {u : ℝ} (hu0 : 0 < u) (hu : u < 1 / 2) : (Summable fun (Q : ↑(maximalCubes (offGridCube w R))) => HCPolySupport.cubeVolume ↑Q * 3 ^ (2 * u * ↑(maximalCubeDepth w R Q))) ∧ ∑' (Q : ↑(maximalCubes (offGridCube w R))), HCPolySupport.cubeVolume ↑Q * 3 ^ (2 * u * ↑(maximalCubeDepth w R Q)) ≤ 12 * ↑d * HCPolySupport.cubeVolume R / (1 - 2 * u)

The depth sum of the covering.

Both the summability and the value of the multi-scale series over the maximal cubes of an arbitrary real translate, at the explicit constant 12d/(1−2u) of the exponent bookkeeping's table.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.summable_and_tsum_maximalCubes_cap_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) {u c : ℝ} (hu0 : 0 < u) (hu : u < 1 / 2) (hc : 0 ≤ c) : (Summable fun (Q : ↑(maximalCubes (offGridCube w R))) => HCPolySupport.cubeVolume ↑Q * (c * 3 ^ (2 * u * ↑(maximalCubeDepth w R Q)))) ∧ ∑' (Q : ↑(maximalCubes (offGridCube w R))), HCPolySupport.cubeVolume ↑Q * (c * 3 ^ (2 * u * ↑(maximalCubeDepth w R Q))) ≤ c * (12 * ↑d * HCPolySupport.cubeVolume R / (1 - 2 * u))

The depth sum with the constant factor the per-cube cap carries.