OAI/Geometry/Perimeter/Regularity/ExistsTangentialGradientBallBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.exists_tangentialGradient_ball_bound line 16
  2. theorem OAI.RPISingularHarnack.tangentialDivergence_integrable_ball_perimeter line 25
  3. theorem OAI.RPISingularHarnack.minimizing_radial_integral_bound line 37
  4. theorem OAI.RPISingularHarnack.radial_integral_lower_of_density line 118
  5. theorem OAI.RPISingularHarnack.exists_minimizing_riesz_potential_constant line 172
  6. theorem OAI.RPIKernel.lp_average_bound line 264
  7. theorem OAI.RPIKernel.kernel_lp_bound line 280
  8. lemma OAI.RPIKernel.ofReal_integral_le_lintegral line 337
  9. theorem OAI.RPIKernel.exists_potential_lp_bound line 347
  10. theorem OAI.RPISingularHarnack.minimizing_perimeter_sobolev line 415
  11. theorem OAI.RPISingularHarnack.minimizing_perimeter_boundaryArea_comparison line 448
  12. theorem OAI.RPISingularHarnack.minimizing_boundaryArea_sobolev line 476