LocalizationCutoffMesh #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the localization split at the actual cutoff coefficient, mesh-averaged #
Source displays in ABK26:
e.recurrence.params: the two scale gatesK >= m + 10^10 gamma^{-1}andn:= m - h - 16 ceil|log_3 gamma|;e.recurrence.P.def,e.def.w,e.Pz.def,e.Fz.def;- the gluing sentence "Observe that
X_z = S_z + tilde S_z. Since. we may insert it into the minimization problem ine.variational.mu.U.PforbfA_m(cu_K)"; e.variational.mu.U.P, the variational problem the glued field is inserted into.
LocalizationActualSplit.lean produces the per-cell fields S_z,
tilde S_z at the actual carriers but leaves the coefficient family abstract
and the mesh average absent. LocalizationGrid.lean supplies the mesh tiling
identity but at an arbitrary integrable function. This module composes the
two at the genuine cutoff coefficient: the global bfA_m(cu_K) and every
cell bfA_m(z+cu_n) are the same Cutoff.coefficientCutoffTriadicCoeffFamily
evaluated at cu_K and at each descendant cell, and the right-hand side is the
mesh average over the scale-n grid.
The coefficient compatibility that makes "simultaneously at cu_K and at #
each cell" true
Cutoff.coefficientCutoffTriadicCoeffFamily M m omega gives every triadic cube
the same literal coefficient field a_m = nu I + k_m; only the recorded upper
ellipticity constant varies with the cube, and blockMatrixField does not read
it. Hence the restriction of the family's representative from cu_K to a
descendant cell is an identity of functions, not an a.e. identity, and no
null set is spent. That is
toCoeffField_coefficientCutoffTriadicCoeffFamily_congr below and its two
consequences; they are what let the mesh step replace bfA_m(cu_K)'s
representative by bfA_m(z+cu_n)'s inside each cell integral. A caller working
with a general Ch02.TriadicCoeffFamily would have to spend
Ch02.pointwiseCoeffOnRestrict and an a.e. argument instead; at the actual
cutoff coefficient neither is needed.
What is proved #
toCoeffField_coefficientCutoffTriadicCoeffFamily_congr,blockMatrixField_coefficientCutoffTriadicCoeffFamily_congr,blockEnergyDensityAt_coefficientCutoffTriadicCoeffFamily_congr-- the compatibility layer just described, at the level of the coefficient field, of the doubled matrix field, and of the doubled energy density.two_mul_doubledMuValue_gluedDoubledField_eq_mesoGridAverage-- the mesh step: for the actual cutoff coefficient,fint_{cu_K} X. bfA_m X = avsum_{z in 3^n Zd cap cu_K} fint_{z+cu_n} X_z. bfA_m X_zwhenXis the glued field of the cell fieldsX_z. The tiling constant is1.exists_localizationCutoffCellSplit_blockVecDot_coarseBlockMatrix_le-- the frozen pre-mesh intermediate ofLocalizationActualSplit.leaninstantiated at the actual coefficient family,a := (...).coeffOn QandaCell R:= (.).coeffOn R, with the glued field's membership inP + L^2_{pot,0}(cu_K) x Lsolo(cu_K)carried in the conclusion.exists_localizationCutoffMeshSplit_le_mesoGridAverage-- the first line ofe.lower.bound.basic.splitat the actual coefficients, at the actual carriers, at the recurrence scales, mesh-averaged.exists_localizationCutoffMeshSplit_le_mesoGridAverage_expanded-- the same bound with the cell energy replaced by the manuscript's third line, i.e.P_z. bfA_m(z+cu_n) P_z + 2 P_z. fint bfA_m tilde S_z + fint tilde S_z. bfA_m tilde S_z, mesh-averaged.
Which printed lines are proved here, and which are not #
Proved here (as conditional helper statements, with the binders listed in each
docstring): the inequalities, both mesh-averaged over the full scale-n grid,
both at bfA_m on cu_K and on every cell. The passage between them runs
through inside LocalizationBasicSplit.doubledMuValue_add; the intermediate
line is therefore used, and no declaration below states it as a separate
mesh-averaged display.
NOT proved here, and not claimed: any estimate on S_z, on tilde S_z, on
bfF_z or on the correctors; the expectation (Step 2); the reverse of the
insertion inequality.
Divergences from the printed statement #
- . Only the inequality direction of the insertion is produced.
- . The site set
3^n Z^d cap cu_KismesoCubeGrid d K n, the finite family of scale-ntriadic descendants ofcu_K, indexed by cubes rather than by corner points. On this family the tiling identity holds at constant1, which is what the mesh step below uses. - The line composed below is the full-grid leg, where
LocalizationGrid.cubeAverage_originCube_eq_mesoGridAverageapplies exactly and no deficit is incurred. likewise bears on the interior/full mismatch of a different average and is not consumed below. - : the gap multiplier stays free. The meso scale is
recurrenceMesoScale a gamma m hat a freea: Nat; the printed16is nowhere written, and noa >= 28gate is assumed, because the mesh step needs onlyn <= K. - The
Kgate is carried, not derived.hKbelow is the printed `K >= m- 10^10 gamma^{-1}
. Only its consequencem <= Kis used; nothing here derives the gate frome.cgamma.constraints`.
- 10^10 gamma^{-1}
- . Carrier and totalization conventions are inherited unchanged from
LocalizationSelectionExistence.leanandLocalizationGluingAdmissible.lean:SandTare total functions onTriadicCube dand every conclusion is quantified over the grid, the values off it being neither used nor mentioned. - The factor two. As in
LocalizationBasicSplit.lean, the manuscript'sfint_U X . bfA Xis twice CoarseGraining'sdoubledMuValue; the factor is carried explicitly and neither object is renormalized. - The scale pair.
highScaleis the manuscript'smandlowScaleism - h:Corrector.streamForcing sigmaInv omega lowScale highScale eis the forcingshom_{m-h}^{-1}(k_m - k_{m-h}) eofe.def.w. The coefficient family is therefore taken athighScale, which isbfA_m, and the meso scale atm = highScale,h = highScale - lowScale. - One sample drives both sides.
omega : Cutoff.CutoffSample dsupplies the coefficientbfA_mand, through its underlying shell sequence, the correctors andbfF_z; no second, unrelated sample appears.
The coefficient compatibility layer #
The actual cutoff coefficient is one field, shared by every cube. The
representative of Cutoff.coefficientCutoffTriadicCoeffFamily M m omega on Q
and its representative on R are the same function a_m = nu I + k_m; the
family's cube dependence lives entirely in the recorded upper ellipticity
constant, which no statement below reads. Unconditional.
The doubled matrix field of the actual cutoff coefficient is cube-free.
bfA_m computed on cu_K and bfA_m computed on a cell agree as functions on
all of space, because blockMatrixField reads only toCoeffField.
Unconditional.
The doubled energy density of the actual cutoff coefficient is cube-free.
This is the pointwise identity the mesh step consumes: inside a cell the
integrand X . bfA_m X may be read at the cell's own representative of bfA_m
without changing its value, at every point and not merely a.e.
Unconditional.
Two elementary facts about the grid average #
The mesh step #
The descendant mesh average of the glued energy, at the actual cutoff coefficient.
fint_{cu_K} X . bfA_m X
= avsum_{z in 3^n Zd cap cu_K} fint_{z+cu_n} X_z . bfA_m X_z ,
X = sum_z X_z 1_{z+cu_n} .
Two ingredients meet here. The tiling identity
LocalizationGrid.cubeAverage_originCube_eq_mesoGridAverage splits the average
over cu_K into the average of the cell averages at tiling constant 1; inside
each cell the glued field is the cell field
(LocalizationGluingAdmissible.gluedDoubledField_eval_of_mem_openCubeSet) and
bfA_m(cu_K)'s representative is bfA_m(z+cu_n)'s
(blockEnergyDensityAt_coefficientCutoffTriadicCoeffFamily_congr), so each cell
average is exactly the cell's own doubled energy. The factor 2 is
LocalizationBasicSplit.lean's normalization convention.
: on hn : n <= K and on the two MemVectorL2 memberships of the glued field
on cu_K, which supply the integrability the tiling identity consumes. Both
memberships are discharged from the gluing admissibility at the call site below
and are not manuscript premises.
The pre-mesh intermediate at the actual coefficient #
The frozen pre-mesh intermediate of LocalizationActualSplit.lean,
instantiated at the actual cutoff coefficient on the cube and on every cell.
a and aCell are no longer free: both are
Cutoff.coefficientCutoffTriadicCoeffFamily M highScale omega, the
development's rendering of bfA_m, evaluated at Q and at each descendant
cell respectively. The one sample omega supplies the coefficient and,
through its underlying shell sequence, P_z, bfF_z and the correctors of
e.def.w.
The conclusion additionally carries the membership assertion, sum_z X_z 1_{z+cu_n} in P + L^2_{pot,0}(cu_K) x Lsolo(cu_K), which is derived here
from isDoubledMuAdmissible_localizationBackground and the cell minimality,
not assumed; the mesh step consumes it for the integrability of the glued
energy density.
Per only the inequality direction is available.
: on hwN, the defining property of w_{N,e'}^{(K)}.
The recurrence scales #
The meso scale of e.recurrence.params at the recurrence's own scale pair.
With highScale = m and lowScale = m - h -- the two endpoints of the fresh
shell h = k_m - k_{m-h} carried by Corrector.streamForcing -- this is n = m - h - a ceil|log_3 gamma| at a free multiplier a (; the printed 16
is nowhere written).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The meso scale never exceeds m - h = lowScale. This is
LocalizationParams.recurrenceMesoScale_le at the recurrence's scale pair;
nothing about the multiplier a or about gamma is used. Unconditional.
The meso scale sits below the big scale K. The printed gate is K >= m + 10^10 gamma^{-1}; only its consequence m <= K is used, together with h >= 0.: on hgamma0, hlow and hK, all caller-supplied; nothing here derives
hK from e.cgamma.constraints.
The first line of e.lower.bound.basic.split, at the actual coefficients, at
the actual carriers, at the recurrence scales, mesh-averaged.
P . bfA_m(cu_K) P <= avsum_{z in 3^n Zd cap cu_K} fint_{z+cu_n} X_z . bfA_m X_z ,
X_z = S_z + tilde S_z , P = bfAhom_{m-h}^{-1/2}(e'; e) .
Every object is the manuscript's own: P is e.recurrence.P.def, the big cube
is cu_K at the scale, the site set is 3^n Z^d cap cu_K at the meso scale,
S_z is the constant-load minimizer at P_z of e.Pz.def, tilde S_z is the
minimizer over bfF_z + (L^2_{pot,0} x Lsolo)(z+cu_n) of e.Fz.def, and
bfA_m is Cutoff.coefficientCutoffTriadicCoeffFamily M highScale omega on
the cube and on every cell simultaneously. The tiling constant of the mesh
average is 1.
Per this direction, and only this direction, is available.
: on hwN, the defining property of w_{N,e'}^{(K)}, and on the three scale
binders hgamma0, hlow (h >= 0) and hK.
The third line of e.lower.bound.basic.split, at the actual coefficients, at
the actual carriers, at the recurrence scales, mesh-averaged.
P . bfA_m(cu_K) P
<= avsum_{z in 3^n Zd cap cu_K} ( 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 passage from the previous statement runs cell by cell through
LocalizationActualSplit.two_mul_doubledMuValue_localizationActual_add_eq,
whose own route is the quadratic expansion followed by the Euler--Lagrange
collapse of the cross term; the intermediate printed line is therefore used,
and is not restated here as a separate display. All three occurrences of
bfA_m on the right are the cell's representative of the same cutoff family
whose cu_K representative appears on the left.
Per this direction, and only this direction, is available. No estimate on
P_z, on tilde S_z or on bfF_z is asserted; bounding the two fluctuation
terms is Step 2 of the manuscript and is not attempted here.
: identical to the previous statement -- hwN and the three scale binders
hgamma0, hlow, hK.