OAI/Geometry/RCD/Sobolev/SupportedEnergyLocality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Energy locality against a supported Sobolev test

  1. theorem OAI.RegularPointCoordinates.energyForm_eq_of_test_support line 14