OAI/Analysis/LipschitzHilbert/Geometry/RectangleProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact coordinate projections and exact change of orthogonal coordinates for the popularity packing in Lacey--Li (3.11).

  1. theorem OAI.LipschitzHilbert.Rectangle.isClosed_carrier line 13
  2. theorem OAI.LipschitzHilbert.Rectangle.isCompact_carrier line 18
  3. theorem OAI.LipschitzHilbert.Rectangle.isCompact_popularSet line 24
  4. theorem OAI.LipschitzHilbert.Rectangle.continuous_orthogonalCoordinates line 29
  5. def OAI.LipschitzHilbert.Rectangle.coordinateProjection line 33
  6. theorem OAI.LipschitzHilbert.Rectangle.isCompact_coordinateProjection line 36
  7. theorem OAI.LipschitzHilbert.Rectangle.change_transverse_coordinates line 40
  8. theorem OAI.LipschitzHilbert.Rectangle.coordinate_projection_area line 54
  9. theorem OAI.LipschitzHilbert.Rectangle.popular_projection_density line 83
  10. theorem OAI.LipschitzHilbert.Rectangle.projection_in_long_interval line 100