OAI/Geometry/Perimeter/Regularity/ExistsLocalPolarEqApproximateNormal.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.exists_local_polar_eq_approximateNormal line 14
  2. theorem OAI.RPISingularHarnack.minimizing_gaussGreen_local line 41
  3. theorem OAI.RPISingularHarnack.minimizing_halfspaceBlowup_ae line 55
  4. theorem OAI.RPI.vectorEnergy_bounded_coefficient_tendsto line 92
  5. theorem OAI.RPI.vectorEnergy_varying_bounded_smul_zero line 120
  6. theorem OAI.RPI.vectorEnergy_composed_gradient_tendsto line 131
  7. theorem OAI.RPI.vectorEnergy_smul_bounded_field_le line 193
  8. theorem OAI.RPI.vectorEnergy_lipschitz_comp_zero line 205
  9. theorem OAI.RPI.vectorEnergy_nonlinear_test_tendsto line 227
  10. def OAI.RPISingularHarnack.logTest line 301
  11. def OAI.RPISingularHarnack.logSlope line 303
  12. lemma OAI.RPISingularHarnack.logTest_root_pos line 305
  13. lemma OAI.RPISingularHarnack.logTest_root_sq line 308
  14. lemma OAI.RPISingularHarnack.logTest_abs_lt_root line 312
  15. theorem OAI.RPISingularHarnack.logTest_contDiff line 318
  16. theorem OAI.RPISingularHarnack.logTest_hasDerivAt line 323
  17. theorem OAI.RPISingularHarnack.logSlope_continuous line 332
  18. theorem OAI.RPISingularHarnack.logTest_pos line 338
  19. theorem OAI.RPISingularHarnack.logTest_reciprocal line 343
  20. theorem OAI.RPISingularHarnack.logSlope_eq line 352
  21. theorem OAI.RPISingularHarnack.logSlope_neg line 358
  22. theorem OAI.RPISingularHarnack.logSlope_bound line 362
  23. theorem OAI.RPISingularHarnack.logTest_sq_le_neg_slope line 374
  24. theorem OAI.RPISingularHarnack.logSlope_controls_log_weight line 385