OAI/Analysis/LipschitzHilbert/Geometry/RectangleDilation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual rectangle dilations and containment of intersecting rectangles with controlled relative angle, as used in Lacey--Li (3.4).

  1. def OAI.LipschitzHilbert.Rectangle.dilate line 12
  2. theorem OAI.LipschitzHilbert.Rectangle.mem_dilate line 20
  3. theorem OAI.LipschitzHilbert.Rectangle.carrier_subset_dilate line 25
  4. theorem OAI.LipschitzHilbert.Rectangle.volume_dilate line 34
  5. theorem OAI.LipschitzHilbert.Rectangle.abs_coordinate_le_norm line 40
  6. theorem OAI.LipschitzHilbert.Rectangle.coordinate_difference_zero line 45
  7. theorem OAI.LipschitzHilbert.Rectangle.coordinate_difference_one line 53
  8. theorem OAI.LipschitzHilbert.Rectangle.transverse_axis_le line 61
  9. theorem OAI.LipschitzHilbert.Rectangle.transverse_difference_le line 69
  10. theorem OAI.LipschitzHilbert.Rectangle.controlled_angle_containment line 94