CruxStreamCube #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
S-free translated-cube exit identities for the stream process #
theorem
DivergenceFormProcess.Form.WholeSpaceAnalyticData.killedResolvent_one_eq_cubeSetAtOneResolvent_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)
(y : HCPolySupport.Vec d)
(n : ℤ)
{lam : ℝ}
(hlam : 0 < lam)
{x : HCPolySupport.Vec d}
(hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n)
:
MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent R.onePointKernelSemigroup ⋯
(OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) ⋯ lam (fun (x : OnePoint (HCPolySupport.Vec d)) => 1)
↑x = ENNReal.ofReal
((Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtOneResolvent y n ⟨lam, hlam⟩ x)
The killed stream resolvent of one on a translated triadic cube is its continuous Dirichlet resolvent.
theorem
DivergenceFormProcess.Form.WholeSpaceAnalyticData.lintegral_exitTime_eq_cubeSetAtExitFunction_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)
(y : HCPolySupport.Vec d)
(n : ℤ)
{x : HCPolySupport.Vec d}
(hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n)
:
∫⁻ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))), MarkovProcess.ContinuousPath.exitTime (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n)
path ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯) ↑x = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtExitFunction y n ↑x
The expected exit time from a translated triadic cube is the zero-shift limit of its Dirichlet resolvents of one.