CruxStreamExitTime #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Exit times for the stream-field process #
These are the exhaustion-cube exit-time consequences of the coefficient-generic C₀ barrier comparison. Their assumptions contain no global small-contrast datum.
theorem
DivergenceFormProcess.Form.WholeSpaceAnalyticData.killedResolvent_one_eq_cubeExitResolvent_stream
{d : ℕ}
[NeZero d]
{M : Algsuperdiff.Section3.ABKModel d}
{omega : Algsuperdiff.Section5.Field.FullSample d M.gamma}
(R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d))
(hreg : R.OnePointRegular)
(hcons : R.kernelSemigroup.IsConservative)
(hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R)
(hT :
∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ),
(R.operator mu) g = (⋯.resolvent.operator mu) g)
(v : ℕ)
{lam : ℝ}
(hlam : 0 < lam)
{z : OnePoint (HCPolySupport.Vec d)}
(hz : z ∈ OnePoint.some '' wholeSpaceCube d v)
:
MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent R.onePointKernelSemigroup ⋯
(OnePoint.some '' wholeSpaceCube d v) ⋯ lam (fun (x : OnePoint (HCPolySupport.Vec d)) => 1) z = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeExitResolvent v lam z
The killed stream resolvent of one on a centered exhaustion cube is its Dirichlet resolvent.
theorem
DivergenceFormProcess.Form.WholeSpaceAnalyticData.lintegral_exitTime_eq_cubeExitFunction_stream
{d : ℕ}
[NeZero d]
{M : Algsuperdiff.Section3.ABKModel d}
{omega : Algsuperdiff.Section5.Field.FullSample d M.gamma}
(R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d))
(hreg : R.OnePointRegular)
(hcons : R.kernelSemigroup.IsConservative)
(hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R)
(hT :
∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ),
(R.operator mu) g = (⋯.resolvent.operator mu) g)
(v : ℕ)
{x : HCPolySupport.Vec d}
(hx : x ∈ wholeSpaceCube d v)
:
∫⁻ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), MarkovProcess.ContinuousPath.exitTime (OnePoint.some '' wholeSpaceCube d v)
path ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑x = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeExitFunction v ↑x
The expected exit time from a centered exhaustion cube is its analytic zero-shift Dirichlet limit.
theorem
DivergenceFormProcess.Form.WholeSpaceAnalyticData.lintegral_exitTime_lt_top_stream
{d : ℕ}
[NeZero d]
{M : Algsuperdiff.Section3.ABKModel d}
{omega : Algsuperdiff.Section5.Field.FullSample d M.gamma}
(R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d))
(hreg : R.OnePointRegular)
(hcons : R.kernelSemigroup.IsConservative)
(hid : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R)
(hT :
∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ),
(R.operator mu) g = (⋯.resolvent.operator mu) g)
(v : ℕ)
{x : HCPolySupport.Vec d}
(hx : x ∈ wholeSpaceCube d v)
:
The expected exit time from a centered exhaustion cube is finite for the stream-field process.