CruxStreamGeneralDomain

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

S-free crux comparison on bounded part domains

The localized stream tail works on any bounded part domain after embedding it in a centered exhaustion cube. This extends the stream crux equality from the centered cubes to every open bounded convex part domain.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.iInf_toReal_analyticPenalizedResolvent_le_of_isRepresentative_of_error {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (v : ℕ) (hVcube : V ⊆ wholeSpaceCube d v) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 < D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {u : HCPolySupport.Vec d → ℝ} (hucont : ContinuousOn u V) (hurep : u =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 hV hf hfD)))) {x : HCPolySupport.Vec d} (hx : x ∈ V) (error : ℕ → ℝ) (herror : Filter.Tendsto error Filter.atTop (nhds 0)) (hcompare : ∀ᶠ (n : ℕ) in Filter.atTop, (A.analyticPenalizedResolvent ⋯ n mu f hf hfD x).toReal ≤ A.analyticPenalizedCubeResolvent ⋯ n mu f hf hfD (v + 1) x + error n) : ⨅ (n : ℕ), (A.analyticPenalizedResolvent ⋯ n mu f hf hfD x).toReal ≤ u x

A vanishing-error exterior-penalization interchange on a bounded part domain.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.iInf_toReal_analyticPenalizedResolvent_le_utilde_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)) {D : ℝ} (hD : 0 < D) (hfD : ∀ (y : HCPolySupport.Vec d), |P.f y| ≤ D) {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 localized stream tail gives the penalization upper bound on every bounded part domain.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_le_partResolvent_stream_general {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) {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 comparison on every bounded part domain.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_eq_partResolvent_stream_general {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) {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 crux equality on every open bounded convex part domain.