LocalizationRecurrenceMesh #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The localized variational test at the recurrence carriers #
ABK26, l.approximate.recurrence.formula (statement), Step 1, the display
e.lower.bound.basic.split.
LocalizationCutoffMesh.lean proves the insertion inequality and its quadratic
expansion at the actual cutoff coefficient family, on the mesh
mesoCubeGrid d K (cutoffMesoScale a gamma lowScale highScale), at abstract
sigma, lowScale, highScale, gapMultiplier and gamma. This module
reads that statement at the recurrence's own data --
sigma := Annealed.sigmaBar M (m - h), the manuscript'sshom_{m-h};lowScale := m - handhighScale := m, the two endpoints of the fresh shellbfh = k_m - k_{m-h};gapMultiplier := recurrenceGapMultiplier = 32, the proof-internal multiplier; the printed16ofe.recurrence.paramsis nowhere used;gamma := M.gamma;- the big cube
originCube d Kcat the gate10^10 gamma^{-1} <= Kc - m
-- and converts the grid average into the descendantsAverage form at the
depth j fixed by (originCube d Kc).scale - j = recurrenceMesoScale 32 gamma m h.
That is exactly the carrier convention of
exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit,
whose conclusion bounds the descendantsAverage of the first summand
produced here. The two statements are therefore composable at one and the same
corrector pair: the terminal produces a corrector family and this module's
principal statement consumes a corrector pair, so a caller may specialize the
family at a sample and feed it here.
What is proved #
localizationRecurrenceMesoScale_eq-- the scale identitycutoffMesoScale a gamma (m - h) m = recurrenceMesoScale a gamma m h.mesoCubeGrid_recurrenceMesoScale_eq_descendantsAtDepth-- the mesh at the recurrence buffer is the depth-jdescendant family ofcu_{Kc}.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded-- the third line ofe.lower.bound.basic.splitat the recurrence carriers, indescendantsAverageform: the localized variational test, with its principal term and its two fluctuation terms displayed separately. The two correctors ofe.def.ware assumed, not produced.
References #
The recurrence geometry: buffer scale, mesh, descendant depth #
The buffer scale of e.recurrence.params read at the recurrence's own scale
pair. With lowScale = m - h and highScale = m, cutoffMesoScale is
literally recurrenceMesoScale ... m h, i.e. n = m - h - a ceil|log_3 gamma|. Unconditional.
The mesoscopic tiling is the descendant family of the manuscript's depth.
The site set 3^n Z^d cap cu_{Kc} at the buffer scale n = recurrenceMesoScale a gamma m h is descendantsAtDepth (originCube d Kc) j exactly when j is
the depth named by (originCube d Kc).scale - j = recurrenceMesoScale a gamma m h.
: on hscale, which only names j, and on hn, the containment of the
buffer scale below Kc.
The localized variational test #
The third line of e.lower.bound.basic.split at the recurrence carriers, in
descendantsAverage form: the localized variational test.
P . bfA_m(cu_{Kc}) P
<= avsum_{z in 3^n Zd cap cu_{Kc}}
( P_z . bfA_m(z+cu_n) P_z
+ 2 P_z . fint_{z+cu_n} bfA_m tilde S_z
+ fint_{z+cu_n} tilde S_z . bfA_m tilde S_z ) .
The first summand is the principal term of Step 3; the latter two are the fluctuation contribution of Step 2. No estimate on either is asserted here.
The descendantsAverage carrier, the sigmaBar gauge, the shell pair
(m - h, m) and the depth identity are the same as those of
exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit,
so a caller holding both may add them cube by cube.
: identical to the previous statement.