OAI/Geometry/Perimeter/Regularity/QuadraticMoment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.exactFiberHeight_measurable line 13
  2. theorem OAI.RPISingularHarnack.exactFiberHeight_norm_le line 25
  3. theorem OAI.RPISingularHarnack.exactFiberMoment_integrable line 33
  4. theorem OAI.RPISingularHarnack.normalWindowTest_integrableOn line 43
  5. theorem OAI.RPISingularHarnack.setIntegral_tsupport_mul line 54
  6. def OAI.RPISingularHarnack.normalWindowQuadratic line 60
  7. theorem OAI.RPISingularHarnack.normalWindowQuadratic_expand line 65
  8. theorem OAI.RPISingularHarnack.normalWindowQuadratic_integral_expand line 76
  9. theorem OAI.RPISingularHarnack.exactFiberQuadratic_integral_expand line 96