OAI/Geometry/BallPacking/Moser/CircleCorrection.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.circlePullback line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePullback_smooth line 16
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.circlePullback_periodic line 21
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_circle_primitive line 26
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_surjective_circle line 55
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_zero_outside_collar line 69
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_positive_lt_finite line 79
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCurl_sub_differential line 92
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_disjoint_radial_collars line 106
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.finite_potential_correction line 125
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_finite_circle_correction line 160
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_sphere_distance_bound line 179
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.lipschitz_zero_on_sphere_bound line 208
  14. def OAI.PackingSufficiencySupport.Hamiltonian.radialDrift line 221
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDrift_smooth line 224
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDrift_compact line 227
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_normSq_plane line 235
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_radialDrift_bound line 240
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.trajectory_preserves_circle line 265
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_preserves_circle line 291
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_preserves_circle_iff line 329
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_preserves_circle_iff line 342
  23. def OAI.PackingSufficiencySupport.Hamiltonian.coordinateForm line 354
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.coordinateForm_apply line 357
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.coordinateForm_smooth line 360
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.coordinateForm_compact line 364
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.form_eval_fderiv line 372
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.coordinateForm_curl line 378
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_relative_planar_primitive line 389
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserField_tangent line 432
  31. def OAI.PackingSufficiencySupport.Hamiltonian.closedRoundDisk line 445
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.closedRoundDisk_isCompact line 447
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_eq_zero_of_isLocalMax line 460
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_mapsTo_closedRoundDisk line 476
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_mapsTo_roundDisk line 499
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_image_roundDisk line 510
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_density_transport_relative line 521