OffGridStabilityCap

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

The per-cube cap the covering consumes

The printed proof of l.lambdas.stability (ABK26) feeds the greedy covering with e.bound.one.cube.by.lambdas: every grid cube inside the big cube has its one-cube quantity bounded by 3^{2s·depth} times the multiscale quantity of the big cube.

This module proves the 𝓔_{·,∞,2} form of that input:

max_{|e|=1} 𝐉(Q, …)  ≤  3^{2u·(P.scale − Q.scale)} · 𝓔_{u,∞,2}(P; a, a₀)²

for any grid cube Q whose half-open realization is contained in P's — no descendant hypothesis is assumed, it is derived — and the recognition lemma that supplies it.

Two ingredients, both from already-proved material:

• mem_descendantsAtScale_of_cubeSet_subset (new here) — containment of half-open realizations plus a scale inequality already forces descendancy. This is what turns the covering geometry's maximal cubes, which are only known to sit inside a real translate of a cube, into descendants of the enclosing grid cube once the printed containment x + □_n ⊆ z + □_{n+2} is supplied.
• normalizedBlockResponseMax_le_homogenizationErrorOnCube_sq (new here) — the q = 2 sibling of CoarseGraining's Ch02.scaleResponseAtScale_infinity_self_le_homogenizationErrorOnCube_infinity_one, proved by the same route through Homogenization.self_le_tsum_geometricWeight_of_monotone; there is no normalization constant, because the shell sequence is monotone and the weights sum to 1. That last point matters: the naive route through the single weight c_{2u}3^{-2uj} would cost a spurious (1 - 3^{-2u})^{-1} ≍ u^{-1}, i.e. an s-power, and the printed e.bound.one.cube.by.lambdas — which carries no such factor — is therefore correct as printed.

Main results

• mem_descendantsAtScale_of_cubeSet_subset — containment forces descendancy.
• normalizedBlockResponseMax_le_homogenizationErrorOnCube_sq — the one-cube bound at zero depth, constant 1.
• normalizedBlockResponseMax_le_rpow_mul_homogenizationErrorOnCube_sq — the displayed per-cube cap.

References

• ABK26, e.bound.one.cube.by.lambdas.
• ABK26, l.lambdas.stability.
• CoarseGraining, Homogenization/Deterministic/MultiscaleQuantitiesBasic/Foundation/Geometric.lean (self_le_tsum_geometricWeight_of_monotone), Homogenization/Book/Ch02/Theorems/HomogenizationError/ResponseBounds.lean.

1. Containment forces descendancy

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeCenter_mem_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeCenter Q ∈ HCPolySupport.cubeSet Q

The centre of a triadic cube lies in its half-open realization.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_descendantsAtScale_of_cubeSet_subset {d : ℕ} {P Q : HCPolySupport.TriadicCube d} (hsub : HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet P) (hscale : Q.scale ≤ P.scale) : Q ∈ HCPolySupport.descendantsAtScale P Q.scale

Containment forces descendancy.

If the half-open realization of Q sits inside that of P and Q is not coarser, then Q is a triadic descendant of P. No common-root hypothesis is needed: the address map of OffGridStabilityGrid.lean recovers it.

2. The one-cube bound at zero depth

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedBlockResponseMax_le_homogenizationErrorOnCube_sq {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {u : ℝ} (hu : 0 < u) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q a a0 ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ^ 2

The one-cube bound at zero depth, with constant 1.

max_{|e|=1} 𝐉(Q, …)  ≤  𝓔_{u,∞,2}(Q; a, a₀)² .

There is no (1 - 3^{-2u})^{-1}: the shell sequence is nondecreasing and the geometric weights sum to 1, so the whole weighted average dominates the zeroth shell. This is why e.bound.one.cube.by.lambdas is correct as printed and no s-power is lost at this step.

3. The per-cube cap

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedBlockResponseMax_le_rpow_mul_homogenizationErrorOnCube_sq {d : ℕ} [NeZero d] {P Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {u : ℝ} (hu : 0 < u) (hsub : HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet P) (hscale : Q.scale ≤ P.scale) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q a a0 ≤ Real.rpow 3 (u * ↑(P.scale - Q.scale).toNat * 2) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube P u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ^ 2

The per-cube cap of the printed covering argument.

For every grid cube Q contained in P,

max_{|e|=1} 𝐉(Q, …)  ≤  3^{2u·(P.scale − Q.scale)} · 𝓔_{u,∞,2}(P; a, a₀)² .

This is e.bound.one.cube.by.lambdas in the 𝓔_{·,∞,2} normalization, and it is what the countable subadditivity's majorant B is instantiated with.