Process

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

The whole-space continuous process from resolvent tails

This module constructs the continuous process from an explicit resolvent-tail input. The main construction uses the exhaustion metric on the one-point compactification. It therefore accepts the localized split-skew route for coefficients a = nu I + ks + kl with logarithmic local bounds and a finite cubic layer-cake tail budget. Conservativity shows that a process started in the whole space almost surely never reaches the added point.

The construction is generic over the exhaustion function and tail profile. The scale-free small-contrast tail supplies the first analytic instance; the localized split-skew tail can replace it without changing the process API.

noncomputable def DivergenceFormProcess.Form.onePointProcess {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (hreg : R.OnePointRegular) : ProbabilityTheory.Kernel (OnePoint (HCPolySupport.Vec d)) (MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)))

The canonical process on a one-point regularity witness.

Equations

• DivergenceFormProcess.Form.onePointProcess hreg = MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess R.onePointKernelSemigroup ⋯

theorem DivergenceFormProcess.Form.onePointProcess_spec {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (hreg : R.OnePointRegular) : ProbabilityTheory.IsMarkovKernel (onePointProcess hreg) ∧ ∀ (I : Finset NNReal), (onePointProcess hreg).map (MarkovProcess.ContinuousPath.finsetEvaluation I) = R.onePointKernelSemigroup.finiteSetKernel I

The canonical process is Markov and has the finite-dimensional distributions of the represented one-point kernel semigroup.

theorem DivergenceFormProcess.Form.onePointProcess_ae_stays_live {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (x : HCPolySupport.Vec d) : ∀ᵐ (omega : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂(onePointProcess hreg) ↑x, MarkovProcess.ContinuousPath.exitTime (Set.range OnePoint.some) omega = ⊤

Under live-space conservativity, the canonical process started at a live point almost surely never reaches the added point.

noncomputable def DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput.wholeSpaceProcess {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (H : WholeSpaceVariableExhaustionResolventTailInput R) : have hreg := H.toOnePointRegular; ProbabilityTheory.Kernel (OnePoint (HCPolySupport.Vec d)) (MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)))

The whole-space process supplied by a shift-dependent exhaustion-tail input.

Equations

• H.wholeSpaceProcess = DivergenceFormProcess.Form.onePointProcess H.toOnePointRegular

theorem DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput.wholeSpaceProcess_spec {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (H : WholeSpaceVariableExhaustionResolventTailInput R) : have hreg := H.toOnePointRegular; ProbabilityTheory.IsMarkovKernel H.wholeSpaceProcess ∧ ∀ (I : Finset NNReal), ProbabilityTheory.Kernel.map H.wholeSpaceProcess (MarkovProcess.ContinuousPath.finsetEvaluation I) = R.onePointKernelSemigroup.finiteSetKernel I

The variable-tail whole-space process is Markov and has the represented one-point kernel semigroup's finite-dimensional distributions.

theorem DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput.wholeSpaceProcess_ae_stays_live {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (H : WholeSpaceVariableExhaustionResolventTailInput R) (hcons : R.kernelSemigroup.IsConservative) (x : HCPolySupport.Vec d) : have hreg := H.toOnePointRegular; ∀ᵐ (omega : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d))) ∂H.wholeSpaceProcess ↑x, MarkovProcess.ContinuousPath.exitTime (Set.range OnePoint.some) omega = ⊤

Under conservativity, the variable-tail process started at a live point almost surely never reaches the added point.