OAI/Geometry/BallPacking/Annuli/AnnularChartNormalization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_primitive_on_annular_chart line 18
  2. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderClockPrimitive line 107
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderClockPrimitive_smoothAt line 111
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderClockPrimitive_exterior_cover line 122
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderClockPrimitive_exterior line 149
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_annular_dual_normalization line 180
  7. instance OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.surfaceSigmaCompact line 281
  8. def OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.restrictedTransverseCylinder line 284
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.restrictedTransverseCylinder_source line 289
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_actual_compact_normalized_dual_fixed line 296
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_actual_compact_normalized_dual line 343
  12. structure OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData line 366
  13. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.band line 388
  14. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.core line 390
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.band_compact line 393
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.core_compact line 395
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.core_subset_band line 398
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.band_subset_source line 401
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.image_band_compact line 407
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.image_core_compact line 412
  21. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_fixed_annularHandleData line 425
  22. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_annularHandleData line 438
  23. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderRadialForm line 447
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinder_fst_smooth line 450
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderRadialForm_smooth line 455
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderRadialForm_apply line 460
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderRadialForm_zero line 474
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderRadialForm_closed line 486