OAI/Geometry/Perimeter/Regularity/RankOneNormalError.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.rankOneNormalError line 15
  2. theorem OAI.RPISingularHarnack.inner_rankOnePiola line 20
  3. theorem OAI.RPISingularHarnack.rankOneNormalError_norm_le line 30
  4. theorem OAI.RPISingularHarnack.perimeter_image_rankOneVariation_le line 49
  5. theorem OAI.RPISingularHarnack.norm_unit_add_smul_le_quadratic line 117
  6. theorem OAI.RPISingularHarnack.linear_term_eq_zero_of_local_quadratic_nonneg line 124
  7. theorem OAI.RPISingularHarnack.minimizing_tangentialGradient_integral_eq_zero_local line 149
  8. def OAI.RPISingularHarnack.tangentialDivergence line 238
  9. theorem OAI.RPISingularHarnack.tangentialDivergence_eq_sum line 243
  10. theorem OAI.RPISingularHarnack.tangentialDivergence_smul line 260
  11. theorem OAI.RPISingularHarnack.tangentialDivergence_displacement line 274
  12. def OAI.RPISingularHarnack.radialKernel line 285
  13. theorem OAI.RPISingularHarnack.radialKernel_contDiff line 288
  14. theorem OAI.RPISingularHarnack.radialKernel_hasFDerivAt line 294
  15. theorem OAI.RPISingularHarnack.tangentialDivergence_radial line 311
  16. theorem OAI.RPISingularHarnack.tangentialGradient_integrable_ball_perimeter line 350
  17. theorem OAI.RPISingularHarnack.minimizing_tangentialDivergence_integral_eq_zero line 367
  18. theorem OAI.RPIKernel.kernel_le_dyadic line 406
  19. theorem OAI.RPIKernel.exists_kernel_integral_bound line 442
  20. theorem OAI.RPIKernel.integrable_kernel_of_growth line 510
  21. theorem OAI.RPISingularHarnack.radialKernel_pos line 533
  22. theorem OAI.RPISingularHarnack.radialKernel_mul_dist_le line 538
  23. theorem OAI.RPISingularHarnack.radialKernel_mass_scaling line 556