ResolventDenseRange

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

Dense range from normalized resolvent convergence

This module isolates the elementary implication from the resolvent identity and strong normalization at large positive shifts to dense range at every fixed shift.

theorem DivergenceFormProcess.Semigroup.denseRange_of_resolvent_identity_of_tendsto_scaled {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : ↑MarkovProcess.Semigroup.PositiveShift → E →L[ℝ] E) (hRI : ∀ (α β : ↑MarkovProcess.Semigroup.PositiveShift), R α - R β = (↑β - ↑α) • R α ∘SL R β) (hN : ∀ (f : E), Filter.Tendsto (fun (α : ↑MarkovProcess.Semigroup.PositiveShift) => ↑α • (R α) f) Filter.atTop (nhds f)) (μ : ↑MarkovProcess.Semigroup.PositiveShift) : DenseRange ⇑(R μ)

A resolvent family whose normalized operators converge pointwise to the identity has dense range at every positive shift.