OAI/Geometry/BallPacking/Annuli/QuadricCylinderChart.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_apply line 20
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_symm_apply line 23
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_source line 29
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_core line 37
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_transverseCylinderWidth line 41
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinderWidth line 58
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinderWidth_pos line 60
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinderWidth_subset line 63
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCylinder_compact line 67
  11. def OAI.PackingSufficiencySupport.complexClosedAnnulus line 78
  12. theorem OAI.PackingSufficiencySupport.complexClosedAnnulus_isCompact line 80
  13. theorem OAI.PackingSufficiencySupport.complex_normalize_dist line 87
  14. theorem OAI.PackingSufficiencySupport.exists_complexClosedAnnulus_subset line 98
  15. abbrev OAI.PackingSufficiencySupport.Hamiltonian.RadialPlane line 126
  16. def OAI.PackingSufficiencySupport.Hamiltonian.planeRadiusSq line 128
  17. def OAI.PackingSufficiencySupport.Hamiltonian.planeRadialStep line 130
  18. def OAI.PackingSufficiencySupport.Hamiltonian.planeClosedAnnulus line 133
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRadiusSq_norm line 136
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRadialStep_smooth line 141
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeClosedAnnulus_compact line 145
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRadialStep_zero line 156
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRadialStep_one line 164
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRadialDifferential_zero line 172
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_annulusWidth line 203
  26. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusWidth line 212
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusWidth_pos line 214
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusWidth_lt line 216
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.annulusWidth_subset line 218
  30. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm line 221
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_smooth line 225
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_compact line 232
  33. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_closed line 238
  34. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_pullback line 246
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_support line 251
  36. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint line 258
  37. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint_mem line 262
  38. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle line 281
  39. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_periodic line 283
  40. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint_smooth line 288
  41. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_smooth line 306
  42. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint_first line 311
  43. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint_zero line 313
  44. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transversePoint_one line 316
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_coordinate line 323
  46. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_branch_iff line 329
  47. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRadius line 356
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRadius_pos line 358
  49. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseCycle_coord_norm line 365
  50. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRadius_smooth line 371
  51. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRadius_lower line 375
  52. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRadius_upper line 381
  53. def OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm line 398
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_smooth line 401
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_scalar line 411
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.curveOneForm_pushforward_scalar line 419
  57. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRealCoordinate line 447
  58. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseStep line 450
  59. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle line 452
  60. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseRealCoordinate_smooth line 454
  61. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseStep_smooth line 458
  62. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle_smooth line 461
  63. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle_zero line 464
  64. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle_deriv line 472
  65. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseStep_lower line 480
  66. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseStep_upper line 486
  67. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle_integral_first line 492
  68. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.dualAlongCycle_integral_second line 503
  69. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.compactDualForm_period line 513