StreamProcess

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

The continuous process of the stream field

This module gives names to the split-skew analytic resolvent, its variable exhaustion-tail input, and the resulting continuous-path process on the one-point compactification. Every object is assembled from the model data; there is no global small-contrast hypothesis.

noncomputable def Algsuperdiff.Section5.Field.streamWholeSpaceResolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)

The positive contractive C₀ resolvent assembled from the stream field's localized split-skew estimates.

Equations

• Algsuperdiff.Section5.Field.streamWholeSpaceResolvent M omega = Algsuperdiff.Section5.Field.streamAnalyticMinimalPositiveC0ContractiveResolvent M omega

noncomputable def Algsuperdiff.Section5.Field.streamExhaustionTailInput {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput (streamWholeSpaceResolvent M omega)

The stream resolvent's shift-dependent exhaustion-tail input.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section5.Field.streamProcess {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : have hreg := (streamExhaustionTailInput M omega).toOnePointRegular; ProbabilityTheory.Kernel (OnePoint (HCPolySupport.Vec d)) (MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)))

The continuous-path process associated with one realization of the stream field.

Equations

• Algsuperdiff.Section5.Field.streamProcess M omega = (Algsuperdiff.Section5.Field.streamExhaustionTailInput M omega).wholeSpaceProcess

theorem Algsuperdiff.Section5.Field.streamProcess_ae_stays_live {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : have hreg := (streamExhaustionTailInput M omega).toOnePointRegular; ∀ᵐ (path : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂(streamProcess M omega) ↑x, MarkovProcess.ContinuousPath.exitTime (Set.range OnePoint.some) path = ⊤

A stream process started at a live point almost surely remains in the whole space for all time.

Model-level stopped identities