OAI/MathematicalPhysics/SheetFlows/RectangleGeometry.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows rectangle geometry.

  1. theorem OAI.Solenoidal.Rectangle.halfWidth_pos line 15
  2. theorem OAI.Solenoidal.Rectangle.center_sub_halfWidth line 20
  3. theorem OAI.Solenoidal.Rectangle.center_add_halfWidth line 25
  4. theorem OAI.Solenoidal.Rectangle.mem_iff_abs line 30
  5. theorem OAI.Solenoidal.Rectangle.center_mem line 45
  6. theorem OAI.Solenoidal.Rectangle.upper_mem line 50
  7. theorem OAI.Solenoidal.Rectangle.halfWidth_le_half line 55
  8. theorem OAI.Solenoidal.Rectangle.offset_bound line 62
  9. theorem OAI.Solenoidal.diagonalMap_upper line 69
  10. theorem OAI.Solenoidal.SheetData.ratio_mul_halfWidth line 92
  11. theorem OAI.Solenoidal.SheetData.ratio_eq_halfWidth_ratio line 101
  12. theorem OAI.Solenoidal.SheetData.scaled_offset_bound line 107
  13. abbrev OAI.Solenoidal.OffsetHeight line 119
  14. def OAI.Solenoidal.verticalShear line 121
  15. def OAI.Solenoidal.horizontalShear line 124
  16. def OAI.Solenoidal.threeShears line 127
  17. theorem OAI.Solenoidal.threeShears_action line 131
  18. theorem OAI.Solenoidal.threeShears_on_sheet line 140
  19. def OAI.Solenoidal.coreMatrix₂ line 144
  20. theorem OAI.Solenoidal.coreMatrix₂_det line 147
  21. def OAI.Solenoidal.tripleX line 151
  22. def OAI.Solenoidal.tripleY line 154
  23. def OAI.Solenoidal.sixShears line 157
  24. theorem OAI.Solenoidal.sixShears_action line 160
  25. theorem OAI.Solenoidal.sixShears_on_sheet line 169
  26. def OAI.Solenoidal.coreMatrix₃ line 174
  27. theorem OAI.Solenoidal.coreMatrix₃_mulVec line 179
  28. theorem OAI.Solenoidal.coreMatrix₃_det line 187
  29. def OAI.Solenoidal.centeredCore line 193
  30. theorem OAI.Solenoidal.centeredCore_on_sheet line 196
  31. theorem OAI.Solenoidal.abs_convex_combination_le line 206
  32. theorem OAI.Solenoidal.first_phase line 221
  33. theorem OAI.Solenoidal.middle_phase line 224
  34. theorem OAI.Solenoidal.last_phase line 229
  35. theorem OAI.Solenoidal.triple_path_bounds line 238
  36. theorem OAI.Solenoidal.processing_height_bound line 257