OAI/Geometry/RCD/Sobolev/UniformEventualLowerEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lower energy bounds after discarding a finite initial segment

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.gradient_energy_lower_of_curvature_eventual_sequence line 13