OAI/Geometry/RCD/Transport/ResolvedBranchSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative selection of two branches with a common past

The chosen pair restriction has mass at least a fixed multiple of the time mesh, equal past marginals, and mutually singular future marginals.

  1. theorem OAI.RegularPointCoordinates.select_resolved_branches line 19