OAI/Analysis/KadisonSimilarity/Representation/ConcretePredual.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The Banach predual of a concrete von Neumann algebra, constructed as the closed span of its vector functionals. The double commutant property makes every bounded functional on this space evaluation at an algebra element.

  1. def OAI.KadisonSimilarity.normalCoefficient line 19

    Source documentation

    A vector functional restricted to the concrete algebra.

    def normalCoefficient (x y : H) : StrongDual ℂ M.toStarSubalgebra :=
…
  2. theorem OAI.KadisonSimilarity.normalCoefficient_apply line 32
  3. theorem OAI.KadisonSimilarity.normalCoefficient_norm_le line 35
  4. def OAI.KadisonSimilarity.normalFunctionalSpace line 40

    Source documentation

    Normal functionals, with their operator-dual norm.

    def normalFunctionalSpace : ClosedSubmodule ℂ (StrongDual ℂ M.toStarSubalgebra) :=
…
  5. def OAI.KadisonSimilarity.ConcretePredual line 43
  6. instance OAI.KadisonSimilarity.(instance at line 45) line 45
  7. instance OAI.KadisonSimilarity.(instance at line 48) line 48
  8. instance OAI.KadisonSimilarity.(instance at line 51) line 51
  9. instance OAI.KadisonSimilarity.(instance at line 54) line 54
  10. def OAI.KadisonSimilarity.predualCoefficient line 56
  11. theorem OAI.KadisonSimilarity.predualCoefficient_apply line 60
  12. theorem OAI.KadisonSimilarity.predualCoefficient_add_left line 64
  13. theorem OAI.KadisonSimilarity.predualCoefficient_smul_left line 72
  14. theorem OAI.KadisonSimilarity.predualCoefficient_add_right line 80
  15. theorem OAI.KadisonSimilarity.predualCoefficient_smul_right line 88
  16. theorem OAI.KadisonSimilarity.predualCoefficient_norm_le line 96
  17. def OAI.KadisonSimilarity.predualForm line 99
  18. theorem OAI.KadisonSimilarity.predualForm_isOperatorForm line 102
  19. theorem OAI.KadisonSimilarity.predualForm_bound line 114
  20. def OAI.KadisonSimilarity.operatorOfPredual line 124

    Source documentation

    Riesz reconstruction from a bounded functional on the vector predual.

    def operatorOfPredual (F : StrongDual ℂ (ConcretePredual M)) : H →L[ℂ] H :=
…

    Mentions: OAI.KadisonSimilarity.ConcretePredual

  21. theorem OAI.KadisonSimilarity.operatorOfPredual_coefficient line 128
  22. theorem OAI.KadisonSimilarity.operatorOfPredual_norm_le line 133
  23. theorem OAI.KadisonSimilarity.predualCoefficient_commutant line 138

    Source documentation

    Commutant elements give identical vector functionals on the algebra.

    theorem predualCoefficient_commutant (S : H →L[ℂ] H) (hS : S ∈ M.commutant)
    (x y : H) : predualCoefficient M (S x) y = predualCoefficient M x (S.adjoint y) := by
…

    Mentions: OAI.KadisonSimilarity.predualCoefficient

  24. theorem OAI.KadisonSimilarity.operatorOfPredual_mem line 149

    Source documentation

    Riesz reconstruction belongs to the original double commutant.

    theorem operatorOfPredual_mem (F : StrongDual ℂ (ConcretePredual M)) :
    operatorOfPredual M F ∈ M := by
…

    Mentions: OAI.KadisonSimilarity.ConcretePredual, OAI.KadisonSimilarity.operatorOfPredual