OAI/Geometry/RCD/Sobolev/CompactCoreEnergyExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extending the energy inequality to all compact Lipschitz tests

The same Sobolev family is retained. Positivity and one uniform bound on the test sequence allow dominated convergence in space and then time.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_core_energy_extension line 19