OAI/Analysis/KadisonSimilarity/Representation/KaplanskySelfAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selfadjoint unit ball of the source algebra is strongly dense in the selfadjoint unit ball of the represented bicommutant.

  1. theorem OAI.KadisonSimilarity.lift_selfAdjoint_range line 16
  2. theorem OAI.KadisonSimilarity.selfAdjoint_kaplansky_approximation line 28

    Source documentation

    Exact source norm control, on any finite family of test vectors.

    theorem selfAdjoint_kaplansky_approximation
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ representationVonNeumannAlgebra σ) (hTs : IsSelfAdjoint T)
    (hTn : ‖T‖ ≤ 1) (s : Finset H) (ε : ℝ) (hε : 0 < ε) :
    ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ 1 ∧ ∀ x ∈ s, ‖σ a x - T x‖ < ε := by
…

    Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra