OAI/Geometry/RCD/Metric/MeasurablePairSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A measurable cut retains a fixed fraction of the off-diagonal mass

This is the specialization of Rajala--Sturm, arXiv:1207.6754v2, Lemma 3.1 needed for the branching argument. No normalization of the finite measure is needed; the same constant works before or after restricting pairs.

  1. theorem OAI.RegularPointCoordinates.measurable_pair_separation line 19