KaplanskyStrongSequence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sequential Kaplansky approximation on a separable Hilbert space

Finite-vector Kaplansky approximation applied to increasing finite sets of dense vectors gives an actual strongly convergent sequence. Every source term satisfies the exact norm bound of the target operator.

theorem OAI.KadisonSimilarity.kaplansky_strong_sequence line 25

Source documentation

Every member of a represented bicommutant is a strong sequential limit of source elements, with the exact source norm bound preserved.

theorem kaplansky_strong_sequence
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ) :
    ∃ a : ℕ → A, (∀ n, ‖a n‖ ≤ ‖T‖) ∧
      ∀ x : H, Tendsto (fun n => σ (a n) x) atTop (𝓝 (T x)) := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.isometricExtension_strong_tendsto line 53

Source documentation

Strong convergence survives extension by zero to the common L² model.

theorem isometricExtension_strong_tendsto
    (J : H →ₗᵢ[ℂ] K) (T : ℕ → H →L[ℂ] H) (S : H →L[ℂ] H)
    (hstrong : ∀ x : H, Tendsto (fun n => T n x) atTop (𝓝 (S x))) :
    ∀ y : K, Tendsto (fun n => isometricExtension J (T n) y) atTop
      (𝓝 (isometricExtension J S y)) := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension