OAI/Geometry/RCD/Sobolev/UniformLowerEnergyFromSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean lower energy bound from actual Sobolev sequences

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.gradient_energy_lower_of_curvature_sequence line 14