Resolvents of kernel semigroups

This file defines the resolvent of a sub-Markov kernel semigroup on nonnegative extended-real observables by Laplace transformation of its transition kernels.

Main definitions: SubMarkovKernelSemigroup.kernelResolvent and SubMarkovKernelSemigroup.kernelResolventReal.

No conservativity, topology, or finiteness of the resolvent is asserted.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) (f : alpha → ENNReal) (x : alpha) : ENNReal

The kernel resolvent on nonnegative extended-real observables.

Equations

• P.kernelResolvent lam f x = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-lam * t)) * ∫⁻ (y : alpha), f y ∂(P.kernel t.toNNReal) x

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.kernelResolventReal {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) (f : alpha → ℝ) (x : alpha) : ℝ

The kernel resolvent on real-valued observables. Finiteness is established separately for bounded observables at positive shifts.

Equations

• P.kernelResolventReal lam f x = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-lam * t) * MarkovProcess.kernelIntegral (P.kernel t.toNNReal) f x

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolventReal_add {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) {f g : alpha → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (y : alpha), |f y| ≤ D) (hgE : ∀ (y : alpha), |g y| ≤ E) : P.kernelResolventReal lam (f + g) = P.kernelResolventReal lam f + P.kernelResolventReal lam g

The real kernel resolvent is additive on bounded measurable observables.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolventReal_smul {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam a : ℝ) (f : alpha → ℝ) : P.kernelResolventReal lam (a • f) = a • P.kernelResolventReal lam f

The real kernel resolvent is real homogeneous.

theorem MarkovProcess.SubMarkovKernelSemigroup.norm_kernelResolventReal_le {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) {f : alpha → ℝ} {D : ℝ} (hfD : ∀ (y : alpha), |f y| ≤ D) (x : alpha) : |P.kernelResolventReal lam f x| ≤ D / lam

The uniform bound for the real kernel resolvent of a bounded observable at a positive shift.