SplitFoldCellMoments #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two cell-energy moments hmom of the Step-1--3 split, produced #
ABK26, l.approximate.recurrence.formula, Steps 1--3, e.Fz.def, the
background display, e.def.w, e.nablaw.in.L.eight, e.km.kn.Lp.
What this module supplies #
Closure.SplitObligations.splitScaleObligations_integrability_of_regime carries
one analytic binder, hmom: for every mesoscopic cell of the closure mesh,
- the second sample moment of the Step-2 background's normalized potential
cell energy
meshCellBackgroundPotentialEnergy, and - the first sample moment of its flux cell energy
meshCellBackgroundFluxEnergy.
This module proves both, at the closure's own corrector families, inside the
manuscript's own regime, and therefore removes hmom: the export
splitScaleObligations_integrability_closureFamilies produces conjuncts (1) and
(2) of Closure.SplitProducerFold.SplitScaleObligations with no analytic binder
beyond Closure.ClosureRegime and the two direction bounds.
The two routes #
SplitObligationsBackground.meshCellBackgroundPotentialEnergy_eq and
..._FluxEnergy_eq put the two cell energies in the closed forms
E_pot = shom^{-1} fint_R |e' + grad w_D|^2 ,
E_flux = shom fint_R |e + (grad w_N + shom^{-1} (k_{n+h} - k_n) e')|^2 .
- Potential leg. Since
|e' + v|^2 <= 2|e'|^2 + 2|v|^2and the window identityopenCubeAtScale (triadicCubeShift R) R.scale = openCubeSet Ridentifiesfint_R |grad w_D|^2withmeshEnergyCell R.scale (grad w_D) R ^ 2(LocalizationFluctuationCellIntegrable.meshEnergyCell_rpow_four_eq_sq_volumeAverage), the square of the potential energy is dominated by the proved fourth-power producerexists_gamma0_integrable_freshShellDirichlet_meshEnergyCell_rpow_four. - Flux leg.
|e + grad w_N + F|^2 <= 2|e|^2 + 4|grad w_N|^2 + 4|F|^2. The middle term is the Neumann mirror of the same producer, read at its first moment; the forcing term is bounded byvolumeAverage_vecNormSq_streamForcing_le--- a cell-level Jensen step (L^2 <= L^8on the normalized cube) fed by the provedCorrector.cubeEuclideanLpNorm_streamForcing_le--- against the fourth moment of the fresh-shellL^8norm (Closure.Step5InputGradMoment.exists_integral_streamIncrementLpNorm_eight_pow_four_le, the proved frozen theoreme.km.kn.Lp).
The measurability halves of both legs are produced here by one generic device,
measurable_volumeAverage_vecNormSq_of_measurable_class: the window L^2
functional is 1-Lipschitz on L^2, so the normalized second energy over a
measurable window is a continuous functional of the sample's L^2 class, and
the two classes are the proved
measurable_toHilbertVectorL2OfVecField_freshShellDirichletGrad
and ..._neumannFluxField, shifted by a constant vector.
Binders #
splitScaleObligations_integrability_closureFamilies carries exactly
Closure.ClosureRegime at the produced threshold and the two direction bounds
|e| <= 1, |e'| <= 1. The large-cube gate, the depth-naming identity, the
cgamma-thresholds of the two producers and the spatial families of e.def.w
are all produced. No smallness, moment or measurability proposition survives.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formula, Steps 1--3,e.Fz.def, the background display,e.def.w,e.nablaw.in.L.eight,e.recurrence.params.
The window L^2 functional is Lipschitz on L^2 #
The L^2 size of an L^2 class over a window, read through the seminorm of
the restricted measure.
Equations
Instances For
The generic window second-energy observable #
The normalized second energy of a measurable family of vector L^2 classes
over a measurable window is measurable in the sample.
Unconditional apart from the window geometry and the measurability of the family of classes; no property of the underlying fields is used.
Adding a fixed vector to a measurable family of vector L^2 classes keeps the
family of classes measurable. Unconditional.
Small bridges #
The Chapter-2 average over a cell is the volume average over its open cube.
The volume average over the open cube is the cube average.
L^p integrability transports from the shell-sequence law to the cutoff
sample law along the sample inclusion. Unconditional.
A nonnegative random variable with an integrable square is integrable.
The volume average of a constant plus an integrable function.
The volume average of a constant multiple.
The regime's largeness gate is monotone in its threshold.
The L^8 spatial families of the closure's corrector families #
The closure's Dirichlet corrector gradient is L^8 on the localization cube.
Proved from memLp_eight_grad_freshShellDirichlet.
The mean-zero Neumann mirror.
The cell L^2 average of the forcing of e.def.w #
The cell second energy of the forcing of e.def.w, against the fresh-shell
L^8 norm.
On any cell of the localization cube, fint_R |shom^{-1} (k_m - k_n) e'|^2 is at
most a purely geometric ratio times (shom^{-1} ||k_m - k_n||_{L^8bar(cu_l)})^2:
the window integral is below the cube integral, and on the normalized cube
measure --- a probability measure --- the L^2 norm is below the L^8 one.
only on the geometry hsub, the sign of the gauge and the direction bound.
Anchor-free.
The potential leg's second moment #
The second sample moment of the Step-2 background's potential cell energy, from the fourth-power cell energy of the Dirichlet corrector.
exactly on the geometric membership of the cell and on hcell, the proved
producer read at the closure's own Dirichlet family.
The flux leg's first moment #
The first sample moment of the Step-2 background's flux cell energy, from
the fourth-power cell energy of the Neumann corrector and the second moment of
the fresh-shell L^8 norm.
exactly on the geometric membership of the cell, the direction bound |e'| <= 1, and the two named legs.