OAI/Analysis/CharacterCriterion/RepresentationTheory.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.States.norm_rotation line 37
  2. lemma OAI.KirchbergRordam.States.eval_selfAdjoint_im_zero line 45
  3. lemma OAI.KirchbergRordam.States.eval_nonneg line 64
  4. theorem OAI.KirchbergRordam.States.exists_state line 93
  5. def OAI.KirchbergRordam.PureStates.normStates line 107
  6. def OAI.KirchbergRordam.PureStates.evaluationReal line 109
  7. instance OAI.KirchbergRordam.PureStates.locallyConvexReal line 114
  8. lemma OAI.KirchbergRordam.PureStates.normStates_compact line 117
  9. lemma OAI.KirchbergRordam.PureStates.normStates_nonempty line 126
  10. def OAI.KirchbergRordam.PureStates.IsPure line 132
  11. theorem OAI.KirchbergRordam.PureStates.exists_pure line 135
  12. lemma OAI.KirchbergRordam.PureStates.IsPure.norm_le_one line 142
  13. lemma OAI.KirchbergRordam.PureStates.IsPure.map_one line 144
  14. lemma OAI.KirchbergRordam.PureStates.IsPure.extreme line 147
  15. def OAI.KirchbergRordam.Representations.gnsVector line 166
  16. lemma OAI.KirchbergRordam.Representations.gnsVector_inner line 168
  17. lemma OAI.KirchbergRordam.Representations.gnsVector_apply line 172
  18. lemma OAI.KirchbergRordam.Representations.positive_bound line 176
  19. def OAI.KirchbergRordam.Representations.positiveCLM line 194
  20. lemma OAI.KirchbergRordam.Representations.positiveCLM_apply line 197
  21. lemma OAI.KirchbergRordam.Representations.positiveCLM_norm line 199
  22. def OAI.KirchbergRordam.Representations.representationCLM line 207
  23. lemma OAI.KirchbergRordam.Representations.representationCLM_apply line 212
  24. def OAI.KirchbergRordam.Representations.coefficient line 214
  25. lemma OAI.KirchbergRordam.Representations.coefficient_apply line 222
  26. lemma OAI.KirchbergRordam.Representations.coefficient_nonneg line 236
  27. lemma OAI.KirchbergRordam.Representations.coefficient_norm line 254
  28. lemma OAI.KirchbergRordam.PureStates.IsPure.split line 270
  29. lemma OAI.KirchbergRordam.Representations.coefficient_one line 327
  30. lemma OAI.KirchbergRordam.Representations.coefficient_commutant_injective line 341
  31. lemma OAI.KirchbergRordam.Representations.positive_contraction_scalar line 369
  32. lemma OAI.KirchbergRordam.Representations.positive_scalar line 407
  33. lemma OAI.KirchbergRordam.Representations.selfAdjoint_scalar line 421
  34. theorem OAI.KirchbergRordam.Representations.pure_cyclic_scalar_commutant line 433
  35. lemma OAI.KirchbergRordam.Representations.gns_cyclic line 458
  36. lemma OAI.KirchbergRordam.Representations.positive_zero_of_square_zero line 468
  37. def OAI.KirchbergRordam.Representations.stateOfPure line 478
  38. lemma OAI.KirchbergRordam.Representations.stateOfPure_apply line 481
  39. lemma OAI.KirchbergRordam.Representations.pure_gns_coefficient line 484
  40. lemma OAI.KirchbergRordam.Representations.pure_gns_nontrivial line 490
  41. structure OAI.KirchbergRordam.IrreducibleRepresentation line 502
  42. def OAI.KirchbergRordam.Representations.pureRepresentation line 518
  43. theorem OAI.KirchbergRordam.exists_irreducible_representation line 532
  44. lemma OAI.KirchbergRordam.PureStates.exists_norming_dual line 545
  45. theorem OAI.KirchbergRordam.PureStates.exists_pure_norming line 571
  46. theorem OAI.KirchbergRordam.irreducible_separate_zero line 606