LocalizationOscillationTail

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the fourth moment of the forcing gauge of e.nablaw.oscillations

Source displays in ABK26:

• e.nablaw.oscillations (label; display) carries on its right the forcing amplitude shom_{m-h}^{-1} (m-h-n) 3^n ‖ grad (k_m - k_{m-h}) ‖_{L^infty(z+cu_{m-h})};
• e.lower.bound.oscillations (label; display) takes the fourth moment of exactly that quantity, shom_{m-h}^{-1} 3^n E[ ‖grad(k_m - k_{m-h})‖_{L^infty(cu_{m-h})}^4 ]^{1/4}, and claims it is at most C shom_{m-h}^{-1} 3^{-(m-h-n)} 3^{gamma(m-h)} gamma^{-1}.

This module supplies the probabilistic half of that passage: the fourth moment of the shell-derivative gauge sum on the cube z + cu_{m-h}, obtained from the already-proved weak-Orlicz tail Provider.Stream.isBigOWith_gammaSigma_shellDerivNormSum_Ioc_translate (ABK26's e.nabla.km.kn.infty) through CoarseGraining's layer-cake moment bound IndependentSums.integral_rpow_le_of_isBigOWith_gammaSigma at p = 4.

The carrier

The random variable is the one that the proved instantiation of e.nablaw.oscillations at the fresh-shell correctors (Corrector.exists_freshShellDirichlet_gradient_oscillation_interior_mesh_localGauge and its Neumann counterpart) puts on the right of the display: the summed first-derivative gauges sum_{k in (lowScale, highScale]} localCubeDerivNorm lowScale (translate z (omega k)) on the cube z + cu_{lowScale}, at lowScale = m - h and highScale = m. It dominates ‖grad(k_m - k_{m-h})‖_{L^infty(z+cu_{m-h})} by the triangle inequality over the shells, with no loss.

What is proved

• integral_shellDerivNormSum_rpow_four_le -- the fourth moment.
• shellDerivNormSum_momentRoot_four_le -- its fourth root, which is the shape the display consumes.
• mul_shellDerivNormSum_momentRoot_four_le_gap -- the same bound multiplied by the display's prefactor 3^n, rewritten in the manuscript's two-factor gap form 3^{-(m-h-n)} 3^{gamma(m-h)}.

Divergences from the printed statement

• The constant is absolute, and sharper than the printed one. The manuscript writes C gamma^{-1} for the amplitude of this term; the bound below has no gamma^{-1} and no (m-h-n) factor, only the dimension-free weak-Orlicz constants of the class Gamma_2. The printed form follows from this one, since gamma^{-1} >= 1 in the regime of e.cgamma.constraints. Nothing is absorbed silently: the constant appears in full as gammaMomentConst 2 * 4^{1/2} * gammaTriangleConst 2.
• . The statement below is a per-base-point statement, quantified over z.
• The gauge, not the L^infty norm. The manuscript's random variable is ‖grad(k_m - k_{m-h})‖_{L^infty(z+cu_{m-h})}; the one below is the summed first-derivative gauge that dominates it (see the carrier note above). The moment bound therefore implies the printed one and is stronger.

The random variable

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellDerivNormSum {d : ℕ} (lowScale highScale : ℤ) (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : ℝ

The summed first-derivative shell gauges on the cube z + cu_ell, over the shell range (lowScale, highScale]. At ell = lowScale = m - h and highScale = m this is the forcing amplitude of e.nablaw.oscillations.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellDerivNormSum_nonneg {d : ℕ} (lowScale highScale : ℤ) (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : 0 ≤ shellDerivNormSum lowScale highScale z omega

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_shellDerivNormSum {d : ℕ} (lowScale highScale : ℤ) (z : HCPolySupport.Vec d) : Measurable (shellDerivNormSum lowScale highScale z)

The fourth-moment constant

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellDerivGammaFourthConst : ℝ

The absolute fourth-moment constant of the class Gamma_2: the layer-cake constant gammaMomentConst 2 * 4^{1/2} composed with the triangle constant of the shell sum.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellDerivGammaFourthConst_pos : 0 < shellDerivGammaFourthConst

The fourth moment

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_shellDerivNormSum_rpow_four_le {d : ℕ} (M : ABKModel d) {lowScale highScale : ℤ} (hlt : lowScale < highScale) (z : HCPolySupport.Vec d) : ∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum lowScale highScale z omega ^ 4 ∂↑M.P ≤ (shellDerivGammaFourthConst * 3 ^ ((M.gamma - 1) * ↑lowScale)) ^ 4

The fourth moment of the forcing gauge of e.nablaw.oscillations. The weak-Orlicz tail e.nabla.km.kn.infty at the translated cube, run through the layer-cake moment bound at p = 4.

The fourth root, and the manuscript's gap form

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellDerivNormSum_momentRoot_four_le {d : ℕ} (M : ABKModel d) {lowScale highScale : ℤ} (hlt : lowScale < highScale) (z : HCPolySupport.Vec d) : (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum lowScale highScale z omega ^ 4 ∂↑M.P) ^ 4⁻¹ ≤ shellDerivGammaFourthConst * 3 ^ ((M.gamma - 1) * ↑lowScale)

The fourth root of the previous display, which is the shape in which e.lower.bound.oscillations consumes it.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_gap_factorization (gamma : ℝ) (n : ℤ) (N : ℕ) : 3 ^ ↑n * 3 ^ ((gamma - 1) * (↑n + ↑N)) = 3 ^ (-↑N) * 3 ^ (gamma * (↑n + ↑N))

The manuscript writes the amplitude of this term as the product of the scale gap and the shell gauge, 3^{-(m-h-n)} 3^{gamma(m-h)}. With lowScale = n + N and N = m - h - n that is exactly the prefactor 3^n applied to the bound above.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mul_shellDerivNormSum_momentRoot_four_le_gap {d : ℕ} (M : ABKModel d) {n : ℤ} {N : ℕ} {highScale : ℤ} (hlt : n + ↑N < highScale) (z : HCPolySupport.Vec d) : 3 ^ ↑n * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum (n + ↑N) highScale z omega ^ 4 ∂↑M.P) ^ 4⁻¹ ≤ shellDerivGammaFourthConst * (3 ^ (-↑N) * 3 ^ (M.gamma * (↑n + ↑N)))

The forcing term of e.lower.bound.oscillations, at one base point. The prefactor 3^n of the display times the fourth moment root of the forcing gauge on z + cu_{n+N} is at most the absolute constant times the manuscript's two-factor amplitude 3^{-N} 3^{gamma (n+N)}.