OAI/Geometry/BallPacking/Layers/PlanarRotation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.planeRotate line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRotate_smooth line 16
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRotate_zero line 20
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_planeRotate line 23
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_planeRotate line 28
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRotate_hasDerivAt line 32
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_smooth line 42
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_hasFDerivAt line 45
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_fderiv line 57
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_thin_grid line 70
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_thin_planar_embedding line 164
  12. def OAI.PackingSufficiencySupport.Hamiltonian.productForm line 190
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.productForm_apply line 195
  14. def OAI.PackingSufficiencySupport.Hamiltonian.oneCovectorForm line 198
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.oneCovectorForm_apply line 206
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.oneCovectorForm_skew line 212
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.oneCovectorForm_isInvertible line 219
  18. def OAI.PackingSufficiencySupport.Hamiltonian.planarProduct line 277
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarProduct_smooth line 280
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarProduct_fderiv line 284
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarProduct_pullback line 292
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.monotone_strip_inverse line 308