OAI/Geometry/PolarProducts/PlanarSquare.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarSquare.square line 13
  2. def OAI.PlanarSquare.radius line 14
  3. def OAI.PlanarSquare.angle line 15
  4. def OAI.PlanarSquare.rotation line 16
  5. def OAI.PlanarSquare.map line 17
  6. theorem OAI.PlanarSquare.radius_pos line 19
  7. theorem OAI.PlanarSquare.radius_sq line 23
  8. theorem OAI.PlanarSquare.angle_re line 26
  9. theorem OAI.PlanarSquare.angle_im line 27
  10. theorem OAI.PlanarSquare.norm_rotation line 30
  11. theorem OAI.PlanarSquare.norm_map_sq line 32
  12. theorem OAI.PlanarSquare.map_bound line 35
  13. theorem OAI.PlanarSquare.map_injOn line 39
  14. theorem OAI.PlanarSquare.contDiffAt_map line 64
  15. theorem OAI.PlanarSquare.hasFDerivAt_radius line 71
  16. def OAI.PlanarSquare.derivative line 86
  17. theorem OAI.PlanarSquare.hasFDerivAt_map line 90
  18. theorem OAI.PlanarSquare.derivative_apply line 94
  19. def OAI.PlanarSquare.form line 100
  20. theorem OAI.PlanarSquare.form_mul line 102
  21. theorem OAI.PlanarSquare.derivative_preserves line 106
  22. abbrev OAI.PlanarCylinder.V line 125
  23. def OAI.PlanarCylinder.domain line 127
  24. def OAI.PlanarCylinder.map line 128
  25. theorem OAI.PlanarCylinder.map_apply line 132
  26. theorem OAI.PlanarCylinder.map_first line 136
  27. theorem OAI.PlanarCylinder.map_injOn line 139
  28. def OAI.PlanarCylinder.derivative line 149
  29. theorem OAI.PlanarCylinder.derivative_apply line 156
  30. theorem OAI.PlanarCylinder.hasFDerivAt_map line 162
  31. theorem OAI.PlanarCylinder.contDiffAt_map line 174
  32. def OAI.PlanarCylinder.form line 186
  33. theorem OAI.PlanarCylinder.form_eq_inner line 189
  34. theorem OAI.PlanarCylinder.derivative_preserves line 199
  35. theorem OAI.PlanarCylinder.first_bound line 211
  36. theorem OAI.PlanarCylinder.norm_bound line 216