OAI/Analysis/CharacterCriterion/Representations.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.GenericRW.Representations.gnsVector line 22
  2. lemma OAI.KirchbergRordam.GenericRW.Representations.gnsVector_inner line 24
  3. lemma OAI.KirchbergRordam.GenericRW.Representations.gnsVector_apply line 28
  4. lemma OAI.KirchbergRordam.GenericRW.Representations.positive_bound line 32
  5. def OAI.KirchbergRordam.GenericRW.Representations.positiveCLM line 50
  6. lemma OAI.KirchbergRordam.GenericRW.Representations.positiveCLM_apply line 53
  7. lemma OAI.KirchbergRordam.GenericRW.Representations.positiveCLM_norm line 55
  8. def OAI.KirchbergRordam.GenericRW.Representations.representationCLM line 63
  9. lemma OAI.KirchbergRordam.GenericRW.Representations.representationCLM_apply line 68
  10. def OAI.KirchbergRordam.GenericRW.Representations.coefficient line 70
  11. lemma OAI.KirchbergRordam.GenericRW.Representations.coefficient_apply line 77
  12. lemma OAI.KirchbergRordam.GenericRW.Representations.coefficient_nonneg line 80
  13. lemma OAI.KirchbergRordam.GenericRW.Representations.coefficient_norm line 98
  14. lemma OAI.KirchbergRordam.GenericRW.PureStates.IsPure.split line 114
  15. lemma OAI.KirchbergRordam.GenericRW.Representations.coefficient_one line 170
  16. lemma OAI.KirchbergRordam.GenericRW.Representations.coefficient_commutant_injective line 173
  17. lemma OAI.KirchbergRordam.GenericRW.Representations.positive_contraction_scalar line 201
  18. lemma OAI.KirchbergRordam.GenericRW.Representations.positive_scalar line 239
  19. lemma OAI.KirchbergRordam.GenericRW.Representations.selfAdjoint_scalar line 253
  20. theorem OAI.KirchbergRordam.GenericRW.Representations.pure_cyclic_scalar_commutant line 265
  21. lemma OAI.KirchbergRordam.GenericRW.Representations.gns_cyclic line 290
  22. lemma OAI.KirchbergRordam.GenericRW.Representations.positive_zero_of_square_zero line 300
  23. def OAI.KirchbergRordam.GenericRW.Representations.stateOfPure line 310
  24. lemma OAI.KirchbergRordam.GenericRW.Representations.stateOfPure_apply line 313
  25. lemma OAI.KirchbergRordam.GenericRW.Representations.pure_gns_coefficient line 316
  26. lemma OAI.KirchbergRordam.GenericRW.Representations.pure_gns_nontrivial line 322
  27. structure OAI.KirchbergRordam.GenericRW.IrreducibleRepresentation line 334
  28. def OAI.KirchbergRordam.GenericRW.Representations.pureRepresentation line 350
  29. theorem OAI.KirchbergRordam.GenericRW.exists_irreducible_representation line 364