FreshShellL8 #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.nablaw.in.L.eight #
This module assembles ABK26's three-line display
‖∇w_{D,e}^{(K)}‖²_{L^8(cu_K)} + ‖∇w_{N,e'}^{(K)}‖²_{L^8(cu_K)}
<= C shom_{m-h}^{-2} ‖k_m - k_{m-h}‖²_{L^8(cu_K)} (i)
<= C shom_{m-h}^{-2} h 3^{2 gamma m}
+ O_{Gamma_1}( C shom_{m-h}^{-2} 3^{2 gamma m} h 3^{-(K-m)d/8}) (ii)
<= C + O_{Gamma_1}( gamma^100 ) (iii)
inside the proof of l.approximate.recurrence.formula, with h = k_m - k_{m-h} the fresh shell, K >= m + 10^10 gamma^{-1} and h <= 6 cstar gamma^{-1} the parameters of e.recurrence.params, and |e|, |e'| <= 1.
The three lines #
- (ii) is
e.km.kn.Lpatp = 8,l = K,m - n = h. It is supplied here byexists_streamIncrementLpNormSq_head_tail, derived from the frozen theoremAlgsuperdiff.Frozen.Section3.stream_increment_lp_large_cube_bound. - (iii) is the deterministic normalization arithmetic, already established
unconditionally in
ShellNormalization:inv_sigmaBarSq_mul_shellWidth_legives the absolute head constant24 * 3^18andconst_mul_rpow_gap_le_gammaPowtogether withexists_gamma_threshold_for_gap_constantgive the manuscript's "increasingMine.cgamma.constraints, if necessary".
Norm gauge #
Every L^8 norm below is cubeEuclideanLpNorm, i.e. the manuscript's
volume-normalized L^8 norm read with the Euclidean pointwise length. The
frozen Calder'on-Zygmund anchor is stated in the ambient sup gauge of
Vec d = Fin d -> ℝ; module CubeEuclideanL8 converts between the two at the
cost of a factor sqrt d, which the dimension-only constant absorbs. The
stream-increment side is Euclidean already: Provider.Stream measures the
increment in Book.Ch02.matrixOperatorNorm, the Euclidean operator norm.
Main results #
exists_streamIncrementLpNormSq_head_tail-- line (ii).exists_cubeEuclideanL8_gradient_sq_sum_le_const_add_gammaPow-- the whole display.
References #
- ABK26,
e.nablaw.in.L.eight. - ABK26,
e.def.w;e.recurrence.params. - ABK26,
e.km.kn.Lp;e.shom.h.bounds.
The positive part of a one-sided tail #
Line (ii): e.km.kn.Lp at p = 8 #
Line (ii) of e.nablaw.in.L.eight.
The squared volume-normalized L^8 norm of a stream increment on a large cube
obeys
‖k_m - k_n‖²_{L^8(cu_l)}
<= C min{gamma^{-1}, m-n} 3^{2 gamma m}
+ O_{Gamma_1}( C min{gamma^{-1}, m-n} 3^{2 gamma m} 3^{-(d/8)(l-m)} ) ,
with one dimension-only constant C, produced before the model and the scales.
The fresh-shell forcing of e.def.w #
The forcing of the two corrector problems e.def.w: shom_{m-h}^{-1} (k_m - k_{m-h}) e.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Euclidean length is homogeneous.
The stream increment is continuous in the space variable.
The forcing of e.def.w is continuous.
The pointwise size of the forcing of e.def.w, for a direction of Euclidean
length at most one.
The right-hand side of line (i). The L^8 norm of the forcing of
e.def.w is at most shom^{-1} times the L^8 norm of the fresh shell.
The display #
e.nablaw.in.L.eight.
There is one dimension-only constant Chead and one positive scale threshold
gamma0 -- the quantitative content of the manuscript's "increasing M in
e.cgamma.constraints, if necessary" -- such that, for every ABK model with
gamma <= gamma0, every valid induction state S(m0, E) of d.mathcalS.def,
every m, K, h obeying the recurrence parameters
m - h <= m0, h <= 6 cstar gamma^{-1}, K >= m + 10^10 gamma^{-1} of
e.recurrence.params, and all directions e, e' of Euclidean length at most
one, there is a nonnegative random amplitude Tfluct with
Tfluct <= O_{Gamma_1}( gamma^100 )
such that every pair of a zero-trace Dirichlet solution and a mean-zero
Neumann solution of the two problems e.def.w satisfies, pathwise,
‖∇w_{D,e}^{(K)}‖²_{L^8(cu_K)} + ‖∇w_{N,e'}^{(K)}‖²_{L^8(cu_K)}
<= Chead + Tfluct(omega) .
Tfluct does not depend on the solutions, so no measurable selection of
correctors is claimed or needed; the left-hand side is the manuscript's actual
sum of squared gradient norms, not a majorant substituted for it.
The L^8 norms are cubeEuclideanLpNorm, i.e. the manuscript's Euclidean
reading of the volume-normalized L^8 norm.
This theorem therefore reaches those two anchors and carries the standard three
axioms, [propext, Classical.choice, Quot.sound]. Line (iii) reaches neither
(ShellNormalization).