Strong limits of Yosida approximations

This file constructs the canonical contraction obtained by taking the strong limit of the Yosida exponentials along the shifts n + 1. Continuity of its orbits is proved in Semigroup/Generation.lean, from the criterion of Semigroup/OrbitContinuity.lean.

def MarkovProcess.Semigroup.naturalShift (n : ℕ) : ↑PositiveShift

The canonical sequence of positive shifts, n + 1.

Equations

• MarkovProcess.Semigroup.naturalShift n = ⟨↑n + 1, ⋯⟩

@[simp]

theorem MarkovProcess.Semigroup.naturalShift_coe (n : ℕ) : ↑(naturalShift n) = ↑n + 1

theorem MarkovProcess.Semigroup.tendsto_naturalShift_atTop : Filter.Tendsto naturalShift Filter.atTop Filter.atTop

The canonical positive shifts tend to infinity.

theorem MarkovProcess.Semigroup.ContractiveResolvent.tendsto_yosidaGenerator_naturalShift_apply_operator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : ContractiveResolvent E) (mu : ↑PositiveShift) (y : E) : Filter.Tendsto (fun (n : ℕ) => (R.yosidaGenerator (naturalShift n)) ((R.operator mu) y)) Filter.atTop (nhds (↑mu • (R.operator mu) y - y))

Along the canonical shifts, Yosida generators converge on every fixed resolvent range.

theorem MarkovProcess.Semigroup.ContractiveResolvent.cauchySeq_yosidaGenerator_naturalShift_apply_operator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : ContractiveResolvent E) (mu : ↑PositiveShift) (y : E) : CauchySeq fun (n : ℕ) => (R.yosidaGenerator (naturalShift n)) ((R.operator mu) y)

Along the canonical shifts, Yosida generators are Cauchy on every fixed resolvent range.

theorem MarkovProcess.Semigroup.ContractiveResolvent.cauchySeq_yosidaOperator_naturalShift_apply_operator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (mu : ↑PositiveShift) (t : NNReal) (y : E) : CauchySeq fun (n : ℕ) => (R.yosidaOperator (naturalShift n) t) ((R.operator mu) y)

At a fixed time, the canonical Yosida exponentials are Cauchy on every fixed resolvent range.

noncomputable def MarkovProcess.Semigroup.ContractiveResolvent.yosidaOperatorSequence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : ContractiveResolvent E) (t : NNReal) : ℕ → E →L[ℝ] E

The canonical Yosida exponential sequence at a fixed time.

Equations

• R.yosidaOperatorSequence t n = R.yosidaOperator (MarkovProcess.Semigroup.naturalShift n) t

theorem MarkovProcess.Semigroup.ContractiveResolvent.norm_yosidaOperatorSequence_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (t : NNReal) (n : ℕ) : ‖R.yosidaOperatorSequence t n‖ ≤ 1

theorem MarkovProcess.Semigroup.ContractiveResolvent.cauchySeq_yosidaOperatorSequence_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (t : NNReal) (x : E) : CauchySeq fun (n : ℕ) => (R.yosidaOperatorSequence t n) x

noncomputable def MarkovProcess.Semigroup.ContractiveResolvent.yosidaStrongLimit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (t : NNReal) : E →L[ℝ] E

The canonical strong limit of the Yosida exponential approximants.

Equations

• R.yosidaStrongLimit t = MarkovProcess.Semigroup.strongOperatorLimit (R.yosidaOperatorSequence t) ⋯ ⋯

theorem MarkovProcess.Semigroup.ContractiveResolvent.tendsto_yosidaOperator_naturalShift_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (t : NNReal) (x : E) : Filter.Tendsto (fun (n : ℕ) => (R.yosidaOperator (naturalShift n) t) x) Filter.atTop (nhds ((R.yosidaStrongLimit t) x))

The canonical Yosida exponential approximants converge strongly.

theorem MarkovProcess.Semigroup.ContractiveResolvent.norm_yosidaStrongLimit_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (t : NNReal) : ‖R.yosidaStrongLimit t‖ ≤ 1

The canonical strong limit is a contraction.

@[simp]

theorem MarkovProcess.Semigroup.ContractiveResolvent.yosidaStrongLimit_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) : R.yosidaStrongLimit 0 = ContinuousLinearMap.id ℝ E

theorem MarkovProcess.Semigroup.ContractiveResolvent.yosidaStrongLimit_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (R : ContractiveResolvent E) (s t : NNReal) : R.yosidaStrongLimit (s + t) = R.yosidaStrongLimit s ∘SL R.yosidaStrongLimit t

The canonical strong limits satisfy the semigroup law.