LocalizationOscillationFullMesh #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.lower.bound.oscillations on the full mesh, and at the closure's carrier #
ABK26, e.lower.bound.oscillations. Two transports separate the proved interior
endpoint from the shape the Step-5 gauge junction consumes; the docstring of
Closure.JunctionDischargeStepFiveDisplay names both under "Carrier transports the
caller must supply on hosc". This module performs both.
1. Interior mesh to full mesh #
LocalizationOscillationEndpoint averages over interiorMesoCubeGrid, whereas
the manuscript's display -- and Closure.Step5GaugeEndpoint -- averages over the
full mesh 3^n Zd cap cu_K. The three steps are
LocalizationFluctuationGammaFold.gridFourthMoment_mesoCubeGrid_le_interior_add_of_eighthMoment: the full grid fourth moment is the interior one plus a geometric boundary remainder carrying the square root of an eighth-moment envelopeE;gridFourthMomentRoot_le_add_rpow_of_lebelow: the fourth root is subadditive,(A + B)^{1/4} <= A^{1/4} + B^{1/4}, so the remainder survives the outer root as its own fourth root -- the proved per-cubegridFourthMomentRoot_le_add_of_ledoes not serve, its majorant being pointwise on the grid rather than additive on the functional;LocalizationFluctuationGammaFold.exists_gamma_threshold_mesh_boundary: under the recurrence's own large-cube gate10^10 gamma^{-1} <= K - mthe remainder is belowgamma^{100}, hence its fourth root belowgamma^{25}.
The interior half is taken at gamma^{16}
(LocalizationOscillationEndpointSixteen), so the sum is
gamma^{16} + gamma^{25} <= 2 gamma^{16} <= gamma^{15} for gamma <= 1/2, which
the standing gamma <= 1/4 gives.
2. Shell-sequence law to cutoff-sample law #
The endpoint runs on M.P.toMeasure, the closure's carrier is
(cutoffSampleLaw M).toMeasure. Cutoff.map_cutoffSampleLaw_val pushes the
second forward onto the first along Subtype.val, which is a measurable
embedding (Cutoff.measurableSet_lowerTailGoodSet), so
MeasurableEmbedding.integral_map transports every Bochner integral with no
measurability hypothesis on the integrand. gridFourthMoment_val_cutoffSampleLaw
and integral_cutoffSampleLaw_val are the two resulting identities; both are
unconditional.
3. The mesh index #
LocalizationGrid.mesoCubeGrid_eq_descendantsAtDepth identifies the display's
grid 3^{nmesh} Zd cap cu_K with the closure's descendantsAtDepth cu_K j at
nmesh = K - j. The corollary is stated at the closure's index.
What is proved #
gridFourthMomentRoot_le_add_rpow_of_le-- grid-level fourth-root subadditivity.integral_cutoffSampleLaw_val,gridFourthMoment_val_cutoffSampleLaw,gridFourthMomentRoot_val_cutoffSampleLaw-- the carrier transport, unconditional.exists_gamma0_freshShellDirichlet_fullMeshOscillation_le_gamma_pow_fifteen-- the full-mesh endpoint onM.P.toMeasure.
Binders #
Beyond those of the proved endpoint -- the model gate, the induction state, the
four source gates of e.recurrence.params, the direction bound and the weak
formulation of e.def.w -- exactly two propositions are added, both analytic
side conditions on the very objects the display is about, and both instances
of e.nablaw.in.L.eight:
hmem8, theL^2-in-the-sample membership of the fourth powers of the oscillation cells, i.e. the finiteness of their eighth moments;hE, an envelope for the eighth-moment grid average of the same cells.
LocalizationFluctuationGridEighth reduces hE to fint_{cu_K} |u|^8 at the
tiling constant 1, and thence to ‖u‖^8_{L8bar(cu_K)}; the last step of that
reduction -- the finiteness of E[(Chead + Tfluct)^4] -- is at its producer
and is not performed here. E is a parameter of the statement, quantified
before the threshold, so no smallness or normalization is assumed: the
threshold is produced from E, as exists_gamma_threshold_mesh_boundary
requires.
Scope #
There is no sorry.
References #
- ABK26,
e.lower.bound.oscillations,e.recurrence.params,e.nablaw.in.L.eight.
Grid-level fourth-root subadditivity #
The fourth root is subadditive on the grid functional. If the grid
fourth moment splits as A + B, its fourth root splits as A^{1/4} + B^{1/4}.
The proved gridFourthMomentRoot_le_add_of_le does not serve here: its
majorant is pointwise on the grid (F R omega <= G R omega + H R omega), whereas
the mesh transfer's remainder is additive on the functional, with no
pointwise representative. only on hA, hB and h.
The carrier transport #
Unconditional. Every Bochner integral against the cutoff-sample law,
read through Subtype.val, is the corresponding integral against the
shell-sequence law. Subtype.val is a measurable embedding onto the
lower-tail-good carrier, so no measurability hypothesis on the integrand is
needed.
Unconditional. The grid fourth-moment functional is carrier-independent in the same sense.
Unconditional. The same for the outer fourth root.
The full-mesh endpoint #
e.lower.bound.oscillations on the full mesh, below gamma^{15}.
The interior endpoint of LocalizationOscillationEndpointSixteen at
gamma^{16}, plus the boundary remainder at gamma^{25}, on the manuscript's
own carrier 3^n Zd cap cu_K.
on the binders of the proved endpoint together with the two
e.nablaw.in.L.eight side conditions hmem8 and hE; see the module
docstring's binder census. The threshold is produced from E.
The Step-5 hosc shape #
The full-mesh endpoint, read at the closure's own carrier
(cutoffSampleLaw M).toMeasure, at the closure's own grid
descendantsAtDepth cu_K j, and at the shell pair (n, n + h) with gauge
shom_n^{-1} -- i.e. at m = n + h in the parameters of the endpoint. The
mesh scale nmesh and the depth j are tied by hj : j = K - nmesh, which is
the identification LocalizationGrid.mesoCubeGrid_eq_descendantsAtDepth, and
nmesh is the recurrence buffer of e.recurrence.params by hnmesh.
A caller instantiates wD := Closure.alongIncrementPath n h w, at which point
the conclusion is literally the hosc binder.
on the binders of the full-mesh endpoint; see the module docstring.