{A : ℕ → H →L[ℂ] H} {Alim : H →L[ℂ] H} (hA : ∀ n, IsSelfAdjoint (A n)) (hlim : IsSelfAdjoint Alim) (hconv : ∀ u : H, Tendsto (fun n => A n u) atTop (𝓝 (Alim u))) :...

-- Generated from ChapterSirkTrotterKatoGalerkin.lean — theorem BookProof.ChapterSirkTrotterKato.strongResolventConvergence_ofBounded
import Mathlib
import Definitions.Def_ChapterSirkTrotterKatoGalerkin
open BookProof.ChapterSirkTrotterKato








noncomputable section

open Filter Topology


open BookProof.ChapterStoneResolvent BookProof.ChapterUnitaryTransport

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

theorem BookProof.ChapterSirkTrotterKato.strongResolventConvergence_ofBounded {A : ℕ → H →L[ℂ] H} {Alim : H →L[ℂ] H}
    (hA : ∀ n, IsSelfAdjoint (A n)) (hlim : IsSelfAdjoint Alim)
    (hconv : ∀ u : H, Tendsto (fun n => A n u) atTop (𝓝 (Alim u))) :
    StrongResolventConvergence (ofBounded Alim hlim) (fun n => ofBounded (A n) (hA n)) := by sorry