GammaTenFluxMeasurability #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Sample-measurability and fourth-power integrability of the flux leg's #
oscillation cell
ABK26, e.nablaw.oscillations, e.Fz.def, e.def.w.
The gap this module fills #
The interior Besov envelope
exists_besovEnvelope_interiorMesoCubeGrid_of_depth_gridRoot_const
carries the two cellwise typing binders
hmeascell : Measurable fun w => meshOscillationCell nn (U w) R' ,
hintcell : Integrable (fun w => meshOscillationCell nn (U w) R' ^ 4) mu ,
and the proved producers of both --- Closure.Step5InputOscillation and the
octic layer of LocalizationFluctuationNumericOctic --- are stated only for
the corrector gradient families. The Neumann leg of the gauged bfF_z is
read at PrincipalResponsePz.neumannFluxField = grad w_N + streamForcing, for
which no producer exists. This module supplies both, without any new analytic
input.
How #
Measurability. The shared representative-based core in
LocalizationFluctuationNumericOctic takes measurable ambient L² classes,
almost-everywhere representatives and measurability of the quadratic window
observable. Here coeFn_toHilbertVectorL2OfVecField identifies the plain vector
field with its class, and
Closure.SplitFoldCellMoments.measurable_volumeAverage_vecNormSq_of_measurable_class
supplies the quadratic measurability. Coordinate transport and centring use the
same earlier producers as the gradient families. The flux class is measurable by
LocalizationFluctuationBackgroundClass.measurable_toHilbertVectorL2OfVecField_neumannFluxField.
Integrability. The cellwise Minkowski split
Closure.GammaTenInteriorMinkowski.meshOscillationCell_neumannFluxField_le
dominates the flux cell by the gradient cell plus the deterministic forcing
gauge 3^{nn} sigma^{-1} d |e'| shellDerivNormSum; (a+b)^4 <= 8(a^4+b^4) and
the proved fourth-power integrability of the forcing gauge
(LocalizationOscillationDisplay.integrable_shellDerivNormSum_rpow_four)
reduce the flux cell's fourth power to the gradient cell's, which the caller
supplies.
What is proved #
measurable_meanSquareOscillationVecOn_of_measurable_class--- the measurability core, for an arbitrary measurable family of ambientL^2classes.measurable_meshOscillationCell_of_measurable_class--- the same at the cell ofe.nablaw.oscillations, read at the cell's own scale.measurable_meshOscillationCell_neumannFluxFieldand..._neumannFluxField_cutoffSample--- the flux leg's cell, on the shell law and on the closure's cutoff-sample carrier.integrable_meshOscillationCell_pow_four_neumannFluxField_cutoffSample--- the flux leg'shintcell, from the gradient leg's.
Binders #
The window data (hS, hSU, hfin, hpos) and the coordinate integrabilities
in the general core; the cell data (hsc, hsub) at the cell; the Neumann
weak-solution property hsol and the L^2 memberships at the flux instances;
and for the integrability the scale gate hnn <= lowScale, lowScale < highScale, and the gradient leg's own fourth-power integrability. No smallness
gate on cgamma, no model estimate and no stationarity is assumed.
Scope #
Internal Provider infrastructure for the Step-2 fluctuation estimate. There is
no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
Proof-text provenance #
Representative transport and oscillation measurability specialize the shared
producers in LocalizationFluctuationNumericOctic. The plain-field instance
obtains its quadratic observable from Closure.SplitFoldCellMoments; the
gradient instances retain that observable as an explicit premise.
References #
- ABK26,
e.nablaw.oscillations,e.Fz.def,e.def.w.
The measurability core, for an arbitrary measurable family of classes #
The measurability core. For a family of vector fields on the cube whose
ambient L^2 classes are measurable in the sample, the mean-square oscillation
over a measurable window is measurable in the sample.
No structure of the fields beyond the measurability of their classes is used; in particular they need not be gradients.
: the window data hS, hSU, hfin, hpos; the L^2 memberships hu; the
class measurability hclass; and the coordinate integrabilities on the window.
The oscillation cell of e.nablaw.oscillations is measurable in the sample
for any family of fields with measurable ambient L^2 classes.
: the cell data hsc, hsub; the L^2 memberships hu; the class
measurability hclass; and the two coordinate integrability families on the
cell.
The flux leg #
The flux leg's oscillation cell is measurable on the shell law.
: the cell data hsc, hsub, the Neumann weak-solution property hsol, and
the two coordinate integrability families on the cell.
The flux leg's oscillation cell is measurable on the cutoff-sample carrier. The closure reads its Besov tower there, not on the shell law.
: the binders of measurable_meshOscillationCell_neumannFluxField.
The flux leg's fourth-power integrability #
The flux leg's hintcell, from the gradient leg's.
The cellwise Minkowski split of
Closure.GammaTenInteriorMinkowski.meshOscillationCell_neumannFluxField_le and
the proved fourth-power integrability of the forcing gauge reduce the flux
cell's fourth power to the gradient cell's.
: the scale gates hnn, hlt, the cell data hsc, hsub, the measurability
hmeas, and the gradient leg's own fourth-power integrability hoscInt.