PthMomentProcessModel

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

Stopping-time removal at the model confinement scale

The theorem in this module preserves a caller-supplied confinement-scale family. Its one probabilistic input beyond the lift's scale data is the restricted displacement tail used verbatim by the process C4 and C6 estimates.

theorem Algsuperdiff.Section5.Provider.streamProcess_moment_removal_bounds_of_confinement (d : ℕ) [NeZero d] (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (c : ℝ) (hc : 0 < c) (hc1 : c ≤ 1) : ∃ (gamma4 : ℝ) (C4 : ℝ) (C6 : ℝ) (Kc : ℝ), 0 < gamma4 ∧ gamma4 = 1 / 4 ∧ 0 ≤ C4 ∧ 0 ≤ C6 ∧ 1 ≤ Kc ∧ Kc = 1 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma4 → ∀ (t : ℝ), 0 < t → ∀ (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (K L delta : ℝ) (Y : ℤ → Section3.Cutoff.CutoffSample d → ℕ), 1 ≤ K → Kc ≤ K → L = K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t → 0 < delta → delta ≤ 1 → (∀ (i : ℤ), Measurable (Y i)) → (∀ (i : ℤ) (omega : Section3.Cutoff.CutoffSample d), S i omega = Support.displacementScale delta M.gamma (Y i omega)) → (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (i : ℤ) => S i ↑omega) n) L (Support.confinementScale S L ↑omega)) → (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), have m := Support.confinementScale S L ↑omega; have R := 3 ^ m; have Q := (Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0; ∀ (k : ℤ), R ≤ 3 ^ k → Q.real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t.toNNReal)‖} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) → (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), cubeExitProbability M omega (Support.confinementScale S L ↑omega) t.toNNReal ≤ M.gamma ^ 100) → (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), have m := Support.confinementScale S L ↑omega; HCPolySupport.vecNormSq (∫ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (path t.toNNReal) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0 - cubeStoppedMean M omega m t.toNNReal) ≤ C4 * M.gamma ^ 100 * (3 ^ m) ^ 2) ∧ ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), have m := Support.confinementScale S L ↑omega; |∫ (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) => cubeCutoff d m z * HCPolySupport.vecNormSq z) (path (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt 0 m) t.toNNReal path)) ∂(Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0| ≤ C6 * M.gamma ^ 50 * (3 ^ m) ^ 2

The C4 and C6 stopping-time removal bounds at the lift's confinement scale. The restricted tail hypothesis is stated at the same family and scale supplied by the caller.