OAI/Geometry/RCD/Transport/MidpointSupportVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Both endpoint volumes in the actual CD midpoint inequality

This form applies to the preimages of Euclidean balls under metric approximations. No measured limit or volume convergence is assumed.

  1. theorem OAI.RegularPointCoordinates.FullCD.midpoint_support_volume_bound line 18
  2. theorem OAI.RegularPointCoordinates.midpoint_root_bound_to_mass line 74