OAI/Geometry/BallPacking/Annuli/AnnularHandleDensity.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.radial line 15
  2. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density line 18
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_smooth line 21
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_pullback line 34
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_band_zero line 56
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_core_zero line 64
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_compact line 85
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.density_cover line 90
  9. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderRectangleInverse line 117
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.cylinderRectangleInverse_smooth line 120
  11. def OAI.PackingSufficiencySupport.Hamiltonian.cylinderRectangle line 128
  12. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.densityChart line 146
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.densityChart_apply line 150
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.densityChart_source line 153
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.densityChart_contains line 161
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusFirstForm_clock_zero line 179
  17. def OAI.PackingSufficiencySupport.Hamiltonian.globalHandleRadialForm line 194
  18. def OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity line 199
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_smooth line 204
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_zero line 222
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_compact line 232
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_pullback line 241
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_turns line 261
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnulusMap_derivative line 275
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.torusAnnularDensity_cylinder line 301
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_annular line 331
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.partial_inverse_oneForm_smooth line 357
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.partial_inverse_oneForm_exterior line 371
  29. def OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularClockPrimitive line 401
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularClockPrimitive_smooth line 408
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularClockPrimitive_exterior line 417
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularClockPrimitive_eq line 430
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_coefficient line 458
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.annular_coefficient_smooth_on line 464
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.annular_inverse_fst_smooth line 485
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.image_band_subset_target line 504
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.off_band_inverse line 509
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.radial_zero line 514
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.radial_pullback line 518
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.radial_smooth line 529