OAI/Analysis/KadisonKastler/ConjugationFunctionalCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Real functional calculus under an antiunitary conjugation

  1. def OAI.KadisonKastler.conjugationRealStarAlgEquiv line 15

    Source documentation

    An involutive antiunitary acts by a real star-algebra automorphism.

    def conjugationRealStarAlgEquiv (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) :
    (H →L[ℂ] H) ≃⋆ₐ[ℝ] (H →L[ℂ] H) where
…
  2. theorem OAI.KadisonKastler.conjugationRealStarAlgEquiv_isometry line 29
  3. theorem OAI.KadisonKastler.conjugationOperator_selfAdjoint line 37
  4. theorem OAI.KadisonKastler.conjugationOperator_cfc_real line 43