GammaTenAssemblyCell #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-2 cell integrand, bounded at one sample point #
ABK26, Step 2 of l.approximate.recurrence.formula, target
e.lower.bound.localization.terms.
The gap this module fills #
LocalizationFluctuationSelectEndpoint.fluctuationEnergyAverage --- the quantity
Step 2 must put below cgamma^{10} --- is the grid average of the sample
integral of
meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega
= fluct( z + cu_n , a_omega; P_z , bfF_z ) ,
the canonical fluctuation number of LocalizationFluctuationSelectValue, which
mentions no minimizer. The per-cube estimate that Step 2 rests on,
LocalizationFluctuationPerCube.perCube_localizationFluctuation_le, is instead
stated about a realization tilde S_z of the split's second argmin: its
left-hand side is 2 P_z . fint bfA tilde S_z + 2 mu(tilde S_z).
The two are reconciled exactly as
blockVecDot_recurrenceP_le_descendantsAverage_switch_add_fluctuation
reconciles them: at each sample point the proved split
LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded
produces a triple (S, T, response) on the whole grid, and
LocalizationFluctuationSelectValue.localizationFluctuationValue_eq_of_isDoubledMuMinimizerField
turns the canonical number into the realized pair. The existential is opened
inside the sample-pointwise statement, so no measurable selection is made and
nothing about S or T survives in the conclusion.
What is proved #
meshFluctuationCellIntegrand_le_of_besovEnvelope--- the per-cell, per-sample Step-2 bound:
withfluct_R(omega) <= 2 kappa Theta^2 | bfAhom^{1/2} P_z(omega) | Bg + ( kappa Theta Bg )^2 ,kappa = besovDualityConst R s,Theta = doubledPoincareEllipticityFactorat the sample's own coefficient family, andBgany pathwise envelope of the finite-depth positiveq = 2Besov seminorms of the gaugedbfF_zonR. All eight analytic side conditions of the per-cube bound are discharged fromClosure.GammaTenAssemblySide; none of them appears as a binder.meshFluctuationCellIntegrand_le_ancestor_fold_shape--- the same withTheta^2replaced by32 c_{s,2}^{-2}timesLocalizationFluctuationEllipticity.gaugedEllipticitySum, the latter read at the cell's own scale-(n+h)ancestor and at exponentcgamma, viaLocalizationFluctuationAncestor.doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor(the ancestor bridge, cost3^{22}). This is the shape in which the annealed Hoelder fold ofClosure.GammaTenGridFoldreads the ellipticity leg --- both summands are then linear in that sum --- and itsF-leg is literally the quantityLocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_lebounds, so it forcescgamma < s, hence a fixed Besov exponents.besovDualityConst_eq--- the pinned constant is cube-independent: the two Besov scale weights are reciprocal, sobesovDualityConst R s = 2 d 3^{d+s}for every cellR. This is what makes the two coefficients of the fold absolute rather than grid-dependent.
Binders #
The split's own binders (the large-cube gate, the depth-naming identity, and
the two weak formulations of e.def.w read along the sample), the
exponent/gauge windows 0 < s < 1, 0 < sigma_0, the cell membership hR,
and the pathwise envelope Bg with its two positive-seminorm bounds. No
measurability, no integrability, no moment and no smallness proposition occurs:
everything below is a pointwise inequality at one fixed sample point.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
The duality constant is cube-independent #
The pinned constant does not depend on the cell. besovDualityConst Q s
carries the product of the two Besov scale weights at exponents -s and s,
which is (3^{Q.scale})^{s} (3^{Q.scale})^{-s} = 1. Hence besovDualityConst Q s = 2 d 3^{d+s} on every triadic cube; this is why the two coefficients of
the Step-2 Hoelder fold are absolute constants and not grid-dependent weights.
The per-cell, per-sample Step-2 bound #
The Step-2 cell integrand at one sample point (at one mesoscopic cell).
fluct_R(omega) <= 2 kappa Theta^2 | bfAhom^{1/2} P_z | Bg + (kappa Theta Bg)^2 ,
kappa = besovDualityConst R s (cube-independent, besovDualityConst_eq),
Theta = doubledPoincareEllipticityFactor sig0 R a_omega s, and Bg any real
dominating every finite-depth positive q = 2 Besov seminorm of the two gauged
legs of bfF_z on R.
The left-hand side is verbatim
LocalizationFluctuationSelectEndpoint.meshFluctuationCellIntegrand, i.e. the
integrand of fluctuationEnergyAverage.
exactly on the binders listed in the module docstring: the split's own gates
and weak formulations, the exponent/gauge windows, the cell membership, and the
envelope. All eight analytic side conditions of
perCube_localizationFluctuation_le are discharged, not assumed.
The fold shape at the cell's own scale-(n+h) ancestor (after the ancestor
bridge).
This is the variant whose ellipticity leg is exactly the one the proved
moment producer bounds:
LocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_le
delivers E[ (gaugedEllipticitySum sigmabar (ancestorAtScale R m) cgamma a)^4 ] <= cgamma^{-8} at the ancestor ancestorAtScale R (n+h), at exponent
cgamma, whereas the per-cube bound is read at the cell R and at the Besov
exponent s.
LocalizationFluctuationAncestor.doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor
is the bridge, at the price of the absolute factor 3^{22}; it needs cgamma < s, so this route is read at a fixed s (any s with cgamma < s <= 1/2
works, e.g. s = 1/2), which is also what makes c_{s,2}^{-2} and hence c1,
c2 absolute constants.
The conclusion is again
fluct_R(omega) <= c1 * ( F_R G_R H_R ) + c2 * ( F_R H_R H_R )
with F_R = gaugedEllipticitySum sigma_0 (ancestorAtScale R (n+h)) cgamma a_omega.