OAI/Geometry/RCD/Transport/CompressedSegmentIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating a local defect along a compressed geodesic plan

This is the first-moment step for the functional almost-splitting argument. It retains the full local integrable defect, and permits the selected segment to avoid any additional null set of paths.

  1. theorem OAI.RegularPointCoordinates.compressed_segment_integral line 20
  2. theorem OAI.RegularPointCoordinates.exists_compressed_segment line 46