OAI/Analysis/LipschitzHilbert/Geometry/NearRectangleSection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A transverse section bound for intersecting rectangles. This is the area-to-line reduction behind the near-angle part of Lacey--Li (3.5).

  1. def OAI.LipschitzHilbert.Rectangle.nearSection line 12
  2. theorem OAI.LipschitzHilbert.Rectangle.coordinate_difference line 16
  3. theorem OAI.LipschitzHilbert.Rectangle.near_intersection_coordinates line 21
  4. theorem OAI.LipschitzHilbert.Rectangle.near_intersection_area line 43