OAI/Geometry/RCD/Sobolev/CompactLipschitzTests.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.compactLipschitzTests line 17
2. theorem OAI.RegularPointCoordinates.compactLipschitzTests_sup_zero line 30
3. def OAI.RegularPointCoordinates.testSobolev line 45
4. theorem OAI.RegularPointCoordinates.testSobolev_coe line 48
5. def OAI.RegularPointCoordinates.compactTestSobolev line 53

   Source documentation

   The lift is linear because its actual L² representative is the test.

   def compactTestSobolev (Ω : Set X) : compactLipschitzTests Ω →ₗ[ℝ] SobolevSpace μ hQ where
   …

   Mentions: OAI.RegularPointCoordinates.compactLipschitzTests, OAI.RegularPointCoordinates.SobolevSpace

6. theorem OAI.RegularPointCoordinates.compactTestSobolev_coe line 67
7. def OAI.RegularPointCoordinates.compactTestEnergy line 72

   Source documentation

   A local distribution of the form energy pairing plus a constant density.

   def compactTestEnergy (Ω : Set X) (q : SobolevSpace μ hQ) (a : ℝ) :
       compactLipschitzTests Ω →ₗ[ℝ] ℝ where
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.compactLipschitzTests