OAI/Geometry/BallPacking/Annuli/CylinderAnnularNormalization.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCylinderScalar_differential_cover line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalized_annular_scalar_intrinsic line 35
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.closed_cylinder_cover_equation line 94
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.closed_cylinder_normalized_potential line 128
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_period_one line 193
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_period_one line 197
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderCover_derivative_period_one line 203
  8. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderFormA line 221
  9. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderFormB line 224
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderForm_rep line 228
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderForm_coefficients_smooth line 241
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderForm_coefficients_periodic line 257
  13. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderFormPeriod line 269
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderFormPeriod_smooth line 273
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_comp_apply line 298
  16. def OAI.PackingSufficiencySupport.Hamiltonian.globalHandleForm line 315
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleForm_properties line 320
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleForm_annular line 339
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleForm_period line 352
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_global_handle_form line 370
  21. def OAI.PackingSufficiencySupport.Hamiltonian.restrictHandleDiffeomorph line 420
  22. def OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart line 431
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_apply line 437
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_source line 441
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_pullback line 452
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_compact line 461
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_compact_subset line 472
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_sub line 488
  29. def OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleArgument line 491
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleArgument_turn line 494
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleTurn_positiveCircleArgument line 501
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleArgument_smooth line 505
  33. def OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleCoordinate line 516
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.shortCircleArgument_bounds line 534
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleCoordinate_target line 543
  36. def OAI.PackingSufficiencySupport.Hamiltonian.torusRectangleInverse line 567
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusRectangleInverse_smooth line 570
  38. def OAI.PackingSufficiencySupport.Hamiltonian.torusRectangle line 583
  39. def OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock line 605
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_smooth line 608
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_nonneg line 612
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_turn line 615
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_tsupport line 621
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_cut line 629
  45. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_pos line 636
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_integral line 641
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.positiveCircleClock_inverse line 664
  48. def OAI.PackingSufficiencySupport.Hamiltonian.angularReparam line 711
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularReparam_fderiv line 714
  50. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseCoefficient_fderiv_at line 724
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstBaseCoefficient_fderiv_at line 730
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.weightedSecondCoefficient_fderiv_at line 737
  53. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedAreaDensity line 753
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.plane_covector_decomp line 756
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularReparam_weighted_pullback line 762