KaplanskySelfAdjointBall.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded density at self-adjoint elements

The rational preimage lies in the same bicommutant. Its unbounded self-adjoint approximants become contractions under the rational map. A final norm approximation returns to the original star algebra.

theorem OAI.KadisonKastler.selfAdjoint_bicommutant_closureBall_approx line 27

Source documentation

Contractions from the norm closure approximate a self-adjoint bicommutant contraction strongly on any finite set of vectors.

theorem selfAdjoint_bicommutant_closureBall_approx
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hsa : IsSelfAdjoint T) (hn : ‖T‖ ≤ 1) (V : Finset H)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ b ∈ A.topologicalClosure, ‖b‖ ≤ 1 ∧ ∀ x ∈ V, ‖T x - b x‖ < ε := by
…

theorem OAI.KadisonKastler.selfAdjoint_bicommutant_unitBall_approx line 64

Source documentation

The original star algebra's unit ball is strongly dense at every self-adjoint contraction in its bicommutant.

theorem selfAdjoint_bicommutant_unitBall_approx
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hsa : IsSelfAdjoint T) (hn : ‖T‖ ≤ 1) (V : Finset H)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ a : A, ‖(a : H →L[ℂ] H)‖ ≤ 1 ∧ ∀ x ∈ V, ‖T x - (a : H →L[ℂ] H) x‖ < ε := by
…