OAI/Geometry/BallPacking/Moser/DiskMoser.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDisk_pullback_compact line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_disk_moser line 36
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarArea_map line 141
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.family_spatial_fderiv line 151
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.family_spatial_fderiv_smooth line 159
  6. def OAI.PackingSufficiencySupport.Hamiltonian.spatialJacobian line 167
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialJacobian_smooth line 170
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialJacobian_support line 183
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_image_of_fixed_compl line 198
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialJacobian_integral line 214
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_corrected_disk_diffeomorphisms line 251
  12. def OAI.PackingSufficiencySupport.Hamiltonian.rectangularPotential line 322
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectangularPotential_smooth line 326
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectangularPotential_eq_of_hasFDerivAt line 338
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectangularPotential_hasFDerivAt line 359
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_closed_primitive line 372
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.compact_potential_zero_outside line 431
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_disk_closed_primitive line 474