SuperdiffusivityAssembly

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

Annealed assembly of the reachable superdiffusive bounds

This file carries out the measure-theoretic last step from quenched displacement estimates at a random confinement scale. The input structure names the two quenched comparisons, the second- and fourth-order moments of the renormalization error, and the fourth-order moment of the confinement radius. In an application, the first two fields are supplied after the process moment, rare-exit, and stopping-time-removal estimates have been combined.

The Cauchy--Schwarz splits use exponents 2p for the first comparison and 4p, 4p, 2p for the second comparison. Thus the separately available random-radius estimate contributes one power of |log gamma|. The resulting powers are 4 and 7; no claim with the smaller powers is made here.

The component interface

structure Algsuperdiff.Section5.Provider.SuperdiffusivityV2Components {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (cstar t p C0 : ℝ) : Type

Named inputs for the annealed assembly at one model, time, and exponent.

The confinementRadius is 3^m_t in the intended application. The two pointwise fields are the outputs of the quenched stopped-moment assembly after the C2 process moments, the bad-event bound, and the C4/C6 removal estimates have been supplied. The remaining three fields are the random-scale estimates used by the two Holder splits.

• renormalizationError : Field.FullSample d M.gamma → ℝ

  The samplewise renormalization error used in the superdiffusivity assembly.

• confinementRadius : Field.FullSample d M.gamma → ℝ

  The samplewise confinement radius used in the superdiffusivity assembly.

• renormalizationError_nonneg (omega : Field.FullSample d M.gamma) : 0 ≤ self.renormalizationError omega
• confinementRadius_nonneg (omega : Field.FullSample d M.gamma) : 0 ≤ self.confinementRadius omega
• renormalizationError_aemeasurable : AEMeasurable self.renormalizationError ↑(Field.fullSampleLaw M)
• confinementRadius_aemeasurable : AEMeasurable self.confinementRadius ↑(Field.fullSampleLaw M)
• secondMoment_quenched : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), |∫ (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| ≤ C0 * (self.renormalizationError omega + √M.gamma * |Real.log M.gamma|) * self.confinementRadius omega ^ 2
• meanSq_quenched : ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), HCPolySupport.vecNormSq (∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) ≤ C0 * (self.renormalizationError omega ^ 2 + M.gamma ^ 80) * self.confinementRadius omega ^ 2
• renormalizationError_moment_two : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (self.renormalizationError omega) ^ (2 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ (2 * p)
• renormalizationError_moment_four : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (self.renormalizationError omega) ^ (4 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ (4 * p)
• confinementRadius_moment_four : ∫⁻ (omega : Field.FullSample d M.gamma), ENNReal.ofReal (self.confinementRadius omega) ^ (4 * p) ∂↑(Field.fullSampleLaw M) ≤ ENNReal.ofReal (C0 * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t) ^ (4 * p)

Numerical absorption

The reachable provider

theorem Algsuperdiff.Section5.Provider.superdiffusivity_v2_of_components (d : ℕ) [NeZero d] (cstar : ℝ) (hcstar : 0 < cstar) (gammaBase C0 : ℝ) (hgammaBase : 0 < gammaBase) (hC0 : 1 ≤ C0) (hcomponents : (M : Section3.ABKModel d) → Section3.Disorder.cstar M = cstar → M.gamma ≤ gammaBase → (t : ℝ) → 0 < t → (p : ℝ) → 1 ≤ p → p ≤ C0⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) → SuperdiffusivityV2Components M cstar t p C0) : ∃ (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 annealed superdiffusive estimates obtained from the separately named quenched and random-scale components. The conclusion has the reachable logarithmic powers 4 and 7.

No small-time premise is built into the assembly: if the process moment supplier uses a large-time/small-time split, that split is discharged while constructing SuperdiffusivityV2Components.