ErrorSwitch #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Subadditivity of ๐ at the exponent pair (2,2): lifting the domain scale #
ABK26, ยง4.1, e.mathcalE.squared.max.bound. Step 1 of
l.ratio.of.good.scales.for.mathcal.E cites, verbatim,
By Proposition
p.induction.bounds, subadditivity of๐,e.powerofGammasigmaande.maxy.boundโฆ
This module supplies the second of those four inputs, in the only form in which it is true: at the finite spatial exponent.
The statement #
For every triadic cube Q, coefficient family F and comparator aโ,
๐_{s,2,2}(Q; F, aโ)ยฒ โค 3 ยท max_{R โ descendantsAtScale Q (Q.scale โ 2)}
๐_{s,โ,2}(R; F, aโ)ยฒ .
The offset 2 is the one the ๐ขโ atom needs; nothing in the argument is
special to it.
Why the finite spatial exponent #
At p = 2 the shells are descendant averages, and averages factor through an
intermediate generation exactly, descendantsAverage Q (2+k) = descendantsAverage Q 2 (descendantsAverage ยท k) (CoarseGraining's
descendantsAverage_add_eq_descendantsAverage_descendantsAverage), so the
finite average commutes with the infinite shell sum and no cardinality is paid.
This is the structural reason the manuscript's X_j is built from ๐_{s,2,2}
rather than from ๐_{s,โ,2}.
Only the two shallowest shells (l = 0, 1) need e.subaddJ.nosymm itself;
they are discharged by the proved average form
normalizedBlockResponseMax_le_descendantsAverage, which is exponent-free.
Main results #
finsetAverageReal_descendantsAtScale_eq_descendantsAverageโ the shell bridge between the(2,2)identity's scale indexing and CoarseGraining's depth indexing.homogenizationErrorOnCube_two_two_sq_le_infinity_two_sqโ descendant average below descendant supremum, at a fixed cube.homogenizationErrorOnCube_two_two_sq_le_descendant_supโ the domain lift.homogenizationErrorOnCube_two_two_le_sqrt_three_mulโ its square-root form against a uniform bound on the descendants.
Scope #
Deterministic Provider material: proved local helpers, carrier-generic in F
and aโ.
References #
- ABK26,
d.mathcal.E,e.subaddJ.nosymm,e.mathcalE.squared.max.bound.
The shell bridge #
The (2,2) squared identity indexes its shells by descendantsAtScale Q (Q.scale โ l); CoarseGraining's iterated-average calculus indexes them by
depth. The two agree.
Nonnegativity of the two gauges #
The (2,2) error is nonnegative.
The (โ,2) error is nonnegative.
The shells of the (2,2) square #
The l-th shell of ๐_{s,2,2}(Q)ยฒ: the depth-l descendant average of the
normalized block-response maxima.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(2,2) below (โ,2) at a fixed cube #
The descendant average sits below the descendant supremum, shell by shell. Both series converge โ the shared witness is the one-cube uniform response bound โ so the comparison survives the infinite sum.
The two shallow shells #
The deep shells #
The domain lift #
Subadditivity of ๐ at (2,2), two triadic scales up. The manuscript's
"subadditivity of ๐", read in the direction it is used there: the functional
on Q is controlled by the functionals on the descendants of Q two scales
down, at a purely numerical cost.
The right-hand side is read at the endpoint spatial exponent, which is the exponent the Section 3 anchor supplies.
The square-root form: a uniform bound B on the (โ,2) errors of the
depth-2 descendants bounds the (2,2) error of Q by โ3 ยท B.