OAI/Analysis/BrownMeasure/Atomic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolarStructure.Op line 11
  2. def OAI.PolarStructure.generated line 13
  3. def OAI.PolarStructure.MinimalProjection line 22
  4. def OAI.PolarStructure.Atomic line 26
  5. def OAI.PolarStructure.jointSpace line 30
  6. lemma OAI.PolarStructure.mem_jointSpace line 40
  7. lemma OAI.PolarStructure.jointSpace_closed line 43
  8. instance OAI.PolarStructure.jointSpace_complete line 48
  9. def OAI.PolarStructure.JointPurePoint line 51
  10. lemma OAI.PolarStructure.projection_commutes_of_invariant line 54
  11. lemma OAI.PolarStructure.commutant_preserves line 66
  12. lemma OAI.PolarStructure.jointProjection_mem line 74
  13. lemma OAI.PolarStructure.rankOne_commutes line 84
  14. lemma OAI.PolarStructure.generated_scalar_on_joint line 100
  15. lemma OAI.PolarStructure.projection_scalar_zero_or_one line 118
  16. lemma OAI.PolarStructure.jointProjection_minimal line 129
  17. lemma OAI.PolarStructure.exists_joint_not_killed line 154
  18. theorem OAI.PolarStructure.atomic_of_jointPurePoint line 168