OAI/Analysis/FactorGeneration/CyclicPredual.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

A concrete candidate predual: the norm-closed complex span of vector functionals from the faithful cyclic trace representation, with completeness, separability, and an isometric evaluation map.

  1. instance OAI.Generator.Tracial.algebraDualNormed line 26

    Source documentation

    Name the existing operator-norm structure to keep the norm topology explicit through the nested dual and submodule constructions.

    instance algebraDualNormed (M : VonNeumannAlgebra H) :
    NormedAddCommGroup (StrongDual ℂ M.toStarSubalgebra) := inferInstance
  2. def OAI.Generator.Tracial.traceCyclicLinearIsometry line 29
  3. def OAI.Generator.Tracial.cyclicCoefficient line 33
  4. theorem OAI.Generator.Tracial.cyclicCoefficient_apply line 37
  5. theorem OAI.Generator.Tracial.cyclicCoefficient_norm_le line 40
  6. theorem OAI.Generator.Tracial.cyclicCoefficient_continuous line 50
  7. abbrev OAI.Generator.Tracial.cyclicPredual line 55
  8. instance OAI.Generator.Tracial.cyclicPredual_normed line 59
  9. instance OAI.Generator.Tracial.cyclicPredual_normedSpace line 61
  10. instance OAI.Generator.Tracial.cyclicPredual_complete line 63
  11. theorem OAI.Generator.Tracial.cyclicCoefficient_mem line 67
  12. theorem OAI.Generator.Tracial.cyclicPredual_separable line 71
  13. def OAI.Generator.Tracial.cyclicPredualEvaluation line 75
  14. theorem OAI.Generator.Tracial.cyclicPredualEvaluation_apply line 78
  15. theorem OAI.Generator.Tracial.cyclicPredualEvaluation_norm_le line 81
  16. theorem OAI.Generator.Tracial.cyclicPredualEvaluation_norm line 87
  17. def OAI.Generator.Tracial.cyclicPredualEvaluationIsometry line 109
  18. def OAI.Generator.Tracial.ballContinuousFunctionals line 126
  19. theorem OAI.Generator.Tracial.ballContinuousFunctionals_isClosed line 133
  20. theorem OAI.Generator.Tracial.cyclicPredual_le_ballContinuousFunctionals line 157
  21. theorem OAI.Generator.Tracial.cyclicPredual_ball_continuous line 166
  22. instance OAI.Generator.Tracial.predualWeakScalarTower line 181
  23. instance OAI.Generator.Tracial.predualWeakLocallyConvex line 184
  24. def OAI.Generator.Tracial.predualWeakEvaluation line 187
  25. def OAI.Generator.Tracial.predualWeakBall line 190
  26. theorem OAI.Generator.Tracial.predualWeakBall_isCompact line 193
  27. theorem OAI.Generator.Tracial.predualWeakBall_convex line 212
  28. theorem OAI.Generator.Tracial.dual_norm_le_of_re_unitBall line 217
  29. theorem OAI.Generator.Tracial.weakDual_separation line 230
  30. theorem OAI.Generator.Tracial.cyclicPredualEvaluation_unitBall_surjective line 244
  31. instance OAI.Generator.Tracial.functionalSubspaceNormed line 290
  32. instance OAI.Generator.Tracial.functionalSubspaceNormedSpace line 292
  33. def OAI.Generator.Tracial.functionalSubspaceEvaluation line 294
  34. theorem OAI.Generator.Tracial.functionalSubspaceEvaluation_apply line 297
  35. def OAI.Generator.Tracial.functionalSubspaceEvaluationLinear line 300
  36. instance OAI.Generator.Tracial.functionalSubspaceWeakScalarTower line 305
  37. instance OAI.Generator.Tracial.functionalSubspaceWeakLocallyConvex line 308
  38. def OAI.Generator.Tracial.functionalSubspaceWeakEvaluation line 311
  39. def OAI.Generator.Tracial.functionalSubspaceWeakBall line 314
  40. theorem OAI.Generator.Tracial.functionalSubspaceWeakBall_isCompact line 317
  41. theorem OAI.Generator.Tracial.functionalSubspaceWeakBall_convex line 337
  42. theorem OAI.Generator.Tracial.functionalSubspaceEvaluation_unitBall_surjective line 342
  43. theorem OAI.Generator.Tracial.functionalSubspaceEvaluation_surjective line 378

    Source documentation

    Unit-ball surjectivity extends by rescaling to the whole dual.

    theorem functionalSubspaceEvaluation_surjective
    (hF : F ≤ ballContinuousFunctionals M 1) :
    Function.Surjective (functionalSubspaceEvaluation F) := by
…

    Mentions: OAI.Generator.Tracial.ballContinuousFunctionals, OAI.Generator.Tracial.functionalSubspaceEvaluation

  44. theorem OAI.Generator.Tracial.ballContinuousFunctionals_eq_cyclicPredual line 407
  45. theorem OAI.Generator.Tracial.mem_cyclicPredual_iff_unitBall_continuous line 439
  46. theorem OAI.Generator.Tracial.mem_cyclicPredual_of_unitBall_continuous line 445