OAI/Analysis/KLS/Sobolev/Witnesses.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeGiorgi.MemW1p line 16
  2. structure OAI.DeGiorgi.MemW1pWitness line 22
  3. abbrev OAI.DeGiorgi.MemH1 line 34
  4. def OAI.DeGiorgi.MemW01p line 37
  5. abbrev OAI.DeGiorgi.MemH01 line 52
  6. def OAI.DeGiorgi.MemW1p.someWitness line 55
  7. theorem OAI.DeGiorgi.MemW1pWitness.memW1p line 70
  8. def OAI.DeGiorgi.MemW1pWitness.add line 78
  9. def OAI.DeGiorgi.MemW1pWitness.restrict line 141
  10. def OAI.DeGiorgi.MemW1pWitness.smul line 156
  11. def OAI.DeGiorgi.MemW1pWitness.mul_smooth_bounded_p line 202
  12. def OAI.DeGiorgi.MemW1pWitness.of_contDiff_hasCompactSupport line 268
  13. theorem OAI.DeGiorgi.MemW1pWitness.weakGrad_memLp line 289
  14. theorem OAI.DeGiorgi.MemW1pWitness.weakGrad_norm_memLp line 297
  15. theorem OAI.DeGiorgi.MemW01p.memW1p line 306
  16. theorem OAI.DeGiorgi.MemW01p.add line 312
  17. theorem OAI.DeGiorgi.MemW01p.smul line 422
  18. theorem OAI.DeGiorgi.MemW01p.sub line 493
  19. theorem OAI.DeGiorgi.memW01p_of_contDiff_hasCompactSupport line 499
  20. theorem OAI.DeGiorgi.memW01p_of_contDiff_hasCompactSupport_subset line 517