SplitObligationsBackground #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Obligation (2) of SplitScaleObligations, reduced to two cell-energy moments #
ABK26, l.approximate.recurrence.formula, Step 2, e.Pz.def, e.Fz.def, the
background display.
What this module supplies #
Closure.SplitProducerFold.SplitScaleObligations's second conjunct, per
mesoscopic cell:
omega |-> mu( a_omega; P_z + bfF_z ) is integrable under cutoffSampleLaw M .
doubledMuValue U a F is the normalized average over U of the pointwise
doubled energy density (1/2) F(x) . bfA(x) F(x). Two unconditional facts
about that average are proved here:
doubledMuValue_le_plainUpperBound--- the density is a.e. below the plain elliptic upper bound of its carrier, and that bound is integrable as soon as the two legs ofFare vector-L^2onU, soMeasureTheory.integral_mono_of_nonneggives
mu( a; F ) <= (1/2)(Lam + 2 lam^{-1} Lam^2) fint_U |F_pot|^2
+ lam^{-1} fint_U |F_flux|^2 .
At the genuine cutoff cell lam = M.nu and Lam = Cutoff.coefficientCutoffCubeEllipticityUpper M (n+h) omega R, whose every
finite moment is proved. Combining, obligation (2) reduces to exactly two
sample moments of the background's own normalized cell energies:
- the second moment of the potential leg's cell energy (it multiplies
Lam^2), and - the first moment of the flux leg's cell energy (it multiplies the
deterministic
M.nu^{-1}).
integrable_doubledMuValue_meshCellBackground_of_cellMoments is that
reduction. The measurability half is the proved
LocalizationFluctuationBackgroundClass.measurable_doubledMuValue_meshCellBackground,
and the two typing properties are the proved
memVectorL2_meshCellBackground_{potential,flux}.
What is not proved here. The two moment binders themselves.
Binders #
Beyond the typing binders: [NeZero d], the two MeasurableSpace/BorelSpace
pairs on the doubled L^2 carriers, the geometric membership of the cell in the
mesh below the localization cube, the two weak-solution properties of e.def.w,
and the two named cell-energy moments. No smallness, no ellipticity gate and no
selection occurs.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formula, Step 2,e.Pz.def,e.Fz.def, the background display,e.CG.bounds.2.
The doubled energy value of a fixed field #
The doubled energy of any field is nonnegative. The pointwise density is
a.e. nonnegative by CoeffOn.aeElliptic and CoarseGraining's pointwise
coercivity, and the normalized average of an a.e. nonnegative function is
nonnegative even when the function is not known to be integrable.
Unconditional.
The doubled energy of a vector-L^2 field is below the plain elliptic
upper bound of its carrier.
The pointwise density is bounded a.e. by CoarseGraining's
blockMatrixOfCoeff_quadratic_plainUpperBound_of_isEllipticMatrix, whose right
side is integrable because both legs are vector-L^2; the value itself is not
assumed integrable, MeasureTheory.integral_mono_of_nonneg needing only a.e.
nonnegativity on the left.
only on the two L^2 typing properties.
The two named cell energies of the Step-2 background #
The normalized cell energy of the background's potential leg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The normalized cell energy of the background's flux leg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two cell energies in closed form #
The two moment binders below are therefore exactly second- and first-moment
statements about the normalized cell energies of the two corrector legs of
e.def.w, up to the fixed gauge factors shom^{-1} and shom.
The potential leg's cell energy is shom^{-1} times the normalized cell
energy of e' + grad w_D. Unconditional.
The flux leg's cell energy is shom times the normalized cell energy of
e + (grad w_N + shom^{-1} h e'). Unconditional.
Obligation (2), reduced #
Obligation (2) of SplitScaleObligations at one cell, from two cell-energy
moments.
No estimate of the manuscript is used, and no competitor is selected.