CruxStreamLower

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

S-free lower process comparison

The excessive-barrier stopping argument is repeated with WholeSpaceC0BarrierData in place of global small contrast. Its explicit inputs are vanishing and dense range for the analytic minimal C₀ resolver, compact-data vanishing for the barrier, the ordinary axis-cube barrier data with its continuity witnesses, kernel identification, and the C₀ operator identification. No global coefficient-contrast hypothesis is used.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_ge_partResolvent_wholeSpace_of_c0Barrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (B : WholeSpaceC0BarrierData A) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hid : A.KernelResolventIdentifiesAnalyticMinimal R) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = A.analyticMinimalC0ResolventOfVanishing ⋯ mu g) {x : HCPolySupport.Vec d} (hx : x ∈ P.V) : ENNReal.ofReal (P.utilde x) ≤ MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent R.onePointKernelSemigroup ⋯ (OnePoint.some '' P.V) ⋯ (↑P.lam) (MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension fun (y : HCPolySupport.Vec d) => ENNReal.ofReal (P.f y)) ↑x

S-free lower process comparison. The process killed on leaving the compactified part domain dominates the continuous part-resolvent representative. All coefficient-dependent C₀ inputs are carried by B; the general global-small-contrast case is not asserted.