OAI/Geometry/Perimeter/Regularity/PhaseMomentLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.phaseMollification_c1_eq line 12
  2. theorem OAI.RPISingularHarnack.phaseMollification_ae_tendsto line 21
  3. theorem OAI.RPISingularHarnack.phaseMollification_c1_mem_Icc line 32
  4. theorem OAI.RPISingularHarnack.phaseMollification_diffuse_tendsto_zero line 38
  5. def OAI.RPISingularHarnack.exactFiberHeight line 63
  6. theorem OAI.RPISingularHarnack.phaseMollification_fiber_ae_tendsto line 67
  7. theorem OAI.RPISingularHarnack.mollified_fiber_height_ae_tendsto line 77
  8. theorem OAI.RPISingularHarnack.interval_height_abs_le line 103
  9. theorem OAI.RPISingularHarnack.mollified_fiber_height_square_tendsto line 121