StepProducers #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-4 endpoint at the closure families, and the Step-5 analytic basket #
Closure.ClosureFinal names three inputs of twoSidedClosure_of_endpoints.
This module produces the second, Closure.ClosureStep4Input, outright, and
discharges every binder of the third that is a statement about the closure's own
corrector families rather than a display of the manuscript.
Step 4 #
Closure.JunctionDischargeStepFour.step4GaugeEndpoint_of_correctors carries
five binders. hD is e.def.w at the Step-6 branch direction e = 0,
discharged by the proved
Closure.isZeroTraceDirichletRhsWeakSolution_alongIncrementPath. The other
four are analytic side conditions of the display itself:
| binder | content | route |
|---|---|---|
hmemN | grad w_N^{(K)} is L^2 of each descendant cube | |
memLp_two_grad_normalizedCubeMeasure_descendant: the H^1 membership on cu_K, restricted along | ||
memLp_normalizedCubeMeasure_of_mem_descendantsAtDepth | ||
hintN | |grad w_N^{(K)}|^2 is integrable on cu_K | integrableOn_cubeSet_vecNormSq_grad, |
| the same membership | ||
hsampR | the per-cube average is sample integrable | continuity of f |-> (grad w_N(f))_R --- |
the set-integral functional hilbertVectorL2CoordSetIntegralCLM composed with | ||
Closure.continuous_gradToHilbertVectorL2_closureNeumannFamily --- dominated by the hsampK | ||
| integrand through per-cube Jensen and the descendant volume ratio | ||
hsampK | E[||grad w_N^{(K)}||^2_{L2(cu_K)}] exists | |
Corrector.CorrectorLimitNode.integrable_cubeAverage_neumann_energy at the closure family |
closureStep4Input is the resulting Closure.ClosureStep4Input d. Its
threshold is C4 = 1: the endpoint holds at every localization scale K and
every mesh depth, so no regime fact of Closure.ClosureRegime is consumed.
The input's leading dimension antecedent 2 <= d is likewise absorbed
trivially: the Step-4 production is dimension-free.
Step 5 #
step5GaugeEndpoint_closureFamilies_of_legs is
Closure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gauge
--- the per-cube-gauge endpoint --- at the closure families with seven
binders discharged: hgauge0, hD and hN (the two halves of e.def.w) and
the Dirichlet mirrors hmemD, hintD, hsampN, hsampG of the four Step-4
routes above. What remains are the mathematical legs --- hintP, hsampX,
hsampS, hsampDef, hdefect, hmemOsc, hmemGauge, hosc, hprod,
hshell, hgradM and the two constants hCdef, hgate, hC1, hgrad0. No
Closure.ClosureStep5Input is claimed.
The per-cube base point #
This module used to route through a single-window declaration
step5GaugeEndpoint_of_correctors (since removed), whose hdefect and
hmemGauge read the forcing gauge of e.nablaw.oscillations at one base
point z0:
step5CrossDefect R omega n (n+h) e (grad w_D)
<= Cdef * ( meshOscillationCell nmesh (grad w_D) R
* (3^nmesh * shellDerivNormSum n (n+h) z0 omega) ) .
That binder is not dischargeable. The left factor meshOscillationCell nmesh u R is the mean square oscillation on openCubeAtScale (triadicCubeShift R) nmesh, sited at the cube R's own base point, whereas shellDerivNormSum n (n+h) z0 omega is an L^infty gauge on the single window z0 + cu_n.
The per-cube step is the deterministic mean value inequality followed by
Cauchy--Schwarz on R, and it needs the gauge on a window containing cubeSet R; as K -> infinity the grid tiles cu_K, so all but finitely many of its
cubes lie outside z0 + cu_n, and Frozen.Assumptions.ShellField is an
arbitrary C^2 skew field.
fun R omega => 3^nmesh * shellDerivNormSum n (n+h) (triadicCubeShift R) omega ,
for which Closure.Step5DefectGauge.step5CrossDefect_le_meshOscillationCell
proves hdefect outright at R.scale = K - j = nmesh <= n (carried out in
Closure.Step5Basket), and for which
ApproximateRecurrence.LocalizationOscillationTail.gridFourthMoment_shellDerivNormSum_le
is uniform in the base point, so hosc keeps its present strength.
References #
- ABK26,
e.lower.bound.pre1;e.nablaw.oscillations;e.lower.bound.oscillations;e.lower.bound.pre2;e.def.w.
Spatial regularity of an H^1 gradient on a triadic cube #
Per-cube Jensen and the descendant volume comparison #
The descendant-cube average of the squared gradient length is dominated by the parent's energy, at the explicit volume ratio.
The descendant cube average as a continuous functional of the class #
The Neumann family: continuity of the descendant cube average #
The two sample-integrability binders of Step 4 #
The Step-4 binder hsampK at the closure's Neumann family, on the increment
path law.
The Step-4 binder hsampK at the closure's Neumann family.
The Step-4 binder hsampR at the closure's Neumann family, on the increment
path law: per-cube Jensen dominates the per-cube average by the cube energy.
The Step-4 binder hsampR at the closure's Neumann family.
The Step-4 endpoint at the closure families, and the input #
Closure.ClosureStep4Input, produced.
The Dirichlet mirror: the Step-5 analytic side conditions #
The Step-5 binder hsampG at the closure's Dirichlet family.
The Step-5 binder hsampN at the closure's Dirichlet family.
The Step-5 endpoint at the closure families, reduced to the residual legs #
Closure.Step5GaugeEndpoint at the closure's own corrector families and at
the per-cube forcing gauge, with the seven analytic side conditions of
step5GaugeEndpoint_of_correctors_gauge discharged.
hgauge0 is the nonnegativity of the gauge; hD, hN are the two halves of
e.def.w at the closure families; hmemD, hintD, hsampN, hsampG are the
Dirichlet mirrors of the four Step-4 routes. What is left is exactly the
mathematical legs.
The forcing gauge is read at each cube's own base point, so the base-point
obstruction recorded in earlier versions of the module docstring no longer
applies: hdefect is dischargeable, and Closure.Step5Basket discharges it.