OAI/Analysis/RCDHeat/GeodesicMarginalCompact.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: GeodesicMarginalCompact.

  1. theorem OAI.RegularPointCoordinates.isCompact_bounded_geodesic_plans_marginals line 21