StabilityIndexCube

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

Index and one-scale cube stability of the (∞,2) homogenization error

Two elementary stability properties of CoarseGraining's 𝓔_{s,∞,2} at a fixed coefficient family and comparator, both derived here (not assumed) at the q = 2 exponent that the Section 4.3 good-event caps use:

• index antitonicity — 𝓔 decreases when its first index increases;
• one-scale cube descent — passing from a cube to a triadic descendant costs the single factor 3^{s·(depth)}.

What this module does and does not do

l.lambdas.stability is a one-scale descent for an arbitrary translate: its target cube is x + □_{-1} for a real x with x + □_{-1} ⊆ □_0, and its proof is a greedy Whitney-type decomposition of that off-grid cube by grid subcubes at all deeper scales, combined with subadditivity of σ_*^{-1} and a packing count. Nothing of that kind is proved here.

What is proved here is the grid case: the target cube is a triadic descendant, so the shell maxima of the smaller cube are literally a subfamily of the shell maxima of the larger one and the whole estimate is the reindexing w_{s,2}(l) = 3^{2s·h} w_{s,2}(l+h) of the geometric weights. In that case the constant is not the printed C(d)/(1−2s) but the explicit 3^{s·h}, which for a one-scale descent (h = 1) and s ≤ 1 is at most 3.

It is not smuggled in anywhere below: every statement quantifies over descendantsAtScale, never over translates.

Monotonicity directions, derived

Both directions matter for the §4.3 chain and both are read off the same shell representation

𝓔_{s,∞,2}(Q; a, a₀)²  =  ∑_{l≥0} w_{s,2}(l) · M_l(Q),
      w_{s,2}(l) = (1 − 3^{-2s}) 3^{-2sl},   M_l(Q) = max_{R ⊆ Q, scale Q.scale−l} J(R),

in which l ↦ M_l(Q) is nondecreasing (deeper shells maximize over more cubes) and ∑_l w_{s,2}(l) = 1:

• larger s concentrates the unit mass on small l, i.e. on the smaller terms of a nondecreasing sequence, hence 𝓔 is antitone in the index;
• descending to a depth-h descendant deletes the h shallowest shells and shifts the rest, hence the factor 3^{2s·h} on the square.

The first item is the one the §4.3 chain needs: the annular anchor delivers the cap at the small index s/8, while the consumers ask for the larger indices s/6 and s/4, so the index change is free (constant 1) and in particular needs no part of l.lambdas.stability.

Main results

• homogenizationErrorOnCube_infinity_two_nonneg — 0 ≤ 𝓔_{s,∞,2}.
• homogenizationErrorOnCube_infinity_two_le_of_lt — index antitonicity.
• homogenizationErrorOnCube_infinity_two_le_of_mem_descendantsAtScale — the fixed-index descent, with factor 3^{s·depth}.
• homogenizationErrorOnCube_infinity_two_descendant_index_le — the composite the §4.3 caps chain performs.

References

• ABK26, e.mathcalE.stability.applied.
• ABK26, l.lambdas.stability.
• ABK26, d.mathcal.E; the shell display.

0. Two arithmetic helpers

1. The shell series of the (∞,2) square

theorem Algsuperdiff.Section4.Provider.ExcessDecay.homogenizationErrorOnCube_infinity_two_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s : ℝ} (hs : 0 < s) : 0 ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0

2. Index antitonicity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.homogenizationErrorOnCube_infinity_two_le_of_lt {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {t s : ℝ} (ht : 0 < t) (hts : t < s) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0

𝓔_{·,∞,2} is antitone in its first index.

For 0 < t < s the smaller index dominates:

𝓔_{s,∞,2}(Q; a, a₀)  ≤  𝓔_{t,∞,2}(Q; a, a₀) .

This is the direction the §4.3 caps chain needs — the annular anchor delivers its cap at s/8, the consumers ask for s/6 and s/4 — and it costs no constant at all. It is the q = 2 sibling of CoarseGraining's Ch02.homogenizationErrorOnCube_infinity_one_le_of_lt.

3. One-scale cube descent at a fixed index

theorem Algsuperdiff.Section4.Provider.ExcessDecay.homogenizationErrorOnCube_infinity_two_le_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s : ℝ} (hs : 0 < s) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube R s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0

Fixed-index descent to a triadic descendant.

If R is a triadic descendant of Q at scale k, then

𝓔_{s,∞,2}(R; a, a₀)  ≤  3^{s·(Q.scale − k)} · 𝓔_{s,∞,2}(Q; a, a₀) ,

with the same coefficient family and comparator on both sides — which is exactly how the printed transport e.mathcalE.stability.applied uses the flux-corrected field ã_{L,n+2} and the comparator σ_{n+2} of the parent cube on the smaller cube as well.

For a one-scale descent and s ≤ 1 the factor is at most 3; the printed constant C(d)(1−2s)^{-1} is never needed in the grid case. This is the q = 2 sibling of CoarseGraining's Ch02.homogenizationErrorOnCube_infinity_one_le_of_mem_descendantsAtScale.

4. The composite the §4.3 chain uses

theorem Algsuperdiff.Section4.Provider.ExcessDecay.homogenizationErrorOnCube_infinity_two_descendant_index_le {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {t u : ℝ} (ht : 0 < t) (htu : t ≤ u) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube R u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ≤ Real.rpow 3 (t * ↑(Q.scale - k).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0

The two moves composed, in the order the §4.3 chain performs them.

From a cap at the parent cube Q and the small index t, one reads off the same cap at every triadic descendant R and every larger index u, at the single cost 3^{t·(Q.scale − k)}:

𝓔_{u,∞,2}(R; a, a₀)  ≤  3^{t·(Q.scale − k)} · 𝓔_{t,∞,2}(Q; a, a₀)   (t ≤ u).