StabilityExponentComparison

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

The q = 1 ← q = 2 comparison of the homogenization error

This module proves the manuscript's own scale-exponent comparison e.compareEqs (ABK26) at the endpoint pair (q, p) = (1, 2):

𝓔_{s,∞,1}(Q; a, a₀)  ≤  𝓔_{s/2,∞,2}(Q; a, a₀) ,          s > 0 ,

with no constant. The printed statement is 𝓔_{s,∞,q} ≤ 𝓔_{sq/p,∞,p} for 1 ≤ q ≤ p < ∞; only the pair the §4.3 chain uses is formalized here.

Why this matters for §4.3

The comparison is not missing from the manuscript: e.compareEqs, proved in Section 2 by Jensen's inequality immediately before l.lambdas.stability, supplies it — and it proves on the index s/8 rather than the printed s/6:

𝓔_{s/4,∞,1}(W)  ≤  𝓔_{s/8,∞,2}(W)          (this module, at `s := s/4`)

which is exactly the index at which the frozen annular anchor delivers its cap. So the printed intermediate rung 𝓔_{s/6,∞,2} is removable, and with it the only place where the §4.3 chain used l.lambdas.stability for an index/exponent change.

Recorded deviation from print: the printed first inequality of e.good.set.giveth.v2 (𝓔_{s/4,∞,1} ≤ C 𝓔_{s/6,∞,2} at the same cube) is not proved here and is not derivable from Jensen plus index monotonicity — the index s/6 is too large for the Jensen pairing and too small for antitonicity. It is true, by a weighted Cauchy--Schwarz with an absolute constant, but it is not needed: the route through s/8 reaches the same endpoint with constant 1.

The proof, in one line

Both sides are the same weighted series, because the weights agree:

w_{s,1}(l) = (1 − 3^{-s}) 3^{-sl} = w_{s/2,2}(l),
𝓔_{s,∞,1}   = ∑_l w_{s,1}(l) · Rₗ,        𝓔_{s/2,∞,2}² = ∑_l w_{s,1}(l) · Rₗ² ,

and ∑_l w_{s,1}(l) = 1. With A := 𝓔_{s/2,∞,2} the pointwise inequality 2 A Rₗ ≤ Rₗ² + A² (i.e. 0 ≤ (Rₗ − A)²) summed against the unit-mass weights gives ∑ w R ≤ (A² + A²)/(2A) = A. No Cauchy--Schwarz machinery is needed.

References

• ABK26, e.compareEqs, (statement, Jensen proof); its Λ/λ siblings e.compareLambdaqs.
• ABK26, e.good.set.giveth.v2.
• ABK26, d.mathcal.E.

1. The two series and their common weights

2. e.compareEqs at (q, p) = (1, 2)

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

The manuscript's e.compareEqs at the endpoint pair (q, p) = (1, 2).

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

Same cube, same coefficient family, same comparator, no constant: only the scale-exponent and the index move, and they move together (s ↦ s/2 when q = 1 ↦ 2), which is exactly Jensen's inequality for the unit-mass geometric weights.

At s := s/4 this reads 𝓔_{s/4,∞,1} ≤ 𝓔_{s/8,∞,2}, i.e. it converts the q = 1 quantity of the coarse-graining display e.homogenization.L2.interior into the q = 2 quantity at the annular anchor's own index s/8.