OAI/Analysis/LipschitzHilbert/Estimates/TopAreaAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized intersection averages and top-area weights.

  1. def OAI.LipschitzHilbert.SlopeBox.area line 12
  2. theorem OAI.LipschitzHilbert.SlopeBox.area_pos line 14
  3. def OAI.LipschitzHilbert.SlopeBox.areaWeight line 16
  4. theorem OAI.LipschitzHilbert.SlopeBox.coe_areaWeight line 18
  5. theorem OAI.LipschitzHilbert.SlopeBox.ennreal_areaWeight line 20
  6. def OAI.LipschitzHilbert.SlopeBox.dilationAverage line 23
  7. theorem OAI.LipschitzHilbert.SlopeBox.dilationAverage_nonneg line 26
  8. theorem OAI.LipschitzHilbert.SlopeBox.dilationAverage_normalized line 33
  9. theorem OAI.LipschitzHilbert.SlopeBox.dilation_intersection_eq line 46
  10. theorem OAI.LipschitzHilbert.SlopeBox.sum_dilation_intersection_eq line 56