OAI/Geometry/BallPacking/DiskMaps/ParameterRelativeDiskMoser.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_disk_moser line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parameter_relative_corrected_disk_diffeomorphisms line 119
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.circle_volume_zero line 195
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.roundDisk_ae_closedRoundDisk line 210
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_roundDisk_eq_closedRoundDisk line 219
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.jacobian_defect_roundDisk_of_area line 223
  7. def OAI.PackingSufficiencySupport.Hamiltonian.planarHamiltonianField line 252
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarHamiltonianField_neg_area line 254
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.familyGenerator_hasDerivAt line 258
  10. structure OAI.PackingSufficiencySupport.Hamiltonian.HamiltonianDiskIsotopyFamily line 269
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_hamiltonian_disk_isotopy line 284
  12. structure OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding line 362
  13. def OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.carrier line 377
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.compact_carrier line 379
  15. def OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.Nested line 382
  16. def OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.pull line 385
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.pull_radius line 405
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.pull_carrier line 408
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.nested_pull line 414
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.PlanarDiskEmbedding.exists_isotopy line 421
  21. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.mono line 441
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.image_closedBall line 452
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_nested_disk_isotopy line 466