OAI/Geometry/Perimeter/Regularity/HeightMeanValue.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.gradient_affine_height line 11
  2. theorem OAI.RPISingularHarnack.gradient_radial_primitive line 18
  3. theorem OAI.RPISingularHarnack.minimizing_height_radialDerivative_nonpos line 35
  4. def OAI.RPISingularHarnack.densityPrimitive line 172
  5. theorem OAI.RPISingularHarnack.densityPrimitive_hasDerivAt line 175
  6. theorem OAI.RPISingularHarnack.densityPrimitive_deriv line 182
  7. theorem OAI.RPISingularHarnack.densityPrimitive_contDiff line 185
  8. theorem OAI.RPISingularHarnack.densityPrimitive_zero line 190
  9. theorem OAI.RPISingularHarnack.densityPrimitive_nonpos line 200
  10. theorem OAI.RPISingularHarnack.integral_hasDerivAt_compact_window line 208
  11. theorem OAI.RPISingularHarnack.height_radial_integral_hasDerivAt line 234
  12. theorem OAI.RPISingularHarnack.minimizing_height_smoothedDensity_antitoneOn line 250
  13. theorem OAI.RPISingularHarnack.height_radial_integral_tendsto line 273
  14. theorem OAI.RPISingularHarnack.minimizing_height_density_monotone line 319
  15. theorem OAI.RPISingularHarnack.exists_minimizing_height_mean_value_constant line 337