OAI/Geometry/BallPacking/Flows/AnnularInverseDomain.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.handleAnnularCover_mem_band line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularUnshearMap_mem_interior line 22
  3. def OAI.PackingSufficiencySupport.Hamiltonian.annularCoverTwoCoefficient line 45
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCoverDomain_eq line 51
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCoverTwoCoefficient_smooth line 58
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCoverTwoCoefficient_ne_zero line 70
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCoverTwoCoefficient_positive line 101
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularCover_positive_exterior line 136
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.handleAnnularCover_surjOn line 158
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularPackingRectangle_subset line 179
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.annularPackingGeometry line 186
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.AnnularHandleData.annularPackingGeometry line 217
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_base_germs line 251
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_congr_germ line 263
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceFirstPath_isInvertible_local line 267
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondPath_isInvertible_local line 295
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.horizontalCoupling_congr_germ line 330
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.baseShear_weighted_pullback_local line 340
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceSecondEndpoint_shear_pullback line 385
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.annular_normalForm_cover line 418
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceFirstPrimitive_cover_germ line 429
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalSurfaceSecondPrimitive_cover_germ line 450
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.circleWeight_radial_deriv line 472