OAI/Geometry/RCD/Transport/PairedBranchLaws.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Equal and singular marginals of normalized paired branch laws

  1. theorem OAI.RegularPointCoordinates.normalized_pair_left_eval line 15
  2. theorem OAI.RegularPointCoordinates.normalized_pair_right_eval line 21
  3. theorem OAI.RegularPointCoordinates.normalized_pair_eval_eq line 27
  4. theorem OAI.RegularPointCoordinates.normalized_pair_eval_singular line 33
  5. theorem OAI.RegularPointCoordinates.half_mixture_map_eval line 41
  6. theorem OAI.RegularPointCoordinates.half_mixture_eval_eq line 48