CruxUpperKernelBridge

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

From the kernel resolvent to the analytic minimal resolvent

The comparison family of the process layer is compared with the real kernel resolvent of the compactified semigroup. This module records the three translations needed for that comparison: the real kernel resolvent of a nonnegative bounded observable is the real value of its extended-real kernel resolvent; at the added point the kernel resolvent reads only the value of the observable there; and at a live point, for a conservative live semigroup, it is the real analytic minimal resolvent of the restricted observable.

The last translation is the named identification hypothesis of the analytic layer, normalized to observables bounded by one, so it is used through a rescaling.

theorem DivergenceFormProcess.Form.kernelResolventReal_nonneg {alpha : Type u_1} [MeasurableSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (lam : ℝ) {f : alpha → ℝ} (hf0 : ∀ (y : alpha), 0 ≤ f y) (x : alpha) : 0 ≤ P.kernelResolventReal lam f x

The real kernel resolvent of a nonnegative observable is nonnegative.

theorem DivergenceFormProcess.Form.ofReal_kernelResolventReal_eq_kernelResolvent {alpha : Type u_1} [MeasurableSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) {f : alpha → ℝ} (hf : Measurable f) (hf0 : ∀ (y : alpha), 0 ≤ f y) {D : ℝ} (hfD : ∀ (y : alpha), |f y| ≤ D) (x : alpha) : ENNReal.ofReal (P.kernelResolventReal lam f x) = P.kernelResolvent lam (fun (y : alpha) => ENNReal.ofReal (f y)) x

On nonnegative bounded measurable observables the real kernel resolvent is the real value of the extended-real kernel resolvent.

theorem DivergenceFormProcess.Form.kernelResolventReal_eq_toReal_kernelResolvent {alpha : Type u_1} [MeasurableSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) {f : alpha → ℝ} (hf : Measurable f) (hf0 : ∀ (y : alpha), 0 ≤ f y) {D : ℝ} (hfD : ∀ (y : alpha), |f y| ≤ D) (x : alpha) : P.kernelResolventReal lam f x = (P.kernelResolvent lam (fun (y : alpha) => ENNReal.ofReal (f y)) x).toReal

The real kernel resolvent of a nonnegative bounded measurable observable is the real value of the extended-real one.

theorem DivergenceFormProcess.Form.onePointKernelResolventReal_infty {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (lam : ℝ) {G : OnePoint (HCPolySupport.Vec d) → ℝ} (hG : Measurable G) : R.onePointKernelSemigroup.kernelResolventReal lam G OnePoint.infty = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-lam * t) * G OnePoint.infty

At the added point the real kernel resolvent of the one-point extension reads only the value of the observable there.

theorem DivergenceFormProcess.Form.onePointKernelResolventReal_infty_eq_zero {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (lam : ℝ) {G : OnePoint (HCPolySupport.Vec d) → ℝ} (hG : Measurable G) (hGzero : G OnePoint.infty = 0) : R.onePointKernelSemigroup.kernelResolventReal lam G OnePoint.infty = 0

An observable vanishing at the added point has vanishing real kernel resolvent there.

theorem DivergenceFormProcess.Form.onePointKernelResolventReal_coe {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hcons : R.kernelSemigroup.IsConservative) (lam : ℝ) {G : OnePoint (HCPolySupport.Vec d) → ℝ} (hG : Measurable G) (x : HCPolySupport.Vec d) : R.onePointKernelSemigroup.kernelResolventReal lam G ↑x = R.kernelSemigroup.kernelResolventReal lam (fun (y : HCPolySupport.Vec d) => G ↑y) x

At a live point the real kernel resolvent of the one-point extension of a conservative semigroup is the real kernel resolvent of the restricted observable.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.kernelResolvent_eq_analyticMinimalResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hid : A.KernelResolventIdentifiesAnalyticMinimal R) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : R.kernelSemigroup.kernelResolvent (↑mu) (fun (y : HCPolySupport.Vec d) => ENNReal.ofReal (f y)) x = A.analyticMinimalResolvent mu f hf hfD x

The kernel resolvent of a nonnegative bounded observable is the analytic minimal resolvent. The named identification hypothesis is normalized to observables bounded by one, so the datum is rescaled by a positive bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.kernelResolventReal_eq_analyticMinimalResolventReal {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) (hid : A.KernelResolventIdentifiesAnalyticMinimal R) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : R.kernelSemigroup.kernelResolventReal (↑mu) f x = A.analyticMinimalResolventReal mu f hf hfD x

The real kernel resolvent is the signed real analytic minimal resolvent on signed bounded measurable observables.