OAI/Geometry/BallPacking/BallMaps/CubicBubbleSeparated.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.exists_cubic_bubble_separated line 14
  2. theorem OAI.PackingSufficiencySupport.CubicModel.cubicBubblePolynomial_complex_smooth line 83
  3. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_bubble_target_packing line 88
  4. theorem OAI.PackingSufficiencySupport.CubicModel.exists_bubble_integer_orders line 147
  5. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_standard_packing line 168
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.planeRotate_fderiv line 190
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarLiouville_rotation line 204
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarLiouville_gauge line 226
  9. def OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormPotential line 249
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormPotential_smooth line 252
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.closedOneForm_derivative_symmetric line 257
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormIntegrand_hasFDerivAt line 265
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormIntegrand_fderiv_continuous line 279
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneForm_strand_hasDerivAt line 290
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormPotential_hasFDerivAt line 306
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialOneFormPotential_fderiv line 323
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_df line 334
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_sub line 344
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_exact_primitive_comparison line 353
  20. def OAI.PackingSufficiencySupport.Hamiltonian.firstLinePrimitive line 378
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLinePrimitive_apply line 382
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLinePrimitive_family_smooth line 388
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLinePrimitive_smooth line 400
  24. def OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift line 416
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.gaugeRotation_smooth line 419
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift_smooth line 426
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift_inverse line 431
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift_isEmbedding line 443
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift_primitive line 453
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineLift_exterior line 482
  31. def OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap line 509
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap_smooth line 511
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap_derivative line 516
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstLineBaseMap_primitive line 533