OAI/MathematicalPhysics/SheetFlows/Localization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows localization.

  1. def OAI.Solenoidal.Rectangle.CollarSeparated line 14
  2. theorem OAI.Solenoidal.Rectangle.disjoint_of_separated line 18
  3. theorem OAI.Solenoidal.Rectangle.exists_coordinate_gap line 28
  4. theorem OAI.Solenoidal.Rectangle.collar_of_coordinate_gap line 49
  5. theorem OAI.Solenoidal.Rectangle.exists_rational_collar line 64
  6. theorem OAI.Solenoidal.Rectangle.CollarSeparated.mono line 101
  7. theorem OAI.Solenoidal.SheetData.exists_rational_collar line 107
  8. theorem OAI.Solenoidal.Rectangle.center_bounds line 116
  9. theorem OAI.Solenoidal.Rectangle.point_bounds line 124
  10. structure OAI.Solenoidal.Collar line 130
  11. def OAI.Solenoidal.lifted line 137
  12. def OAI.Solenoidal.verticalPulse line 139
  13. theorem OAI.Solenoidal.verticalPulse_field line 159
  14. theorem OAI.Solenoidal.rect_support_chart line 166
  15. theorem OAI.Solenoidal.correction_off line 174
  16. theorem OAI.Solenoidal.rect_profile_one line 183
  17. theorem OAI.Solenoidal.verticalPulse_own line 195
  18. theorem OAI.Solenoidal.rect_profile_gap_zero line 205
  19. theorem OAI.Solenoidal.verticalPulse_off_same line 218
  20. theorem OAI.Solenoidal.verticalPulse_off_far line 233
  21. def OAI.Solenoidal.horizontalPulse line 251
  22. theorem OAI.Solenoidal.horizontalPulse_field line 265
  23. theorem OAI.Solenoidal.horizontalPulse_on line 270
  24. theorem OAI.Solenoidal.horizontalPulse_off line 278
  25. theorem OAI.Solenoidal.StationaryPulse.scale_field line 286
  26. def OAI.Solenoidal.travelProgram line 289
  27. theorem OAI.Solenoidal.travelProgram_on line 292
  28. theorem OAI.Solenoidal.travelProgram_off line 306