OAI/Geometry/RCD/Metric/SeparatedPairRestriction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Restricting paired paths to two separated marginals

The retained mass is quantitative. Restriction preserves every previously established almost-everywhere equality between the paired observables.

  1. theorem OAI.RegularPointCoordinates.exists_separated_restriction line 17
  2. theorem OAI.RegularPointCoordinates.restricted_observables_equal line 53