Superdiffusivity with finite displacement moments

This bridge intersects the thresholds from the quantitative theorem and its integrability companion. The displayed expectations therefore have integrable first and second displacement observables in the same small-coupling regime. The original quantitative theorem remains available with its unchanged statement.

theorem Algsuperdiff.superdiffusivity_with_finite_moments (d : ℕ) [NeZero d] (hd : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (t : ℝ), 0 < t → (∀ᵐ (omega : Section5.Field.FullSample d M.gamma) ∂↑(Section5.Field.fullSampleLaw M), MeasureTheory.Integrable (fun (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)) ((Section5.Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) ∧ MeasureTheory.Integrable (fun (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal))) ((Section5.Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0)) ∧ ∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) → ∫⁻ (omega : Section5.Field.FullSample d M.gamma), ENNReal.ofReal |∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)) ∂(Section5.Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - 2 * ↑d * Section5.Support.intrinsicScale M.nu cstar M.gamma t ^ 2| ^ p ∂↑(Section5.Field.fullSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 4 * Section5.Support.intrinsicScale M.nu cstar M.gamma t ^ 2) ^ p ∧ ∫⁻ (omega : Section5.Field.FullSample d M.gamma), ENNReal.ofReal (HCPolySupport.vecNormSq (∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal) ∂(Section5.Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0)) ^ p ∂↑(Section5.Field.fullSampleLaw M) ≤ ENNReal.ofReal (C * (p + |Real.log M.gamma|) * M.gamma * |Real.log M.gamma| ^ 7 * Section5.Support.intrinsicScale M.nu cstar M.gamma t ^ 2) ^ p

One positive threshold gives both displacement integrability and the full quantitative superdiffusivity bounds, uniformly at every positive time.