StoppedMomentsCube

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

The second moment of the whole displacement on a triadic cube

The stopped second moment of StoppedMoments.lean is stated for an abstract conservative Feller process, an abstract open set and one observable. This file sums it over the coordinate directions at the compactified whole-space process of a positive C₀ contractive resolvent and at the image of the translated triadic cube cubeSetAt y n, the carrier the renormalization estimate of the generator is read on: coordinate observables each within B of sigma * t at the stopped position bound the squared norm observable within d * B of d * sigma * t.

Main results

• abs_integral_eval_exitTimeTrunc_vecNormSq_sub_le_cubeSetAt — the sum over the coordinate directions.

References

• ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.

theorem Algsuperdiff.Section5.Provider.abs_integral_eval_exitTimeTrunc_vecNormSq_sub_le_cubeSetAt {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (y : HCPolySupport.Vec d) (n : ℤ) {c : HCPolySupport.Vec d → ℝ} (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) {sigma B : ℝ} (t : NNReal) (hQ : ∀ (i : Fin d), |∫ (omega : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension (fun (z : HCPolySupport.Vec d) => c z * quadraticObservable (HCPolySupport.basisVec i) z) (omega (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑y - sigma * ↑t| ≤ B) : |∫ (omega : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension (fun (z : HCPolySupport.Vec d) => c z * HCPolySupport.vecNormSq z) (omega (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑y - ↑d * (sigma * ↑t)| ≤ ↑d * B

The second moment of the whole displacement on a triadic cube. Summing the coordinate observables, each within B of sigma * t at the stopped position, bounds the squared norm observable within d * B of d * sigma * t.