Step5InputShellMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hshell: the grid fourth moment of the averaged fresh shell #
Closure.Step5Basket.step5GaugeEndpoint_closureFamilies_of_momentLegs leaves
hshell as the binder
( avsum_{R in grid} E[ |(k_{n+h} - k_n)_R|^4 ] )^{1/2}
<= C1 * h * 3^{2 cgamma (n+h)} ,
the grid being descendantsAtDepth cu_K j at K - j = nmesh <= n and |.| the
exact Euclidean matrix operator norm. This module proves it.
The route #
The cube R has scale nmesh <= n, so cu_R sits inside the window
z_R + cu_n based at the cube's own site z_R = triadicCubeShift R. On that
window ABK26's e.km.kn.Linfty.smallcube gives the deterministic domination
|k_{n+h} - k_n|(x) <= translatedIncrementSupBound z_R n (n+h), so the cube
average of each entry is dominated by the same random variable, and
|(k_{n+h} - k_n)_R| <= d^2 * translatedIncrementSupBound z_R n (n+h) .
The probabilistic half is the proved weak-Orlicz tail
Provider.Stream.isBigOWith_gammaSigma_translatedIncrementSupBound_cutoffLaw,
whose amplitude is uniform in the base point; CoarseGraining's layer-cake
moment bound at p = 4, sigma = 2 turns it into a per-cube fourth moment
<= (C_d sqrt h 3^{cgamma (n+h)})^4, and a uniform per-cube bound passes to
the grid average by gridFourthMoment_le_of_forall_le. Taking the square root
gives the display with C1 = step5ShellMomentConst d.
Nothing here is asymptotic in K: the per-cube bound does not see the
localization scale at all.
References #
- ABK26,
e.km.kn.Lp;e.km.kn.Linfty.smallcube; Step 5.
The cube average against a uniform bound on the open cube #
The cube average of an integrable scalar is dominated by a bound assumed on the open cube alone: the closed and open forms of a triadic cube differ by a null set.
The deterministic per-cube domination #
A cube of scale at most n sits inside the window based at its own site.
The averaged fresh shell is dominated by the small-cube L^infty bound at
the cube's own site. For a cube of scale at most n the entries of
k_{n+h} - k_n are dominated on cu_R by translatedIncrementSupBound z_R, and
the exact Euclidean operator norm is at most the entrywise l^1 sum.
The per-cube fourth moment #
The absolute dimensional constant of hshell: the entrywise-l^1 comparison
d^2 of the Euclidean operator norm, times CoarseGraining's layer-cake moment
constant at p = 4, sigma = 2, times the small-cube L^infty constant of
e.km.kn.Linfty.smallcube, squared.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant of hshell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The measurability of the averaged fresh shell in the sample, on the closure's own carrier.
The weak-Orlicz tail of the averaged fresh shell, at the amplitude of
e.km.kn.Linfty.smallcube and the entrywise constant d^2. The proved tail
is uniform in the base point, so this bound does not see the cube.
The per-cube fourth moment of the averaged fresh shell.
hshell on the closure's grid #
hshell, proved. The square root of the grid fourth moment of the
averaged fresh shell is at most h 3^{2 cgamma (n+h)}, at the explicit absolute constant = step5ShellMomentConst d.
This is e.km.kn.Lp in the shape the Hoelder step consumes it, read on the
closure's own grid descendantsAtDepth cu_K j at K - j = nmesh <= n. The
bound is uniform in the localization scale K.
hAmem: the L^4 sample membership of the averaged fresh shell #
hAmem, proved. The averaged fresh shell is L^4 in the sample: its
weak-Orlicz tail is Gamma_2, and CoarseGraining's layer-cake integrability at
p = 4 turns that into the fourth-power integrability.