OAI/Geometry/Perimeter/Regularity/TotallyBoundedRangeOfUniformApproximation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.totallyBounded_range_of_uniform_approximation line 14
  2. theorem OAI.RPISingularHarnack.totallyBounded_toLp_of_lipschitz line 34
  3. theorem OAI.RPISingularHarnack.isClosed_lp_ae_mem line 68
  4. theorem OAI.RPISingularHarnack.compact_subtype_volume_finite line 92
  5. def OAI.RPISingularHarnack.compactIndicatorLp line 98
  6. theorem OAI.RPISingularHarnack.compactIndicatorLp_ae line 104
  7. theorem OAI.RPISingularHarnack.compactIndicatorLp_edist_mollified_le line 117
  8. theorem OAI.RPISingularHarnack.bounded_perimeter_indicator_totallyBounded line 152
  9. theorem OAI.RPISingularHarnack.compactIndicatorLp_edist line 209
  10. theorem OAI.RPISingularHarnack.exists_indicator_L1_subsequence line 241
  11. theorem OAI.RPISingularHarnack.tendsto_setIntegral_of_indicator_L1 line 308
  12. theorem OAI.RPISingularHarnack.perimeter_le_of_indicator_L1 line 344
  13. theorem OAI.RPISingularHarnack.exists_bounded_perimeter_L1_subsequence line 368
  14. theorem OAI.RPISingularHarnack.ae_tendsto_scaled_polar_oscillation line 393
  15. theorem OAI.RPISingularHarnack.exists_differentiating_unit_polar line 434
  16. theorem OAI.RPISingularHarnack.ae_inner_ne_value line 472
  17. theorem OAI.RPISingularHarnack.ordered_indicator_halfspace line 497