OAI/Analysis/LipschitzHilbert/Geometry/NearRectangleLine.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Projection of a transverse rectangle section onto an actual line. The dilation is explicit, and no geometric covering hypothesis is assumed.

  1. def OAI.LipschitzHilbert.Rectangle.projectionTime line 12
  2. theorem OAI.LipschitzHilbert.Rectangle.line_coordinate line 15
  3. theorem OAI.LipschitzHilbert.Rectangle.projectionTime_bound line 22
  4. theorem OAI.LipschitzHilbert.Rectangle.projected_point_mem_dilate line 35
  5. def OAI.LipschitzHilbert.Rectangle.nearLineParameters line 70
  6. theorem OAI.LipschitzHilbert.Rectangle.nearSection_measurable line 73
  7. theorem OAI.LipschitzHilbert.Rectangle.nearLineParameters_subset line 76
  8. theorem OAI.LipschitzHilbert.Rectangle.nearSection_le_lineParameters line 94
  9. theorem OAI.LipschitzHilbert.Rectangle.nearSection_le_line_integral line 112