OAI/Geometry/Perimeter/Regularity/SmoothSublevelPairingBound.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.smooth_sublevel_pairing_bound line 15
  2. theorem OAI.RPISingularHarnack.sublevel_pairing_bound line 39
  3. theorem OAI.RPISingularHarnack.wholeBoundary_sublevel_energy line 52
  4. def OAI.RPISingularHarnack.rankOneVariation line 160
  5. def OAI.RPISingularHarnack.rankOneJacobian line 163
  6. def OAI.RPISingularHarnack.rankOnePiola line 166
  7. theorem OAI.RPISingularHarnack.rankOneVariation_contDiff line 171
  8. theorem OAI.RPISingularHarnack.rankOneVariation_hasFDerivAt line 176
  9. theorem OAI.RPISingularHarnack.divergence_comp_rankOneVariation line 183
  10. theorem OAI.RPISingularHarnack.rankOneJacobian_hasFDerivAt line 202
  11. theorem OAI.RPISingularHarnack.rankOneJacobian_contDiff line 211
  12. theorem OAI.RPISingularHarnack.rankOnePiola_contDiff line 216
  13. theorem OAI.RPISingularHarnack.divergence_rankOnePiola line 223
  14. theorem OAI.RPISingularHarnack.det_id_add_smulRight line 284
  15. theorem OAI.RPISingularHarnack.det_fderiv_rankOneVariation line 302
  16. theorem OAI.RPISingularHarnack.exists_rankOneVariation_homeomorph line 321
  17. theorem OAI.RPISingularHarnack.rankOneJacobian_pos line 344
  18. theorem OAI.RPISingularHarnack.rankOneVariation_eq_self_of_notMem_tsupport line 360
  19. theorem OAI.RPISingularHarnack.Homeomorph.image_eq_of_eqOn_compl line 365
  20. theorem OAI.RPISingularHarnack.rankOnePiola_tsupport_subset line 393
  21. theorem OAI.RPISingularHarnack.rankOnePiola_hasCompactSupport line 402
  22. theorem OAI.RPISingularHarnack.rankOnePiola_tsupport_subset_region line 411
  23. theorem OAI.RPISingularHarnack.rankOneVariation_image_region line 426
  24. theorem OAI.RPISingularHarnack.symmDiff_image_rankOneVariation_subset line 436