OAI/Geometry/Perimeter/Regularity/FlatExcess.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.integral_abs_indicator_sub_eq_symmDiff line 12
  2. theorem OAI.RPISingularHarnack.halfspace_perimeterSupport_subset_plane line 24
  3. theorem OAI.RPISingularHarnack.halfspace_hasHalfspaceBlowup line 42
  4. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.local_L1 line 52
  5. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.support_height line 121
  6. def OAI.RPISingularHarnack.orientedTilt line 146
  7. theorem OAI.RPISingularHarnack.orientedTilt_le_calibration_gap line 149
  8. theorem OAI.RPISingularHarnack.exists_halfspace_calibration line 214
  9. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.orientedTilt_tendsto line 281
  10. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.orientedTilt_tendsto_all_scales line 317
  11. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.support_height_all_scales line 340
  12. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.small_height_and_orientedTilt line 363
  13. theorem OAI.RPISingularHarnack.minimizing_height_caccioppoli line 374
  14. theorem OAI.RPISingularHarnack.minimizing_height_distribution line 472
  15. def OAI.RPISingularHarnack.planarDivergence line 515
  16. theorem OAI.RPISingularHarnack.normal_quadratic_difference_le line 518
  17. theorem OAI.RPISingularHarnack.normal_error_integral_le line 543
  18. theorem OAI.RPISingularHarnack.minimizing_height_planar_residual line 568
  19. theorem OAI.RPISingularHarnack.horizontal_normal_le_height_projection line 649
  20. theorem OAI.RPISingularHarnack.minimizing_horizontal_normal_square_le line 666
  21. theorem OAI.RPISingularHarnack.integral_abs_le_of_quadratic_mean_bound line 738
  22. theorem OAI.RPISingularHarnack.minimizing_horizontal_normal_integral_le line 762
  23. theorem OAI.RPISingularHarnack.minimizing_horizontal_test_le line 826