GammaTenDepthFluxOscillation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The depth oscillation root of the flux leg, on the cutoff-sample carrier #
ABK26, e.lower.bound.oscillations, e.nablaw.oscillations, e.Fz.def.
The two gaps this module closes #
The depth-indexed interior endpoints
from Closure.GammaTenDepthOscillation for the Dirichlet and Neumann correctors
bound the oscillation of the corrector gradient, on M.P.toMeasure. The
Besov tower of Step 2 is read
- at the Neumann leg not of
grad w_Nbut ofPrincipalResponsePz.neumannFluxField = grad w_N + streamForcing, and - on
(cutoffSampleLaw M).toMeasure, the closure's own carrier.
Both transports are performed here, in one statement, at an arbitrary depth ---
the depth index rides the mesh scale nn and the cube family, not the carrier,
so nothing in either transport is depth-specific.
How the flux leg is paid for #
Closure.GammaTenInteriorMinkowski.meshOscillationCell_neumannFluxField_le splits
the cell into osc(grad w_N) plus the deterministic forcing term
3^{nn} shom^{-1} d |e'| shellDerivNormSum, and
LocalizationOscillationGridMoment.gridFourthMomentRoot_le_add_of_le turns the
cellwise split into the grid root at the elementary cost 8^{1/4} <= 2. The
forcing term's own grid root is the single-base-point root at a maximizing cube
(Closure.Step5DefectGauge.gridFourthMomentRoot_shellDerivNormSum_le_of_base_point),
which is exactly the additive term the depth endpoints already carry --- so the
hypothesis hend is used at that maximizing base point and the whole forcing
budget is absorbed into it, at the price of the factor d |e'| <= d.
The conclusion is therefore 2 d times the endpoint's own bound Bd: no new
analytic input, one explicit dimensional constant.
What is proved #
gridFourthMomentRoot_meshOscillationCell_neumannFluxField_cutoffSample_le--- the flux-leg depth root: on the cutoff-sample carrier, the grid fourth-moment root of the flux field's oscillation cells over an interior mesh is at most2 d Bd, whereBdis any bound on the endpoint's own left-hand side (the gradient root plus the forcing gauge) at every base point.
Binders #
The scale gate nn <= lowScale (which is what makes the shell-derivative gauge a
majorant on the oscillation cube), lowScale < highScale (the forcing gauge's
fourth-power integrability), 1 <= d, |e'| <= 1, the window containment hwin
of the mesh cells in the localization cube, the fourth-power integrability
hoscInt of the gradient oscillation cells in the sample, and the endpoint
hypothesis hend. No smallness gate on cgamma, no model estimate and no
measurability of the flux oscillation cell 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.
References #
- ABK26,
e.lower.bound.oscillations,e.nablaw.oscillations,e.Fz.def,e.def.w.
The flux leg #
The depth oscillation root of the flux leg, on the cutoff-sample carrier.
Bd is any bound on the depth endpoints' own left-hand side --- the gradient
oscillation root plus the forcing gauge --- valid at every base point z0;
the depth endpoints of Closure.GammaTenDepthOscillation deliver exactly that,
their base point being universally quantified. The conclusion is the same
quantity read at neumannFluxField instead of grad w_N, on
(cutoffSampleLaw M).toMeasure instead of M.P.toMeasure, at the explicit cost
2 d.
on hnn, hlt, hd1, he', hwin, hoscInt and hend.