LocalizationFluctuationSplitOscEnvelope #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hE: the eighth-moment grid envelope of the oscillation cells #
LocalizationOscillationFullMesh and its Neumann mirror
LocalizationFluctuationNumericNeumannMesh carry two e.nablaw.in.L.eight
side conditions into the Step-5 shape:
hmem8, theL^2-in-the-sample membership of the fourth powers of the oscillation cells --- discharged byLocalizationFluctuationNumericOctic.exists_gamma0_memLp_two_freshShell{Dirichlet, Neumann}_meshOscillationCell_rpow_four;hE, an envelope for their eighth-moment grid average, i.e. a realEwithavsum_{z in 3^n Zd cap cu_K} E[ osc(z + cu_n; grad w_omega)^8 ] <= E ,Ebeing quantified before the model, so that the threshold the full-mesh endpoint produces from it is uniform.
This module discharges hE, and re-exports hmem8 alongside it so that a
consumer of the full-mesh endpoint obtains both side conditions from a single
call under a single threshold.
Method #
Nothing new is estimated. Two proved pieces are composed.
LocalizationFluctuationGridEighth.cubeFamilyAverage_integral_meshOscillationCell_pow_eight_lebounds the eighth-moment grid average by the expectation of any observableGdominating the cube averagefint_{cu_K} |u|^8pathwise. TakingGto be that cube average itself, the hypothesis isle_rfland the remaining work is a bound onE[G].Gis measurable byCorrector.CorrectorMeasurableOctic, and it equals the fourth power of‖u‖^2_{L8bar(cu_K)}, whiche.nablaw.in.L.eightbounds byChead + TfluctwithTfluct = O_{Gamma_1}(gamma^100). The producedTfluctis not known to be measurable, so theT'device ofLocalizationFluctuationNumericOctic.memLp_two_meshOscillationCell_rpow_four_of_measurableis reused verbatim:T' := max ((G)^{1/4} - Chead, 0)is measurable, is dominated byTfluct(hence inherits itsGamma_1tail), and still dominatesG^{1/4} - Chead. ThenLocalizationFluctuationGridEighth.integral_le_freshShellEighthEnergyConstgivesE[G] <= freshShellEighthEnergyConst Chead (gamma^100).The amplitude is finally released:
freshShellEighthEnergyConstis monotone in its second argument andgamma^100 <= 1, so the model-independent constantfreshShellEighthEnergyConst Chead 1serves for every admissible model. This is what letsEbe quantified beforeM.
The consumers' hE is stated at the real exponent ^ (8 : ℝ) while the grid
composition is stated at ^ (8 : ℕ); rpow_eight_eq_pow_eight converts.
Main results #
rpow_eight_eq_pow_eight,freshShellEighthEnergyConst_mono_right--- the two pieces of bookkeeping.cubeFamilyAverage_integral_meshOscillationCell_pow_eight_le_freshShellEighthEnergyConst--- the generic core, for an arbitrary sample family with ane.nablaw.in.L.eight-shaped pathwise bound.exists_freshShellDirichlet_meshOscillation_memLp_and_eighthMoment_leand its Neumann mirror ---hmem8andhEtogether, as theorems, withEproduced before the model.
Binders #
Beyond the typing binders: hd : 2 <= d; under the leading quantifiers the
model gate M.gamma <= gamma0, the induction state, the four gates of
e.recurrence.params and the two direction bounds; then the caller's family of
weak solutions of e.def.w (hsol) and the six spatial single-sample
families on cu_K (the L^8 membership hmem and the five integrabilities it
implies); and finally the mesh index bound n <= K, which only names the mesh.
No hypothesis about the sample space survives; no measurability or selection
property of the corrector family is assumed; and no smallness or normalization
is assumed --- both E and the threshold are produced.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
e.def.w,e.nablaw.oscillations,e.nablaw.in.L.eight,e.lower.bound.oscillations,e.recurrence.params.
Two pieces of bookkeeping #
The eighth-energy envelope constant is monotone in the fluctuation
amplitude. This is what releases the model-dependent amplitude gamma^100 and
produces a constant uniform in the model.
The generic core #
The eighth-moment grid envelope, from an e.nablaw.in.L.eight-shaped
pathwise bound.
For any sample family u whose normalized Euclidean L^8 norm on cu_K obeys
‖u‖^2 <= Chead + T pathwise with T a nonnegative O_{Gamma_1}(A) variable,
the eighth-moment grid average of the oscillation cells of
e.nablaw.oscillations over 3^n Zd cap cu_K is below
freshShellEighthEnergyConst Chead A.
T is not assumed measurable: it enters only through the measurable
dominator T' = max((fint_{cu_K}|u|^8)^{1/4} - Chead, 0), which is built from
the measurable cube observable hglobMeas and inherits the Gamma_1 tail by
IsBigOWith.of_le.
: complete binder census beyond the typing binders d, Omega, its MeasurableSpace instance, mu, K, n, u, Chead, A, T: [IsProbabilityMeasure mu]; the mesh index bound hn; hChead, hA; hT0, hT (the Gamma_1
tail); hmem, hpath (the spatial L^8 membership and the pathwise L^8
bound); the five spatial integrability families on cu_K; hcellInt (the
integrability in the sample of the per-cell eighth powers); and hglobMeas
(measurability in the sample of the cube's eighth energy). No estimate on the
oscillation is used.
The two wired consumers #
hmem8 and hE for the Dirichlet corrector of e.def.w, as theorems.
One constant E, produced before the model, and one explicit threshold
gamma0, such that in the whole parameter range of e.recurrence.params and
for every sample family of zero-trace weak solutions of e.def.w obeying the
six spatial families on cu_K, both e.nablaw.in.L.eight side conditions of
LocalizationOscillationFullMesh hold at every mesh scale n <= K.
Reaches exactly the external anchor
Algsuperdiff.Frozen.External.calderon_zygmund, a proved external,
inherited from exists_freshShell_cubeEuclideanL8_leg_bound.