OAI/Geometry/BallPacking/Models/DisjointClocks.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.firstClock line 12
  2. def OAI.PackingSufficiencySupport.Hamiltonian.secondClock line 13
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_smooth line 15
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_smooth line 17
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_zero line 20
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_zero line 22
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_one line 24
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_one line 26
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_locally_zero line 29
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_locally_one line 35
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_deriv_zero line 41
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_deriv_zero line 44
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstClock_deriv_compact line 47
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.secondClock_deriv_compact line 59
  15. def OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap line 75
  16. def OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatHamiltonian line 78
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatHamiltonian_smooth line 81
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatHamiltonian_compact line 86
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_smooth line 91
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_inverse_smooth line 96
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_zero line 101
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_one line 106
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_flow line 110
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_symplectic line 136
  25. def OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.after line 146
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatMap_preserves line 169
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.concatHamiltonian_face line 175
  28. def OAI.PackingSufficiencySupport.Hamiltonian.CompactHamiltonianIsotopy.refl line 198
  29. theorem OAI.PackingSufficiencySupport.MomentPolytope.exists_lifted_rearrangement_convex line 226
  30. theorem OAI.PackingSufficiencySupport.MomentPolytope.exists_successive_rearrangement line 252
  31. theorem OAI.PackingSufficiencySupport.MomentPolytope.hamiltonian_comparison line 307
  32. theorem OAI.PackingSufficiencySupport.MomentPolytope.positive_hamiltonian_comparison line 341
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.isCompact_preimage_planeMoments line 390
  34. theorem OAI.PackingSufficiencySupport.MomentPolytope.planeRegion_isCompact line 419
  35. theorem OAI.PackingSufficiencySupport.MomentPolytope.planeRegion_nonempty line 423
  36. def OAI.PackingSufficiencySupport.Hamiltonian.smoothUpperPositivePart line 437
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothUpperPositivePart_smooth line 439
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothUpperPositivePart_bounds line 444
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_positive_caps line 462