OAI/Geometry/RCD/Transport/ResolvedBranchMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Endpoint and compression control for the measurable branch splice

  1. theorem OAI.RegularPointCoordinates.map_le_add_of_choice line 12
  2. theorem OAI.RegularPointCoordinates.resolved_branch_endpoints line 28
  3. theorem OAI.RegularPointCoordinates.resolved_branch_endpoint_time line 37
  4. theorem OAI.RegularPointCoordinates.resolved_branch_optimal line 50
  5. theorem OAI.RegularPointCoordinates.resolved_branch_compression line 61
  6. theorem OAI.RegularPointCoordinates.resolved_branch_geodesic line 72
  7. theorem OAI.RegularPointCoordinates.resolved_branch_common_past line 80