OAI/Geometry/Perimeter/Regularity/SmoothLayerSumBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.smooth_layer_sum_bounds line 13
  2. theorem OAI.RPISingularHarnack.finite_level_count_le line 44
  3. theorem OAI.RPISingularHarnack.abs_integral_divergence_le_bound_perimeter line 75
  4. theorem OAI.RPISingularHarnack.scalar_layer_admissible line 108
  5. theorem OAI.RPISingularHarnack.finite_level_integral_le line 150
  6. theorem OAI.RPISingularHarnack.integral_divergence_scalar_le line 200
  7. theorem OAI.RPISingularHarnack.abs_integral_divergence_le_integral_norm line 311
  8. def OAI.RPISingularHarnack.smoothVariationDomain line 396
  9. def OAI.RPISingularHarnack.smoothVariationRepresentative line 414
  10. theorem OAI.RPISingularHarnack.smoothVariationRepresentative_spec line 418
  11. theorem OAI.RPISingularHarnack.integral_divergence_eq_of_variation_ae line 426
  12. def OAI.RPISingularHarnack.localVariationFunctional line 446
  13. theorem OAI.RPISingularHarnack.localVariationFunctional_le line 475