PthMomentProcess

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

Stream-process moments and stopping-time removal

A square-exponential displacement tail at every triadic radius above a normalization scale gives all real moments. The second section combines those moments with an almost-everywhere bound for the stopped position to remove a stopping time from the first and second moments.

theorem Algsuperdiff.Section5.Provider.integral_norm_onePointRetract_streamProcess_rpow_le_of_triadic_sq_tail {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) (t : NNReal) {R c p : ℝ} (hR : 0 < R) (hc : 0 < c) (hc1 : c ≤ 1) (hp : 1 ≤ p) : have Q := (Field.streamProcess M omega) ↑0; have A := 3 / 2 * max 1 (c * Real.log 2)⁻¹; (∀ (k : ℤ), R ≤ 3 ^ k → Q.real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t)‖} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) → MeasureTheory.Integrable (fun (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) => ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t)‖ ^ p) Q ∧ ∫ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t)‖ ^ p ∂Q ≤ (6 * p * (A * R)) ^ p

The process C2 moment row. A restricted all-integer-scale triadic tail for the stream process gives every real moment p ≥ 1, with the interpolation constant displayed explicitly.

Removal at the exit time

theorem Algsuperdiff.Section5.Provider.vecNormSq_integral_onePointRetract_sub_exitTimeTrunc_le {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) {U : Set (OnePoint (HCPolySupport.Vec d))} (hU : IsOpen U) (t : NNReal) {R c B : ℝ} (hR : 0 < R) (hc : 0 < c) (hc1 : c ≤ 1) : have Q := (Field.streamProcess M omega) ↑0; have A := 3 / 2 * max 1 (c * Real.log 2)⁻¹; (∀ (k : ℤ), R ≤ 3 ^ k → Q.real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t)‖} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) → (∀ᵐ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂Q, eta ∈ (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ → ‖DivergenceFormProcess.Form.onePointRetract 0 (eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta))‖ ≤ B) → HCPolySupport.vecNormSq (∫ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (eta t) ∂Q - ∫ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRetract 0 (eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta)) ∂Q) ≤ ↑d * (((6 * 2 * (A * R)) ^ 2) ^ (1 / 2) * Q.real (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ ^ (1 / 2) + B * Q.real (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ) ^ 2

The process C4 removal row. The full and stopped stream-process positions agree on survival. The restricted tail supplies the first and second moments of the full position; a pointwise bound supplies integrability of the stopped position.

theorem Algsuperdiff.Section5.Provider.abs_integral_vecNormSq_sub_exitTimeTrunc_cutoff_le {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : Field.FullSample d M.gamma) {U : Set (OnePoint (HCPolySupport.Vec d))} (hU : IsOpen U) (t : NNReal) (cutoff : HCPolySupport.Vec d → ℝ) (hcutoff : Measurable fun (z : HCPolySupport.Vec d) => cutoff z * HCPolySupport.vecNormSq z) {R c B : ℝ} (hR : 0 < R) (hc : 0 < c) (hc1 : c ≤ 1) : have Q := (Field.streamProcess M omega) ↑0; have A := 3 / 2 * max 1 (c * Real.log 2)⁻¹; (∀ (k : ℤ), R ≤ 3 ^ k → Q.real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖DivergenceFormProcess.Form.onePointRetract 0 (eta t)‖} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) → (∀ eta ∉ (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ, HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (eta t)) = DivergenceFormProcess.Form.onePointRealExtension (fun (z : HCPolySupport.Vec d) => cutoff z * HCPolySupport.vecNormSq z) (eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta))) → (∀ᵐ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂Q, eta ∈ (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ → |DivergenceFormProcess.Form.onePointRealExtension (fun (z : HCPolySupport.Vec d) => cutoff z * HCPolySupport.vecNormSq z) (eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta))| ≤ B) → |∫ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), HCPolySupport.vecNormSq (DivergenceFormProcess.Form.onePointRetract 0 (eta t)) ∂Q - ∫ (eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension (fun (z : HCPolySupport.Vec d) => cutoff z * HCPolySupport.vecNormSq z) (eta (MarkovProcess.ContinuousPath.exitTimeTrunc U t eta)) ∂Q| ≤ (↑d ^ 2 * (6 * 4 * (A * R)) ^ 4) ^ (1 / 2) * Q.real (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ ^ (1 / 2) + B * Q.real (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ

The process C6 removal row. The fourth moment supplied by the restricted displacement tail controls the Euclidean second-moment observable. The stopped integrand is exactly the cutoff-weighted observable used by the quenched composer.