OAI/Geometry/Perimeter/Regularity/PairedCutTest.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.pairedCutTest line 13
  2. theorem OAI.RPISingularHarnack.pairedCutTest_eq line 17
  3. theorem OAI.RPISingularHarnack.pairedCutTest_admissible line 24
  4. theorem OAI.RPISingularHarnack.divergence_sub line 53
  5. theorem OAI.RPISingularHarnack.divergence_pairedCutTest line 60
  6. theorem OAI.RPISingularHarnack.integrable_annularCutoff_mul line 77
  7. theorem OAI.RPISingularHarnack.integral_pairedCut_le line 87
  8. theorem OAI.RPISingularHarnack.tendsto_integral_annularCutoff_mul line 129
  9. theorem OAI.RPISingularHarnack.nonnegative_perimeter_test_replacement line 159
  10. theorem OAI.RPISingularHarnack.perimeter_add_le_of_pair_integrals line 171
  11. theorem OAI.RPISingularHarnack.controlled_radius_perimeter_cut line 183
  12. theorem OAI.RPISingularHarnack.minimizing_controlled_radius_perimeter_le line 242
  13. theorem OAI.RPISingularHarnack.exists_minimizing_volume_cut line 275
  14. theorem OAI.RPISingularHarnack.nonlinear_iteration_geometric_bound line 309
  15. theorem OAI.RPISingularHarnack.exists_nonlinear_iteration_threshold line 332
  16. theorem OAI.RPISingularHarnack.nonlinear_iteration_tendsto_zero line 364
  17. theorem OAI.RPISingularHarnack.minimizing_volume_recursion line 388
  18. def OAI.RPISingularHarnack.clearingRadius line 436
  19. theorem OAI.RPISingularHarnack.clearingRadius_zero line 438
  20. theorem OAI.RPISingularHarnack.clearingRadius_sub_succ line 441
  21. theorem OAI.RPISingularHarnack.clearingRadius_pos line 448
  22. theorem OAI.RPISingularHarnack.clearingRadius_half_le line 452
  23. theorem OAI.RPISingularHarnack.clearingRadius_succ_lt line 456
  24. theorem OAI.RPISingularHarnack.minimizing_clearing_out line 463