CruxStreamMeanValueCubeSetAt

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

The exit decomposition on a translated triadic cube for the stream field

The exit decomposition of ExitMeanValueCubeSetAtProcess.lean carries a global small-contrast datum, because the crux equality it invokes does. The stream field of the model supplies no such datum, and the coefficient-generic C₀ barrier comparison replaces it. This file is the small-contrast-free copy of that decomposition on cubeSetAt y n: the same four statements, with the small-contrast datum removed from every hypothesis list and the analytic data fixed to the stream field of the model.

The assumptions are those of the coefficient-generic comparison: the resolvent carrying the process, its one-point regularity data, conservativity of the live kernel semigroup, the bounded-measurable identification of the kernel resolvent with the analytic minimal resolvent, and the operator identification against the C₀ barrier resolvent of the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.killedResolvent_eq_cubeSetAtC0Resolvent_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (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) (y : HCPolySupport.Vec d) (n : ℤ) {lam : ℝ} (hlam : 0 < lam) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) ⋯ lam (MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension fun (z : HCPolySupport.Vec d) => ENNReal.ofReal (g z)) ↑x = ENNReal.ofReal ((Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtC0Resolvent y n g lam x)

The killed resolvent of a continuous datum on a translated triadic cube for the stream field. No small-contrast datum appears.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.operator_eq_cubeSetAtC0Resolvent_add_discountedExitAverage_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (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) (y : HCPolySupport.Vec d) (n : ℤ) {lam : ℝ} (hlam : 0 < lam) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : ((R.operator ⟨lam, hlam⟩) g) x = (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtC0Resolvent y n g lam x + StoppedDirichlet.discountedExitAverage R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) lam (onePointRealExtension fun (z : HCPolySupport.Vec d) => ((R.operator ⟨lam, hlam⟩) g) z) ↑x

The exit decomposition at a positive shift on a translated triadic cube for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.discountedExitAverage_eq_sub_add_cubeSetAt_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (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) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) {lam : ℝ} (hlam : 0 < lam) {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : StoppedDirichlet.discountedExitAverage R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) lam (onePointRealExtension fun (z : HCPolySupport.Vec d) => ((R.operator mu) g) z) ↑x = ((R.operator mu) g) x - (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtC0Resolvent y n g lam x + (↑mu - lam) * (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).cubeSetAtC0Resolvent y n ((R.operator mu) g) lam x

The discounted exit average of a resolvent datum on a translated triadic cube for the stream field.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasExitMeanValueOn_of_isCubeSetAtResolventHarmonicPart_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (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) (y : HCPolySupport.Vec d) (n : ℤ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hg0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ g z) {h : HCPolySupport.Vec d → ℝ} (hh : (Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData M omega).IsCubeSetAtResolventHarmonicPart R y n mu g h) (hwfin : ∀ z ∈ Algsuperdiff.Section5.Support.cubeSetAt y n, StoppedDirichlet.expectedExitTime R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) ↑z ≠ ⊤) : StoppedDirichlet.HasExitMeanValueOn R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) (onePointRealExtension h)

The harmonic part of a stream resolvent datum on a translated triadic cube is represented by the exit distribution.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.expectedExitTime_cubeSetAt_ne_top_stream {d : ℕ} [NeZero d] {M : Algsuperdiff.Section3.ABKModel d} {omega : Algsuperdiff.Section5.Field.FullSample d M.gamma} (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) (y : HCPolySupport.Vec d) (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ Algsuperdiff.Section5.Support.cubeSetAt y n) : StoppedDirichlet.expectedExitTime R.onePointKernelSemigroup ⋯ (OnePoint.some '' Algsuperdiff.Section5.Support.cubeSetAt y n) ↑x ≠ ⊤

The expected exit time from a translated triadic cube is finite for the stream-field process.