CruxStreamUpper

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

Process upper comparison for the stream field

This module propagates the localized split-skew penalization interchange to the process killed resolvent. It is an S-free successor under distinct names; the existing small-contrast declarations remain unchanged.

theorem DivergenceFormProcess.Form.iInf_toReal_streamAnalyticPenalizedResolvent_le_analyticCubeResolvent {d : ℕ} [NeZero d] (M : Algsuperdiff.Section3.ABKModel d) (omega : Algsuperdiff.Section5.Field.FullSample d M.gamma) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (y : HCPolySupport.Vec d), 0 ≤ f y) {D : ℝ} (hD : 0 < D) (hfD : ∀ (y : HCPolySupport.Vec d), |f y| ≤ D) (v : ℕ) (hVcube : V = wholeSpaceCube d v) (hsupp : ∀ᵐ (y : HCPolySupport.Vec d), y ∉ wholeSpaceCube d v → f y = 0) {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) : ⨅ (n : ℕ), ((Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).analyticPenalizedResolvent hV n lam f hf hfD x).toReal ≤ (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).analyticCubeResolvent lam f hf hfD v x

The stream penalization interchange read through an equality identifying the part domain with an exhaustion cube.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.iInf_toReal_streamAnalyticPenalizedResolvent_le_utilde {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (P : WholeSpaceBarrierData (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega)) {D : ℝ} (hD : 0 < D) (hfD : ∀ (y : HCPolySupport.Vec d), |P.f y| ≤ D) (v : ℕ) (hVcube : P.V = wholeSpaceCube d v) {x : HCPolySupport.Vec d} (hx : x ∈ P.V) : ⨅ (n : ℕ), ((Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).analyticPenalizedResolvent ⋯ n P.lam P.f ⋯ hfD x).toReal ≤ P.utilde x

The stream penalization limit is bounded by the continuous representative of the part resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_le_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) (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 upper stream-process comparison. The killed resolvent of any identified conservative C0 process is bounded by the part resolvent. The analytic input is the localized split-skew fixed-collar estimate.