StoppedMomentsCubeStream

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

The stopped moments on a triadic cube for the stream field

The bounds of StoppedMomentsCubeMeanValue.lean carry two premises about the process: the exit mean-value property of the observable on the cube, and the finiteness of the expected exit time from its centre. Against the stream field of the model both are supplied: the first by the consumer lemma of CubeSetAtMeanValueStream.lean, from the weak harmonicity of the observable on the cube and its smooth compactly supported boundary datum; the second by expectedExitTime_cubeSetAt_ne_top_stream.

This file composes the two halves. No global small-contrast datum appears in any statement: the process hypotheses are exactly those of the coefficient-generic comparison, namely the resolvent carrying the process, its one-point regularity data, conservativity of the live kernel semigroup, the bounded-measurable identification of the kernel resolvent with the analytic minimal resolvent, and the operator identification against the C₀ barrier resolvent of the stream field.

The remaining hypotheses are the homogenization inputs: the observable is an H¹ function of the cube solving the homogeneous equation weakly there, is continuous there, agrees off the cube with a smooth compactly supported function, and has that function's trace; and the second observable is uniformly close to it.

Main results

• sq_integral_eval_exitTimeTrunc_onePointRealExtension_le_cubeSetAt_stream — the square of the stopped mean on a triadic cube.
• abs_integral_eval_exitTimeTrunc_onePointRealExtension_sub_mul_le_cubeSetAt_stream — the stopped second moment on a triadic cube.

References

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

2. The composed stopped mean on a triadic cube

theorem Algsuperdiff.Section5.Provider.sq_integral_eval_exitTimeTrunc_onePointRealExtension_le_cubeSetAt_stream {d : ℕ} [NeZero d] {Model : Section3.ABKModel d} {omega : Field.FullSample d Model.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Field.streamWholeSpaceAnalyticData Model omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) {bd : HCPolySupport.Vec d → ℝ} (hbd : ContDiff ℝ (↑⊤) bd) (hbdCompact : HasCompactSupport bd) {u : HCPolySupport.Vec d → ℝ} (hu : Measurable u) {N : ℝ} (hN : ∀ (z : HCPolySupport.Vec d), |u z| ≤ N) (hoff : ∀ z ∉ Support.cubeSetAt y n, u z = bd z) (hucont : ContinuousOn u (Support.cubeSetAt y n)) (Y : HCPolySupport.H1Function (Support.cubeSetAt y n)) (hY : ∀ (z : HCPolySupport.Vec d), Y.toFun z = u z) (hharm : DivergenceFormProcess.Form.IsScalarForcedWeakSolution (Field.streamWholeSpaceAnalyticData Model omega).a (Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 0) Y) (htrace : HCPolySupport.MemH10 (Support.cubeSetAt y n) fun (z : HCPolySupport.Vec d) => u z - bd z) {b : HCPolySupport.Vec d → ℝ} (hb : Measurable b) {K : ℝ} (hK0 : 0 ≤ K) (hKb : ∀ (z : HCPolySupport.Vec d), |b z - u z| ≤ K) (hb0 : b y = 0) (t : NNReal) : (∫ (omegaPath : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension b (omegaPath (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t omegaPath)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑y) ^ 2 ≤ 4 * K ^ 2

The squared stopped mean against the stream-field process on a triadic cube.

3. The composed stopped second moment on a triadic cube

theorem Algsuperdiff.Section5.Provider.abs_integral_eval_exitTimeTrunc_onePointRealExtension_sub_mul_le_cubeSetAt_stream {d : ℕ} [NeZero d] {Model : Section3.ABKModel d} {omega : Field.FullSample d Model.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : (Field.streamWholeSpaceAnalyticData Model omega).KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (y : HCPolySupport.Vec d) (n : ℤ) {bd : HCPolySupport.Vec d → ℝ} (hbd : ContDiff ℝ (↑⊤) bd) (hbdCompact : HasCompactSupport bd) {w : HCPolySupport.Vec d → ℝ} (hwmeas : Measurable w) {N : ℝ} (hN : ∀ (z : HCPolySupport.Vec d), |w z| ≤ N) (hoff : ∀ z ∉ Support.cubeSetAt y n, w z = bd z) (hwcont : ContinuousOn w (Support.cubeSetAt y n)) (Y : HCPolySupport.H1Function (Support.cubeSetAt y n)) (hY : ∀ (z : HCPolySupport.Vec d), Y.toFun z = w z) (hharm : DivergenceFormProcess.Form.IsScalarForcedWeakSolution (Field.streamWholeSpaceAnalyticData Model omega).a (Support.cubeSetAt y n) (fun (x : HCPolySupport.Vec d) => 0) Y) (htrace : HCPolySupport.MemH10 (Support.cubeSetAt y n) fun (z : HCPolySupport.Vec d) => w z - bd z) {q : HCPolySupport.Vec d → ℝ} (hq : Measurable q) {Cq : ℝ} (hCq : ∀ (z : HCPolySupport.Vec d), |q z| ≤ Cq) {sigma : ℝ} (hsigma : 0 ≤ sigma) {K : ℝ} (hKb : ∀ (z : OnePoint (HCPolySupport.Vec d)), |DivergenceFormProcess.Form.onePointRealExtension q z - (DivergenceFormProcess.Form.onePointRealExtension w z - sigma * (DivergenceFormProcess.StoppedDirichlet.expectedExitTime R.onePointKernelSemigroup ⋯ (OnePoint.some '' Support.cubeSetAt y n) z).toReal)| ≤ K) (hq0 : q y = 0) (t : NNReal) : |∫ (omegaPath : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), DivergenceFormProcess.Form.onePointRealExtension q (omegaPath (MarkovProcess.ContinuousPath.exitTimeTrunc (OnePoint.some '' Support.cubeSetAt y n) t omegaPath)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑y - sigma * ↑t| ≤ 2 * K + sigma * (↑t * (((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑y) (DivergenceFormProcess.StoppedDirichlet.survivalEvent (OnePoint.some '' Support.cubeSetAt y n) t)ᶜ).toReal)

The stopped second moment against the stream-field process on a triadic cube. The corrected observable is the weakly harmonic function less sigma times the expected exit time from the cube.