SuperdiffusivityProvider

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

Assembly of the corrected superdiffusivity estimate

This module assembles the corrected annealed estimates from the model's renormalization family, confinement-scale lift, stopped-moment identities, and process-moment removal bounds.

noncomputable def Algsuperdiff.Section5.Provider.providerComponentConstant (d : ℕ) (CS Cren K C4 C6 : ℝ) : ℝ

A common constant for assembling process, renormalization and cutoff-removal estimates.

Equations

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

def Algsuperdiff.Section5.Provider.HasDisplacementRemovalBounds (d : ℕ) [NeZero d] (cstar : ℝ) : Prop

Quantitative control of removing the confinement cutoff from the stream process.

Equations

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

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

The corrected superdiffusivity estimate from the paired removal bounds at the one confinement-scale family returned by the model lift.

theorem Algsuperdiff.Section5.Provider.superdiffusivity_v2_provider (d : ℕ) [NeZero 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 → ∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) → ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal |∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - 2 * ↑d * Support.intrinsicScale M.nu cstar M.gamma t ^ 2| ^ p ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 4 * Support.intrinsicScale M.nu cstar M.gamma t ^ 2) ^ p ∧ ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (HCPolySupport.vecNormSq (∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0)) ^ p ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C * (p + |Real.log M.gamma|) * M.gamma * |Real.log M.gamma| ^ 7 * Support.intrinsicScale M.nu cstar M.gamma t ^ 2) ^ p

The corrected Theorem A provider at the stream model.