LocalizationFluctuationStationarity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The stationarity half #
- geometric -- state the per-cell bound at the cell's own scale-
mancestor. This isLocalizationFluctuationAncestor, proved; - probabilistic -- transport the annealed fourth moment from that ancestor
back to
cu_mby stationarity, "which the manuscript uses silently".
This module performs step 2.
The route #
Every scale-m triadic cube is an integer translate of cu_m
(eq_translateCube_originCube_of_scale), and the cutoff-sample law is
invariant under every real translation
(Cutoff.map_translateCutoffSample_cutoffSampleLaw,
Cutoff.coefficientCutoffLaw_stationary_real). What is missing between those
two facts is the per-cube covariance of the coarse matrices of the actual
cutoff family: CoarseGraining's
Ch02.LambdaSq_translateCube_of_coarseBMatrixNormandCh02.lambdaSq_translateCube_of_coarseSigmaStarInvMatrixNorm
reduce the covariance of the two multiscale ellipticity constants to exactly the per-cube identities
|b(3^n z + R; a_omega)| = |b(R; a_{tau_v omega})| ,
|sigma_*^{-1}(3^n z + R; a_omega)| = |sigma_*^{-1}(R; a_{tau_v omega})| ,
for every descendant R of cu_m at depth n, where v = 3^m z is the
physical shift and a_omega = coefficientCutoffTriadicCoeffFamily M L omega.
coarseBlockMatrix_coefficientCutoff_translateCube proves both at once, at the
level of the coarse block matrix, by the chain
A(cu(3^n z + R); a_omega) = A(open(3^n z + R); cutoff_omega) (Ch02 = CoarseGraining)
= A(v + open(R); cutoff_omega) (geometry)
= A(open(R); translate_v cutoff_omega) (translation)
= A(open(R); cutoff_{tau_v omega}) (Cutoff.Symmetry)
= A(cu(R); a_{tau_v omega}) .
Note that the physical shift 3^n z * 3^{m-n} = 3^m z is the same at every
depth n, which is precisely what the CoarseGraining hypothesis needs.
What is proved #
openCubeSet_translateCube_eq_translateSet-- the geometry step.coarseBlockMatrix_cubeDomain_eq_coarseBlockMatrix_openCubeSet-- the identification of the Chapter-2 coarse block matrix of a cube coefficient object with the CoarseGraining coarse block matrix of its underlying field. This iscoarseBlockMatrix_cubeSet_eq_ch02_coarseBlockMatrix_of_aelocallyUniformlyEllipticFieldwith the a.e.-elliptic-field packaging stripped out; the cutoff family is not built through that packaging.coarseBlockMatrix_coefficientCutoff_translateCube, and the two norm corollariescoarseBMatrixNorm_coefficientCutoff_translateCubeandcoarseSigmaStarInvMatrixNorm_coefficientCutoff_translateCube-- the missing link.gaugedEllipticitySum_translateCube_coefficientCutoffandgaugedEllipticitySum_scale_eq_originCube-- the pathwise covariance of the gauged ellipticity sum.integral_gaugedEllipticitySum_pow_eq_originCubeandintegral_gaugedEllipticitySum_pow_ancestorAtScale_eq_originCube-- the transport: the annealed fourth moment of the gauged ellipticity sum at a cell's scale-mancestor equals the one atcu_m, where the frozenFrozen.Section3.coarse_ellipticity_boundslives.
Binders #
Everything through gaugedEllipticitySum_scale_eq_originCube is pathwise and
unconditional apart from the typing binders and the cube-scale identification
hT : T.scale = m; no measure, no model gate and no moment occurs. The two
transport statements add one binder, hmeas, the a.e.-strong measurability in
the sample of the observable being integrated -- the analytic side condition of
the change of variables, on the very object the moment is formed from. It is
not a smallness, normalization or moment assumption, and it is stated at the
origin cube, i.e. at the carrier the frozen theorem already speaks about.
Scope #
There is no sorry.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2, display and the moment average.
Geometry: the open realization of a translated cube #
Unconditional. The open realization of translateCube w S is the
translate of the open realization of S by the physical shift
w * 3^{S.scale}.
Unconditional. Every scale-m triadic cube is the integer translate of
cu_m by its own index.
The two coarse block matrices agree #
Unconditional. The Chapter-2 coarse block matrix of a cube coefficient object is the CoarseGraining coarse block matrix of its underlying coefficient field on the open cube.
This is the content of
coarseBlockMatrix_cubeSet_eq_ch02_coarseBlockMatrix_of_aelocallyUniformlyEllipticField
without its A packaging: the cutoff family is not built through triadicCoeffFamilyOfA, so that statement does not apply to it.
The missing link: per-cube covariance of the cutoff coarse matrices #
The per-cube covariance of the coarse block matrix of the actual cutoff
family. Translating the cube by w and translating the sample by the
physical shift w * 3^{S.scale} produce the same coarse block matrix.
Unconditional: the only inputs are the geometry step, CoarseGraining's
translation identity for coarseBlockMatrix and the exact commutation
Cutoff.coefficientCutoff_translateCutoffSample.
The upper per-cube norm is covariant. This is the exact hypothesis of
CoarseGraining's Ch02.LambdaSq_translateCube_of_coarseBMatrixNorm.
The lower per-cube norm is covariant. This is the exact hypothesis of
CoarseGraining's Ch02.lambdaSq_translateCube_of_coarseSigmaStarInvMatrixNorm.
The physical shift does not move with the depth #
Unconditional. A depth-n descendant of a cube of scale m, translated
by descendantTranslationShift n z, moves by the physical shift 3^m z, which
does not depend on n.
The gauged ellipticity sum is covariant #
The pathwise covariance of the gauged ellipticity sum. Unconditional.
The pathwise covariance, at an arbitrary scale-m cube. Unconditional
apart from the scale identification hT.
The change of variables in the sample #
The translation change of variables on the cutoff-sample law.
Conditional on hg, the a.e.-strong measurability of the integrand -- the analytic side
condition of the change of variables.
The transport #
The stationarity half. The annealed fourth moment of the gauged
ellipticity sum at any scale-m cube equals the one at cu_m, where
Frozen.Section3.coarse_ellipticity_bounds lives.
Conditional on the scale identification hT and on hmeas, the a.e.-strong measurability
in the sample of the observable at the origin cube. Nothing about the
model, the gauge or the exponent is assumed.
The transport at the ancestor carrier of LocalizationFluctuationAncestor.
The annealed fourth moment of the gauged ellipticity sum at a mesoscopic cell's
own scale-m ancestor is the one at cu_m. Together with
LocalizationFluctuationAncestor.doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor
this closes the carrier mismatch.
Conditional on hm : R.scale <= m (the ancestor exists) and on hmeas.