CruxUpperProcess

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

The process-side upper resolvent comparison

The exterior penalization dominates the killed resolvent at every penalization index, and the penalization limit on the target cube is the part resolvent. Consequently the resolvent of the whole-space process killed on leaving the part domain is at most the continuous representative of the part resolvent.

theorem DivergenceFormProcess.Form.ofReal_onePointRealExtension_eq_onePointLiveExtension {d : ℕ} (f : HCPolySupport.Vec d → ℝ) : (fun (z : OnePoint (HCPolySupport.Vec d)) => ENNReal.ofReal (onePointRealExtension f z)) = MarkovProcess.PositiveC0ContractiveResolvent.onePointLiveExtension fun (y : HCPolySupport.Vec d) => ENNReal.ofReal (f y)

The extended-real zero extension of a nonnegative observable is the live extension of its extended-real form. Both vanish at the added point.

theorem DivergenceFormProcess.Form.eq_analyticCubeResolvent_of_isRepresentative {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (lam : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (y : HCPolySupport.Vec d), |f y| ≤ D) {u : HCPolySupport.Vec d → ℝ} (hucont : Continuous u) (hurep : u =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑(ZeroTraceSobolev.toL2 ((alphaShiftedSolution A.a ⋯ ⋯ ⋯) (partDatumL2 hV hf hfD)))) (v : ℕ) (hVcube : V = wholeSpaceCube d v) {x : HCPolySupport.Vec d} (hx : x ∈ V) : u x = A.analyticCubeResolvent lam f hf hfD v x

The continuous zero extension of the part solution is the analytic cube resolvent on the cube. Both are continuous there and represent the same shifted Dirichlet solution.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.killedResolvent_le_ofReal_of_iInf_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hreg : R.OnePointRegular) (hcons : R.kernelSemigroup.IsConservative) (hid : A.KernelResolventIdentifiesAnalyticMinimal R) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (y : HCPolySupport.Vec d), |P.f y| ≤ D) {x : HCPolySupport.Vec d} {c : ℝ} (hc : ⨅ (n : ℕ), (A.analyticPenalizedResolvent ⋯ n P.lam P.f ⋯ hfD x).toReal ≤ c) : 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 c

The penalization bound for the killed resolvent. The resolvent of the whole-space process killed on leaving the compactified image of the part domain is at most any real upper bound for the infimum of the exterior- penalized resolvents. The domination at each penalization index is the Feynman-Kac comparison of the process layer; the bound itself is the analytic input, supplied by the caller.