OAI/Geometry/BallPacking/Moser/ParametricMoser.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_relative_primitive line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.parametric_backgroundField_smooth line 84
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.parametric_backgroundField_compact line 102
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_relative_background_moser line 117
  5. def OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart line 166
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_source line 171
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_target line 176
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_apply line 187
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_smooth line 198
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_symm_smooth line 202
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_nonneg line 214
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_fderiv line 217
  13. def OAI.PackingSufficiencySupport.Hamiltonian.radialDiskDensity line 241
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskDensity_pos line 243
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskDensity_smooth line 247
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarArea_radial_rank_one line 252
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_area line 261
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_smul line 275
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_radiusSq line 279
  20. def OAI.PackingSufficiencySupport.Hamiltonian.diskChartRadius line 286
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.diskChartRadius_pos line 288
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_closed_iff line 294
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_open_iff line 305
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_image_closed line 316
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_image_open line 333
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.diskChartRadius_strictMonoOn line 350
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_det line 362
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_det line 372
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_integral line 377
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialDiskChart_integral_inner line 385
  31. def OAI.PackingSufficiencySupport.Chart.conjugate line 410
  32. theorem OAI.PackingSufficiencySupport.Chart.conjugate_of_mem line 415
  33. theorem OAI.PackingSufficiencySupport.Chart.conjugate_of_notMem line 420
  34. theorem OAI.PackingSufficiencySupport.Chart.conjugate_apply line 425
  35. theorem OAI.PackingSufficiencySupport.Chart.conjugate_comp line 431
  36. theorem OAI.PackingSufficiencySupport.Chart.conjugate_id line 441
  37. def OAI.PackingSufficiencySupport.Chart.conjugateEquiv line 448
  38. theorem OAI.PackingSufficiencySupport.Chart.conjugate_eq_of_notMem_image line 463
  39. theorem OAI.PackingSufficiencySupport.Chart.conjugate_smooth_compact line 477
  40. theorem OAI.PackingSufficiencySupport.Chart.inverse_displacement_compact line 516
  41. def OAI.PackingSufficiencySupport.Chart.conjugateHomeomorph line 526
  42. theorem OAI.PackingSufficiencySupport.Chart.conjugate_image line 553
  43. theorem OAI.PackingSufficiencySupport.Chart.conjugate_contDiffAt_of_mem line 560
  44. theorem OAI.PackingSufficiencySupport.Chart.chart_fderiv_right_inverse line 570
  45. theorem OAI.PackingSufficiencySupport.Chart.conjugate_fderiv_chart line 583
  46. theorem OAI.PackingSufficiencySupport.Chart.fiber_displacement_compact line 600
  47. theorem OAI.PackingSufficiencySupport.Chart.exists_conjugate_family line 608