OAI/Geometry/RecorderBoxes/Bounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Rectangle widths, chart bounds and centered affine displacement estimates.

  1. def OAI.Solenoidal.Bridge.Rectangle.center line 12
  2. def OAI.Solenoidal.Bridge.Rectangle.halfWidth line 15
  3. def OAI.Solenoidal.Bridge.Rectangle.PositiveSides line 18
  4. theorem OAI.Solenoidal.Bridge.source_positive line 21
  5. theorem OAI.Solenoidal.Bridge.target_positive line 25
  6. theorem OAI.Solenoidal.Bridge.physical_sides_positive line 34
  7. theorem OAI.Solenoidal.Bridge.physical_halfWidth_le line 40
  8. theorem OAI.Solenoidal.Bridge.rectangle_widths line 50
  9. theorem OAI.Solenoidal.Bridge.Rectangle.offset_bound line 62
  10. theorem OAI.Solenoidal.Bridge.Rectangle.center_in_unit line 68
  11. theorem OAI.Solenoidal.Bridge.physical_center line 77
  12. theorem OAI.Solenoidal.Bridge.physical_center_bounds line 81
  13. def OAI.Solenoidal.Bridge.centerRegion line 100
  14. theorem OAI.Solenoidal.Bridge.physical_center_mem_region line 102
  15. theorem OAI.Solenoidal.Bridge.chart_bounds line 117
  16. theorem OAI.Solenoidal.Bridge.affine_lower line 133
  17. theorem OAI.Solenoidal.Bridge.affine_upper line 139
  18. theorem OAI.Solenoidal.Bridge.affine_center line 146
  19. theorem OAI.Solenoidal.Bridge.affine_centered line 162
  20. theorem OAI.Solenoidal.Bridge.branch_offset_bounds line 179