TailMoments

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

First moments of the two tail gauges

The two legs of the quantitative tail condition of TailGauge.lean are controlled in the mean by the two proved shell displays of the assumptions:

• the descending value gauge ‖j_{ℓ-r}‖_{L^∞(□_ℓ)} has the one-shell scaling law of (J2), whose first moment on the cube □_ℓ is of order 3^{γ(ℓ-r)} (1+r)^{1/2}, the profile cubeMajorant;
• the ascending volume-normalized gradient gauge ‖∇ j_{ℓ+r}‖_{W^{1,∞}(y+□_ℓ)} has a Γ₂ upper tail at the amplitude 3^{-ℓ} 3^{(γ-1)(ℓ+r)} of e.nabla.jk.O, so its first moment is at most a constant multiple of that amplitude.

Weighing the first by 3^{-ℓ} and the second by 3^{ℓ} makes both profiles proportional to (3^{γ-1})^{ℓ}, which is summable because γ ≤ 1/4.

References

• ABK26, e.jk.O, e.nabla.jk.O.

3. The ascending gradient leg

theorem Algsuperdiff.Section5.Field.measurable_shellW1InfGradNorm_translate_comp {d : ℕ} (k i : ℤ) (y : HCPolySupport.Vec d) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => Section4.Support.shellW1InfGradNorm k (Frozen.Assumptions.ShellField.translate y (↑omega i))

theorem Algsuperdiff.Section5.Field.shellW1InfGradAmplitude_pos {d : ℕ} (M : Section3.ABKModel d) (k i : ℤ) : 0 < 3 ^ (-k) * Real.rpow 3 ((M.gamma - 1) * ↑i)

Positivity of the ascending amplitude.