OAI/Geometry/BallPacking/Annuli/QuadricNormalizedCycle.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitTransverseCycle line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitTransverseCycle_smooth line 17
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitTransverseCycle_periodic line 21
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.unitTransverseCycle_pullback line 27
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_unit_period line 55
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_not_exact line 64
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_affine line 92
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_periodic line 117
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_period_integral line 126
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderFormB_curve line 133
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_parameter_pullback line 153
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_Acoordinate line 175
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_transverseBranch line 181
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_core_cycle line 195
  15. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.cylinderDualForm line 203
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.cylinderDualForm_B line 206
  17. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.cylinderDualForm_period line 214
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar_joint_smoothOn line 245
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedAnnularPrimitive_cylinder_joint_smoothOn line 273
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldScalarDifferential_comp_at line 300
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar_family_pullback_smoothOn line 308
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar_pullback_differential line 323
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_closed_annular_coordinate_potential line 362
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_intrinsic_annular_coordinate_potential line 411