OAI/Geometry/Perimeter/Regularity/WindowAverage.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.lineWindow line 11
  2. theorem OAI.RPISingularHarnack.lineWindow_measurable line 13
  3. theorem OAI.RPISingularHarnack.lineWindow_integrable line 16
  4. theorem OAI.RPISingularHarnack.lineWindow_lintegral line 19
  5. theorem OAI.RPISingularHarnack.lineWindow_translation_le line 29
  6. def OAI.RPISingularHarnack.normalWindowAverage line 87
  7. theorem OAI.RPISingularHarnack.normalWindowAverage_stronglyMeasurable line 90
  8. theorem OAI.RPISingularHarnack.integrable_window_fiber line 97
  9. theorem OAI.RPISingularHarnack.normalWindowAverage_lintegral_le line 110
  10. theorem OAI.RPISingularHarnack.normalWindowAverage_translation_le line 134
  11. theorem OAI.RPISingularHarnack.normalWindowAverage_add_smul line 152
  12. theorem OAI.RPISingularHarnack.normalWindowAverage_normal_translation_le line 166
  13. theorem OAI.RPISingularHarnack.translation_lintegral_add_le line 210
  14. theorem OAI.RPISingularHarnack.normalWindowAverage_all_translation_le line 230