OAI/Geometry/EinsteinFour/CP2Overlap.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Unit representatives and transition probabilities for the actual Fubini--Study distance on CP2.

  1. abbrev OAI.PositiveEinsteinFour.CP2Vector line 14
  2. def OAI.PositiveEinsteinFour.cp2UnitRep line 16
  3. theorem OAI.PositiveEinsteinFour.cp2UnitRep_norm line 19
  4. theorem OAI.PositiveEinsteinFour.cp2UnitRep_ne_zero line 23
  5. theorem OAI.PositiveEinsteinFour.cp2UnitRep_mk line 29
  6. def OAI.PositiveEinsteinFour.cp2Overlap line 34
  7. theorem OAI.PositiveEinsteinFour.cp2Overlap_nonneg line 37
  8. theorem OAI.PositiveEinsteinFour.cp2Overlap_le_one line 39
  9. theorem OAI.PositiveEinsteinFour.cp2Overlap_eq_ratio line 42
  10. theorem OAI.PositiveEinsteinFour.fubiniStudyDistance_eq_arccos line 55
  11. theorem OAI.PositiveEinsteinFour.cp2Overlap_eq_iff_distance_eq line 60
  12. theorem OAI.PositiveEinsteinFour.cp2Overlap_mk line 69
  13. theorem OAI.PositiveEinsteinFour.cp2Overlap_comm line 74
  14. theorem OAI.PositiveEinsteinFour.cp2Overlap_self line 77