OAI/Geometry/RCD/Transport/ResolvedBranchMixture.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The half mixture as an actual resolved paired subplan

  1. def OAI.RegularPointCoordinates.diagonalFirst line 14
  2. def OAI.RegularPointCoordinates.halfResolvedPair line 16
  3. theorem OAI.RegularPointCoordinates.measurable_diagonalFirst line 20
  4. theorem OAI.RegularPointCoordinates.resolvePathBranch_diagonal line 24
  5. theorem OAI.RegularPointCoordinates.half_smul_self line 30
  6. theorem OAI.RegularPointCoordinates.diagonalFirst_fst line 35
  7. theorem OAI.RegularPointCoordinates.diagonalFirst_snd line 41
  8. theorem OAI.RegularPointCoordinates.halfResolvedPair_fst line 47
  9. theorem OAI.RegularPointCoordinates.halfResolvedPair_snd line 54
  10. theorem OAI.RegularPointCoordinates.halfResolvedPair_mass line 60
  11. instance OAI.RegularPointCoordinates.halfResolvedPair_finite line 65
  12. theorem OAI.RegularPointCoordinates.halfResolvedPair_dominated line 70
  13. theorem OAI.RegularPointCoordinates.diagonalFirst_resolved line 78
  14. theorem OAI.RegularPointCoordinates.halfResolvedPair_resolved line 85
  15. theorem OAI.RegularPointCoordinates.normalized_halfResolvedPair line 91