QuenchedMomentsComposer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Quenched displacement-moment composition #
This module combines the stopped cube estimates, stopping-time removal, and the comparison of the running diffusivity with the intrinsic scale. The process-moment and cube-moment inputs are kept as separately named hypotheses in the forms delivered by their respective provider layers.
theorem
Algsuperdiff.Section5.Provider.secondMoment_quenched_of_moments
{d : ℕ}
[NeZero d]
(M : Section3.ABKModel d)
(cstar t C0 : ℝ)
(omega : Field.FullSample d M.gamma)
(S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ)
(L : ℝ)
(c : HCPolySupport.Vec d → ℝ)
(sigmaBar exitProbability Ccube Cremove Cscale : ℝ)
(ht : 0 < t)
(hgamma4 : M.gamma ≤ 1 / 4)
(hCremove : 0 ≤ Cremove)
(hEBnn : ∀ (n : ℤ) (eta : Section3.Cutoff.CutoffSample d), 0 ≤ EB n eta)
(hexitProbability : 0 ≤ exitProbability)
(hscaleSq : 0 ≤ (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hsigmaTime_le : ↑d * (sigmaBar * t) ≤ (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hC3 :
∀ (i : Fin d),
|∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension
(fun (z : HCPolySupport.Vec d) => c z * quadraticObservable (HCPolySupport.basisVec i) z)
(path
(MarkovProcess.ContinuousPath.exitTimeTrunc
(OnePoint.some '' Support.cubeSetAt 0 (Support.confinementScale S L ↑omega)) t.toNNReal
path)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - 2 * sigmaBar * ↑t.toNNReal| ≤ Ccube * (3 ^ Support.confinementScale S L ↑omega) ^ 2 * EB (Support.confinementScale S L ↑omega) ↑omega + 2 * (sigmaBar * ↑t.toNNReal) * exitProbability)
(hQmeas :
∀ (i : Fin d), Measurable fun (z : HCPolySupport.Vec d) => c z * quadraticObservable (HCPolySupport.basisVec i) z)
{CQ : ℝ}
(hCQ : ∀ (i : Fin d) (z : HCPolySupport.Vec d), |c z * quadraticObservable (HCPolySupport.basisVec i) z| ≤ CQ)
(hC6 :
|∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq
(DivergenceFormProcess.Form.onePointRetract 0
(path t.toNNReal)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - ∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension
(fun (z : HCPolySupport.Vec d) => c z * HCPolySupport.vecNormSq z)
(path
(MarkovProcess.ContinuousPath.exitTimeTrunc
(OnePoint.some '' Support.cubeSetAt 0 (Support.confinementScale S L ↑omega)) t.toNNReal
path)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0| ≤ Cremove * M.gamma ^ 50 * (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hprofile :
|↑d * Support.intrinsicScale M.nu cstar M.gamma t ^ 2 - ↑d * (sigmaBar * t)| ≤ Cscale * √M.gamma * |Real.log M.gamma| * (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hearlyExit : exitProbability ≤ M.gamma ^ 100)
(hCstopped : ↑d * Ccube ≤ C0)
(hCtail : Cremove + 2 + 2 * Cscale ≤ C0)
:
|∫ (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 * (EB (Support.confinementScale S L ↑omega) ↑omega + √M.gamma * |Real.log M.gamma|) * (3 ^ Support.confinementScale S L ↑omega) ^ 2
The quenched second-moment comparison obtained by summing the directional stopped estimates and combining them with stopping-time removal and the intrinsic-scale comparison.
theorem
Algsuperdiff.Section5.Provider.meanSq_quenched_of_moments
{d : ℕ}
[NeZero d]
(M : Section3.ABKModel d)
(t C0 : ℝ)
(omega : Field.FullSample d M.gamma)
(S EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ)
(L : ℝ)
(stoppedMean : HCPolySupport.Vec d)
(Cstopped Cremove : ℝ)
(hgamma4 : M.gamma ≤ 1 / 4)
(hscaleSq : 0 ≤ (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hCremove : 0 ≤ Cremove)
(hC5 :
HCPolySupport.vecNormSq stoppedMean ≤ Cstopped * (3 ^ Support.confinementScale S L ↑omega) ^ 2 * EB (Support.confinementScale S L ↑omega) ↑omega ^ 2)
(hC4 :
HCPolySupport.vecNormSq
(∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0
(path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - stoppedMean) ≤ Cremove * M.gamma ^ 100 * (3 ^ Support.confinementScale S L ↑omega) ^ 2)
(hCstopped : 2 * Cstopped ≤ C0)
(hCtail : 2 * Cremove ≤ C0)
:
HCPolySupport.vecNormSq
(∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0
(path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) ≤ C0 * (EB (Support.confinementScale S L ↑omega) ↑omega ^ 2 + M.gamma ^ 80) * (3 ^ Support.confinementScale S L ↑omega) ^ 2
The quenched squared-mean comparison obtained from the stopped mean and the squared stopping-time-removal estimate.