Exponential comparison under resolvent generation

A pointwise exponential supersolution estimate for every sufficiently large normalized positive resolvent passes through the Poisson representation of the Yosida approximants and then through their strong limit to the generated semigroup. The represented kernel semigroup inherits the same comparison for C₀ observables.

Public declarations:

• PositiveC0ContractiveResolvent.generatedSemigroup_apply_le_exp_mul;
• PositiveC0ContractiveResolvent.integral_kernelSemigroup_le_exp_mul.

No comparison for indicators of arbitrary measurable sets is asserted.

theorem MarkovProcess.PositiveC0ContractiveResolvent.generatedSemigroup_apply_le_exp_mul {X : Type u_1} [TopologicalSpace X] (R : PositiveC0ContractiveResolvent X) (theta : ℝ) (v : ZeroAtInftyContinuousMap X ℝ) (hR : ∀ (mu : ↑Semigroup.PositiveShift), theta < ↑mu → ∀ (x : X), ↑mu * ((R.operator mu) v) x ≤ ↑mu / (↑mu - theta) * v x) (t : NNReal) (x : X) : ((R.generatedSemigroup.operator t) v) x ≤ Real.exp (theta * ↑t) * v x

Exponential comparison is stable under resolvent generation. A pointwise supersolution estimate for every normalized resolvent above theta passes to the canonical semigroup generated by the resolvent.

theorem MarkovProcess.PositiveC0ContractiveResolvent.integral_kernelSemigroup_le_exp_mul {X : Type u_1} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (R : PositiveC0ContractiveResolvent X) (theta : ℝ) (v : ZeroAtInftyContinuousMap X ℝ) (hR : ∀ (mu : ↑Semigroup.PositiveShift), theta < ↑mu → ∀ (x : X), ↑mu * ((R.operator mu) v) x ≤ ↑mu / (↑mu - theta) * v x) (f : ZeroAtInftyContinuousMap X ℝ) (hfv : ∀ (x : X), f x ≤ v x) (t : NNReal) (x : X) : ∫ (y : X), f y ∂(R.kernelSemigroup.kernel t) x ≤ Real.exp (theta * ↑t) * v x

The represented kernel semigroup inherits the generated semigroup's exponential comparison for every C₀ observable below the supersolution.