OAI/Analysis/KadisonSimilarity/Representation/ConcretePredualDuality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Isometric duality between the concrete vector predual and the original von Neumann algebra. The conjugate-linear convention agrees with the predual interface used by the finite normal trace construction.

  1. def OAI.KadisonSimilarity.predualEvaluation line 16
  2. theorem OAI.KadisonSimilarity.predualEvaluation_apply line 24
  3. theorem OAI.KadisonSimilarity.predualEvaluation_norm line 27
  4. theorem OAI.KadisonSimilarity.predual_ext line 44

    Source documentation

    Vector coefficients determine every continuous functional on the predual.

    theorem predual_ext (F G : StrongDual ℂ (ConcretePredual M))
    (h : ∀ x y, F (predualCoefficient M x y) = G (predualCoefficient M x y)) : F = G := by
…

    Mentions: OAI.KadisonSimilarity.ConcretePredual, OAI.KadisonSimilarity.predualCoefficient

  5. theorem OAI.KadisonSimilarity.predualEvaluation_surjective line 63
  6. def OAI.KadisonSimilarity.predualEvaluationIsometry line 70
  7. def OAI.KadisonSimilarity.concretePredualLinearEquiv line 82
  8. def OAI.KadisonSimilarity.concretePredualEquiv line 87

    Source documentation

    The given concrete algebra is the conjugate dual of an actual Banach space.

    def concretePredualEquiv : StrongDual ℂ (ConcretePredual M) ≃ₗᵢ⋆[ℂ] M.toStarSubalgebra :=
…

    Mentions: OAI.KadisonSimilarity.ConcretePredual

  9. theorem OAI.KadisonSimilarity.concretePredualEquiv_symm_apply line 90