CruxStreamEquality

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

Killed-resolvent equality for the stream field

The coefficient-dependent lower input is the stream field's WholeSpaceC0BarrierData; the upper input is its localized split-skew fixed-collar penalization estimate. Thus no global small-contrast datum is present. The operator identification is stated against the C₀ operator carried by the barrier structure.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_eq_partResolvent_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (P : WholeSpaceBarrierData (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega)) (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 : ℕ) (hVcube : P.V = wholeSpaceCube d v) {x : HCPolySupport.Vec d} (hx : x ∈ P.V) : 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 = ENNReal.ofReal (P.utilde x)

S-free stream crux equality. On an exhaustion cube, the resolvent of the whole-space stream process killed on leaving the compactified part domain equals the continuous representative of the part resolvent.