DeepLegSummability #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The shell-index monotonicity of the cutoff's ellipticity witness #
The cutoff local control is monotone in the shell index. Lowering the shell index deletes the leading terms of a nonnegative convergent series.
This is not
Provider.Diffusivity.ApproximateRecurrence.Closure.cutoffLocalControl_mono,
which is monotonicity in the scale ell at a fixed shell index and is proved
termwise from localCubeControl_mono; this one moves the other argument and is
a tail-truncation statement. The name is deliberately different so that a
consumer may open both.
The cutoff's entry envelope on a cube is nonnegative.
The cutoff's entry envelope on a cube is monotone in the shell index.
The cutoff's upper ellipticity constant is monotone in the shell index.
This is the moving comparator's only j-dependence inside
Ch02.normalizedBlockResponseUniformBound; the lower constant is the constant
M.nu.
The isotropic normalizer's row bound #
The row-absolute-square bound of a diagonal full block matrix.
The square-root normalizer of the isotropic comparator. At
a0 = sigma * 1 the Chapter 2 normalizer is the diagonal gauge
diag(sigma^{1/2}, sigma^{-1/2}), whose row bound is d (sigma + sigma^{-1}).
The inverse square-root normalizer of the isotropic comparator. Its row
bound is the same d (sigma + sigma^{-1}).
The plateau ceiling, uniform below a scale #
The annealed plateau, read uniformly below a scale. The upper plateau
bound of Provider.Base.annealedPlateau is increasing in the scale, so its
value at m bounds sigmaBar_k for every k <= m.
The ceiling is spelled with the constant
Provider.Base.cutoffPlateauAmplitude, whose
body is definitionally the plateau amplitude annealedPlateau displays: no
statement in this module spells that product by hand. The two side conditions
after the unfold (hpow, hcoef) are what the monotonicity step needs and are
not a re-spelling of the ceiling.
The uniform bound at the moving comparator #
The explicit form of CoarseGraining's uniform descendant bound: it is a
let-free restatement of Ch02.normalizedBlockResponseUniformBound.
The uniform descendant bound at the moving comparator. CoarseGraining's
Ch02.normalizedBlockResponseUniformBound at the cutoff family of shell index
k and the isotropic comparator sigmaBar_k is bounded by an explicit
expression in any upper bound L for the cutoff's cube ellipticity constant
and any upper bound T for sigmaBar_k + sigmaBar_k⁻¹.
** The uniform-in-j pathwise leg bound at the moving comparator.** For every
sample and every scale m and gap h, one constant bounds both breakdown legs
of every descendant of □_m, at the MOVING comparator (a_{m-j-h}, sigmaBar_{m-j-h}), uniformly in the depth j.
It is entirely deterministic: CoarseGraining's uniform descendant bound is
universally quantified in (a, a0), and the j-dependence of its explicit
value is controlled by the shell monotonicity of the cutoff's ellipticity
constant and by the annealed plateau.
(b) The two deep summability discharges #
The deep a-leg scale series is summable, pathwise. This is the first
Summable premise of localization_mathcalE_estimate_ae, at its exact
carriers.
The deep a^t-leg scale series is summable, pathwise. This is the
second Summable premise of localization_mathcalE_estimate_ae, at its exact
carriers.
(c) The endpoint, unconditional #
(c) l.localization.mathcalE, with both deep Summable premises
discharged. This is localization_mathcalE_estimate_ae with its TWO
conditional-A premises removed; every hypothesis that remains is a source
binder of the printed lemma or the parametric good-event constant Ccg. The
five-term display, the null-set placement and every constant are character
identical to the proved endpoint's; nothing here re-proves the analysis.