OAI/Geometry/Perimeter/Regularity/TangentialGradientComp.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.tangentialGradient_comp line 15
  2. theorem OAI.RPISingularHarnack.tangentialGradient_nonlinear_test line 26
  3. theorem OAI.RPISingularHarnack.wholeBoundarySupersolution_nonlinear_test line 42
  4. theorem OAI.RPISingularHarnack.logTest_lipschitz line 163
  5. def OAI.RPISingularHarnack.logRootWeight line 171
  6. def OAI.RPISingularHarnack.logTestRatio line 172
  7. theorem OAI.RPISingularHarnack.logRootWeight_pos line 174
  8. theorem OAI.RPISingularHarnack.logRootWeight_sq line 177
  9. theorem OAI.RPISingularHarnack.logTestRatio_mem_Icc line 181
  10. theorem OAI.RPISingularHarnack.logRootWeight_bound line 188
  11. theorem OAI.RPISingularHarnack.logTestRatio_continuous line 194
  12. theorem OAI.RPISingularHarnack.logTest_pairing line 199
  13. theorem OAI.RPISingularHarnack.log_weight_le_energy line 213
  14. theorem OAI.RPISingularHarnack.wholeBoundary_log_caccioppoli line 222
  15. def OAI.RPISingularHarnack.smoothPositive line 304
  16. theorem OAI.RPISingularHarnack.smoothPositive_hasDerivAt line 306
  17. theorem OAI.RPISingularHarnack.smoothPositive_deriv line 312
  18. theorem OAI.RPISingularHarnack.smoothPositive_contDiff line 316
  19. theorem OAI.RPISingularHarnack.smoothPositive_of_nonpos line 322
  20. theorem OAI.RPISingularHarnack.smoothPositive_nonneg line 333
  21. theorem OAI.RPISingularHarnack.smoothPositive_le_mul line 339
  22. theorem OAI.RPISingularHarnack.smoothPositive_le_self line 347
  23. theorem OAI.RPISingularHarnack.sub_parameter_le_smoothPositive line 351
  24. def OAI.RPISingularHarnack.sublevelTest line 373
  25. def OAI.RPISingularHarnack.sublevelSlope line 374
  26. theorem OAI.RPISingularHarnack.sublevelTest_contDiff line 376
  27. theorem OAI.RPISingularHarnack.sublevelTest_hasDerivAt line 379
  28. theorem OAI.RPISingularHarnack.sublevelTest_nonneg line 384
  29. theorem OAI.RPISingularHarnack.sublevelSlope_mem_Icc line 387
  30. theorem OAI.RPISingularHarnack.sublevelTest_controls line 390
  31. theorem OAI.RPISingularHarnack.sublevelTest_eq_zero line 398
  32. theorem OAI.RPISingularHarnack.sublevelSlope_eq_zero line 401
  33. theorem OAI.RPISingularHarnack.sublevelTest_lipschitz line 405