Potential measures

The resolvent of a transition family at a shift lam integrates an observable against the exponentially weighted time average of its transition kernels. This file realises that average as a genuine measure, the lam-potential measure

laplacePotential lam mu = ∫_0^∞ e^{-lam t} (mu t) dt,

so that both the kernel resolvent of a sub-Markov kernel semigroup and the killed resolvent of an open set are integrals against a measure on the state space: SubMarkovKernelSemigroup.lintegral_resolventPotential and IsConservative.lintegral_killedPotential. Potential measures of sub-Markov families are finite at every positive shift, with total mass at most 1 / lam.

Two consequences of the measure form are proved here: the killed resolvent is monotone in the open set and in the observable (IsConservative.killedResolvent_mono), and the kernel resolvent is measurable in the starting point and continuous along monotone limits of observables (SubMarkovKernelSemigroup.measurable_kernelResolvent, SubMarkovKernelSemigroup.kernelResolvent_iSup). The kernel resolvent is also additive and homogeneous on measurable observables (SubMarkovKernelSemigroup.kernelResolvent_add, SubMarkovKernelSemigroup.kernelResolvent_const_mul).

No resolvent identity and no topology on the state space are used here.

noncomputable def MarkovProcess.laplaceWeight (lam : ℝ) : MeasureTheory.Measure ℝ

The exponentially weighted measure on positive times at the shift lam.

Equations

• MarkovProcess.laplaceWeight lam = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (Real.exp (-lam * t))

theorem MarkovProcess.measurable_laplaceDensity (lam : ℝ) : Measurable fun (t : ℝ) => ENNReal.ofReal (Real.exp (-lam * t))

The exponential weight is measurable in time.

theorem MarkovProcess.lintegral_laplaceWeight (lam : ℝ) {g : ℝ → ENNReal} (hg : Measurable g) : ∫⁻ (t : ℝ), g t ∂laplaceWeight lam = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-lam * t)) * g t

Integration against the exponentially weighted time measure.

theorem MarkovProcess.laplaceWeight_univ {lam : ℝ} (hlam : 0 < lam) : (laplaceWeight lam) Set.univ = ENNReal.ofReal lam⁻¹

At a positive shift the exponentially weighted time measure has total mass 1 / lam.

theorem MarkovProcess.isFiniteMeasure_laplaceWeight {lam : ℝ} (hlam : 0 < lam) : MeasureTheory.IsFiniteMeasure (laplaceWeight lam)

At a positive shift the exponentially weighted time measure is finite.

noncomputable def MarkovProcess.laplacePotential {alpha : Type u_1} [MeasurableSpace alpha] (lam : ℝ) (mu : ℝ → MeasureTheory.Measure alpha) : MeasureTheory.Measure alpha

The lam-potential measure of a measurable family of transition measures: the exponentially weighted time average of the family.

Equations

• MarkovProcess.laplacePotential lam mu = (MarkovProcess.laplaceWeight lam).bind mu

theorem MarkovProcess.lintegral_laplacePotential {alpha : Type u_1} [MeasurableSpace alpha] (lam : ℝ) {mu : ℝ → MeasureTheory.Measure alpha} (hmu : Measurable mu) {f : alpha → ENNReal} (hf : Measurable f) : ∫⁻ (y : alpha), f y ∂laplacePotential lam mu = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-lam * t)) * ∫⁻ (y : alpha), f y ∂mu t

Integration against a potential measure is the Laplace transform in time of the integrals against the family.

theorem MarkovProcess.laplacePotential_univ_le {alpha : Type u_1} [MeasurableSpace alpha] {lam : ℝ} (hlam : 0 < lam) {mu : ℝ → MeasureTheory.Measure alpha} (hmu : Measurable mu) (hmass : ∀ (t : ℝ), (mu t) Set.univ ≤ 1) : (laplacePotential lam mu) Set.univ ≤ ENNReal.ofReal lam⁻¹

A potential measure of a family of sub-probability measures has mass at most 1 / lam.

theorem MarkovProcess.isFiniteMeasure_laplacePotential {alpha : Type u_1} [MeasurableSpace alpha] {lam : ℝ} (hlam : 0 < lam) {mu : ℝ → MeasureTheory.Measure alpha} (hmu : Measurable mu) (hmass : ∀ (t : ℝ), (mu t) Set.univ ≤ 1) : MeasureTheory.IsFiniteMeasure (laplacePotential lam mu)

A potential measure of a family of sub-probability measures is finite at a positive shift.

theorem MarkovProcess.SubMarkovKernelSemigroup.measurable_toMeasure_toNNReal {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (x : alpha) : Measurable fun (t : ℝ) => (P.kernel t.toNNReal) x

The transition measures of a sub-Markov kernel semigroup are measurable in time.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.resolventPotential {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) (x : alpha) : MeasureTheory.Measure alpha

The lam-potential measure of a sub-Markov kernel semigroup started at x.

Equations

• P.resolventPotential lam x = MarkovProcess.laplacePotential lam fun (t : ℝ) => (P.kernel t.toNNReal) x

theorem MarkovProcess.SubMarkovKernelSemigroup.lintegral_resolventPotential {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) (x : alpha) : ∫⁻ (y : alpha), f y ∂P.resolventPotential lam x = P.kernelResolvent lam f x

The kernel resolvent is integration against the potential measure.

theorem MarkovProcess.SubMarkovKernelSemigroup.isFiniteMeasure_resolventPotential {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) (x : alpha) : MeasureTheory.IsFiniteMeasure (P.resolventPotential lam x)

The potential measure of a sub-Markov kernel semigroup is finite at a positive shift.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent_one_le {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) (x : alpha) : P.kernelResolvent lam (fun (x : alpha) => 1) x ≤ ENNReal.ofReal lam⁻¹

At a positive shift the kernel resolvent of the constant observable one is at most 1 / lam.

theorem MarkovProcess.SubMarkovKernelSemigroup.ofReal_mul_resolventPotential_le_one {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) {lam : ℝ} (hlam : 0 < lam) (x : alpha) (s : Set alpha) : ENNReal.ofReal lam * (P.resolventPotential lam x) s ≤ 1

The normalized potential mass of any set is at most one. At a positive shift the lam-potential measure of a sub-Markov kernel semigroup has total mass at most 1 / lam, so the normalization by lam used in the resolvent tail estimates is a sub-probability.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent_mono {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) {f g : alpha → ENNReal} (hfg : f ≤ g) (x : alpha) : P.kernelResolvent lam f x ≤ P.kernelResolvent lam g x

The kernel resolvent is monotone in the observable.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent_add {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) {f g : alpha → ENNReal} (hf : Measurable f) (x : alpha) : P.kernelResolvent lam (fun (y : alpha) => f y + g y) x = P.kernelResolvent lam f x + P.kernelResolvent lam g x

The kernel resolvent is additive on measurable observables.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent_const_mul {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) (c : ENNReal) {f : alpha → ENNReal} (hf : Measurable f) (x : alpha) : P.kernelResolvent lam (fun (y : alpha) => c * f y) x = c * P.kernelResolvent lam f x

The kernel resolvent is homogeneous under multiplication by an extended-real constant.

theorem MarkovProcess.SubMarkovKernelSemigroup.measurable_kernelResolvent {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) : Measurable fun (x : alpha) => P.kernelResolvent lam f x

The kernel resolvent is measurable in the starting point.

theorem MarkovProcess.SubMarkovKernelSemigroup.kernelResolvent_iSup {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (lam : ℝ) {f : ℕ → alpha → ENNReal} (hf : ∀ (n : ℕ), Measurable (f n)) (hmono : Monotone f) (x : alpha) : P.kernelResolvent lam (fun (y : alpha) => ⨆ (n : ℕ), f n y) x = ⨆ (n : ℕ), P.kernelResolvent lam (f n) x

The kernel resolvent is continuous along monotone limits of observables.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.measurable_killedKernel_toNNReal {alpha : Type u_1} [MeasurableSpace alpha] [MetricSpace alpha] [CompleteSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (x : alpha) : Measurable fun (t : ℝ) => (killedKernel P hP U hU t.toNNReal) x

The killed transition kernels are measurable in time.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedPotential {alpha : Type u_1} [MeasurableSpace alpha] [MetricSpace alpha] [CompleteSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (lam : ℝ) (x : alpha) : MeasureTheory.Measure alpha

The lam-potential measure of the process killed at the exit of U, started at x.

Equations

• One or more equations did not get rendered due to their size.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.lintegral_killedPotential {alpha : Type u_1} [MeasurableSpace alpha] [MetricSpace alpha] [CompleteSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) (lam : ℝ) {f : alpha → ENNReal} (hf : Measurable f) (x : alpha) : ∫⁻ (y : alpha), f y ∂killedPotential P hP U hU lam x = killedResolvent P hP U hU lam f x

The killed resolvent is integration against the killed potential measure.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.isFiniteMeasure_killedPotential {alpha : Type u_1} [MeasurableSpace alpha] [MetricSpace alpha] [CompleteSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) {lam : ℝ} (hlam : 0 < lam) (x : alpha) : MeasureTheory.IsFiniteMeasure (killedPotential P hP U hU lam x)

The killed potential measure is finite at a positive shift.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.killedResolvent_mono {alpha : Type u_1} [MeasurableSpace alpha] [MetricSpace alpha] [CompleteSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (U : Set alpha) (hU : IsOpen U) {V : Set alpha} (hV : IsOpen V) (hUV : U ⊆ V) (lam : ℝ) {f g : alpha → ENNReal} (hfg : f ≤ g) (x : alpha) : killedResolvent P hP U hU lam f x ≤ killedResolvent P hP V hV lam g x

The killed resolvent is monotone in the open set and in the observable. A path leaves a larger set no earlier, so the killed transition kernels increase with the set.