OAI/Geometry/BallPacking/Moser/PlanarCorrection.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_planar_primitive line 13
  2. abbrev OAI.PackingSufficiencySupport.Hamiltonian.Plane line 60
  3. def OAI.PackingSufficiencySupport.Hamiltonian.planarArea line 62
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarArea_apply line 68
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarArea_trace_identity line 70
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothTransition_deriv_compact line 80
  7. def OAI.PackingSufficiencySupport.Hamiltonian.moserDensity line 94
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserDensity_positive line 97
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserDensity_smooth line 108
  10. def OAI.PackingSufficiencySupport.Hamiltonian.moserField line 112
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserField_smooth line 116
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserField_hasCompactSupport line 126
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.plane_deriv_first line 138
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.plane_deriv_second line 143
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasDerivAt_horizontal_first line 148
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.hasDerivAt_horizontal_second line 154
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.moserField_transport line 160
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_planar_moser_correction line 225
  19. def OAI.PackingSufficiencySupport.Hamiltonian.planarCurl line 250
  20. def OAI.PackingSufficiencySupport.Hamiltonian.pullbackForm line 253
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.bilinear_skew_plane line 256
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.pullbackForm_smooth line 265
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.pullbackForm_curl line 270
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_curl_rectangle line 291
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_smooth line 322
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_deriv_first line 326
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_deriv_second line 331
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_area line 336
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_curl_polar_rectangle line 343
  30. def OAI.PackingSufficiencySupport.Hamiltonian.roundDisk line 368
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.polar_mem_roundDisk line 370
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_roundDisk_polar line 379
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_curl_roundDisk line 411
  34. def OAI.PackingSufficiencySupport.Hamiltonian.periodicPrimitive line 419
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodicPrimitive_hasDerivAt line 421
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodicPrimitive_smooth line 426
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodicPrimitive_periodic line 435
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodic_arg_neg line 447
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiffAt_arg_slit line 465
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodic_arg_smooth line 472
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.periodic_arg_polar line 485
  42. def OAI.PackingSufficiencySupport.Hamiltonian.radiusSq line 497
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_smooth line 498
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_polar line 500
  45. def OAI.PackingSufficiencySupport.Hamiltonian.angularExtension line 504
  46. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_zero line 508
  47. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_smooth line 515
  48. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_compact line 537
  49. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularExtension_polar line 553