OAI/Geometry/Perimeter/Regularity/SmulMemPhaseSupport.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.IsCone.smul_mem_phaseSupport line 18
  2. theorem OAI.RPISingularHarnack.isCone_perimeterSupport line 36
  3. theorem OAI.RPISingularHarnack.IsCone.isPathConnected_perimeterSupport line 50
  4. def OAI.RPISingularHarnack.NestedMinimizingConeMaximumObligation line 62
  5. def OAI.RPISingularHarnack.radialDensityIntegrand line 86
  6. def OAI.RPISingularHarnack.radialDensityDerivative line 89
  7. theorem OAI.RPISingularHarnack.radialDensityIntegrand_hasDerivAt line 94
  8. theorem OAI.RPISingularHarnack.radialDensityIntegrand_continuous line 106
  9. theorem OAI.RPISingularHarnack.radialDensityDerivative_continuous line 112
  10. theorem OAI.RPISingularHarnack.radialDensity_integral_hasDerivAt line 119
  11. theorem OAI.RPISingularHarnack.tangentialDivergence_radialProfile line 145
  12. theorem OAI.RPISingularHarnack.radialProfile_tsupport line 172
  13. theorem OAI.RPISingularHarnack.minimizing_radialDensityDerivative_nonpos line 186
  14. theorem OAI.RPISingularHarnack.minimizing_smoothedDensity_antitoneOn line 233
  15. def OAI.RPISingularHarnack.densityProfile line 253
  16. theorem OAI.RPISingularHarnack.densityProfile_contDiff line 256
  17. theorem OAI.RPISingularHarnack.densityProfile_mem_Icc line 259
  18. theorem OAI.RPISingularHarnack.densityProfile_zero line 262
  19. theorem OAI.RPISingularHarnack.densityProfile_deriv_nonpos line 266
  20. theorem OAI.RPISingularHarnack.densityProfile_eventually_one line 274
  21. theorem OAI.RPISingularHarnack.radialDensityIntegrand_tendsto line 283
  22. theorem OAI.RPISingularHarnack.radialDensity_integral_tendsto line 311
  23. theorem OAI.RPISingularHarnack.minimizing_perimeter_density_monotone line 343
  24. theorem OAI.RPISingularHarnack.support_ray_inner_le_zero line 378
  25. theorem OAI.RPISingularHarnack.minimizing_cone_halfspace_radial_tangent line 486
  26. theorem OAI.RPISingularHarnack.minimizing_cone_radial_tangent_ae line 503