OAI/Analysis/KadisonSimilarity/Representation/SelfAdjointStrongDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.symmetrize line 16
2. theorem OAI.KadisonSimilarity.symmetrize_selfAdjoint line 19
3. def OAI.KadisonSimilarity.realTupleOrbitMap line 22
4. theorem OAI.KadisonSimilarity.selfAdjoint_bicommutant_tuple_mem_closure line 42

   Source documentation

   Simultaneous approximation of a selfadjoint bicommutant element by selfadjoint elements of the original star algebra, without a norm bound.

   theorem selfAdjoint_bicommutant_tuple_mem_closure
       (S : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
       (hT : T ∈ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))))
       (hTs : IsSelfAdjoint T) (x : Generator.FiniteHilbert ι H) :
       Generator.diagonalOperator T x ∈ (realTupleOrbitMap S x).range.topologicalClosure := by
   …

   Mentions: OAI.Generator.FiniteHilbert, OAI.Generator.diagonalOperator, OAI.KadisonSimilarity.realTupleOrbitMap

5. theorem OAI.KadisonSimilarity.selfAdjoint_bicommutant_finite_approximation line 88

   Source documentation

   Finite-vector version of selfadjoint strong density.

   theorem selfAdjoint_bicommutant_finite_approximation
       (S : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
       (hT : T ∈ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))))
       (hTs : IsSelfAdjoint T) (s : Finset H) (ε : ℝ) (hε : 0 < ε) :
       ∃ a : S, IsSelfAdjoint a.val ∧ ∀ x ∈ s, ‖T x - a.val x‖ < ε := by
   …