OAI/Geometry/BallPacking/Annuli/AnnularEmbeddedChart.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_eq_densityChart line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_rectangle_domain line 19
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularPackingChart_smoothOn line 28
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularPackingChart_isEmbedding line 37
  5. def OAI.PackingSufficiencySupport.Hamiltonian.handleDensityCore line 60
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityCore_compact line 63
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityCore_subset_band line 67
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_inside line 72
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_core_zero line 85
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHandleDensity_core_support line 110
  11. def OAI.PackingSufficiencySupport.Hamiltonian.handleDensityChart line 125
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityChart_apply line 131
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityChart_source line 135
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityChart_contains line 145
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleDensityChart_coefficient line 162
  16. def OAI.PackingSufficiencySupport.Hamiltonian.handleFirstCorrection line 181
  17. def OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive line 190
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularChart_off_band line 198
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleFirstCorrection_off_band line 210
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_off_band line 229
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_zero line 241
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_smooth line 251
  23. def OAI.PackingSufficiencySupport.Hamiltonian.handleSecondExtra line 300
  24. def OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive line 308
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_zero line 318
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleSecondExtra_off_band line 330
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_off_band line 351
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_smooth line 369
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_normal line 408
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_normal line 427
  31. def OAI.PackingSufficiencySupport.Hamiltonian.annularCoverA line 450
  32. def OAI.PackingSufficiencySupport.Hamiltonian.annularCoverB line 455
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCover_form_rep line 460
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_cover line 472
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_cover line 511
  36. def OAI.PackingSufficiencySupport.Hamiltonian.annularCoverDomain line 557
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCoverDomain_open line 562
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCover_pullback_smoothAt line 567
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCover_coefficients_smooth line 579
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCover_curl line 592
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_eq_densityChart line 622
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_rectangle_domain line 626
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularPackingChart_smoothOn line 636
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularPackingChart_isEmbedding line 645
  45. def OAI.PackingSufficiencySupport.Hamiltonian.annularUnshearMap line 660
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularUnshearMap_apply line 666
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularUnshearMap_smoothOn line 672
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularUnshearMap_isEmbedding line 683
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothHomeomorph_inverse_derivative line 698
  50. def OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap line 716
  51. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap_apply line 722
  52. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap_smoothOn line 728
  53. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap_isEmbedding line 739
  54. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_mapsTo_interior line 759
  55. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_mem_band line 775
  56. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularUnshearMap_mem_interior line 781