CruxStreamMeanValueIdentification

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

S-free identification of stream-field exit mean values

This module identifies the analytic harmonic parts used by the S-free stream mean-value chain and supplies its smooth-boundary consumer. The declarations use the stream field's coefficient and WholeSpaceC0BarrierData; they do not assume a global small-contrast datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.operator_eq_analyticMinimalResolventReal_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hT : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ), (R.operator mu) g = (⋯.resolvent.operator mu) g) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (y : HCPolySupport.Vec d) : ((R.operator mu) g) y = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).analyticMinimalResolventReal mu ⇑g ⋯ ⋯ y

The stream process resolvent agrees pointwise with the analytic minimal resolvent, without a global small-contrast assumption.