OAI/Geometry/BallPacking/BallMaps/QuadricLargeAmbientPacking.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.actual_large_polynomial_packing line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_exterior_at line 92
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_congr_nhds line 107
  4. def OAI.PackingSufficiencySupport.Hamiltonian.firstDiskDomain line 116
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskDomain_open line 118
  6. def OAI.PackingSufficiencySupport.Hamiltonian.firstDiskScale line 121
  7. def OAI.PackingSufficiencySupport.Hamiltonian.firstDiskUnscale line 123
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskScale_smoothOn line 126
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskUnscale_smoothOn line 131
  10. def OAI.PackingSufficiencySupport.Hamiltonian.firstDiskScaleHomeomorph line 137
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskScale_isEmbedding line 162
  12. def OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlanePrimitive line 167
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.phasePlusPlanePrimitive_smooth line 171
  14. def OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial line 175
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial_smoothOn line 178
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial_isEmbedding line 183
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial_primitive line 190
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.firstDiskRadial_exterior line 220
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanTimeField_smooth line 235
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclidean_nonautonomous_curve_eqOn_Icc line 244
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.closed_flow_linear_equivariant_on line 253
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.closed_flow_linear_fixed_on line 269
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.homogeneousCone_shell_flow_linear_equivariant line 284
  24. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.HomogeneousInput line 323
  25. abbrev OAI.PackingSufficiencySupport.DiagonalQuadrics.HomogeneousOutput line 324
  26. def OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial line 326
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_smooth line 333
  28. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_homogeneous line 344
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_zero_iff line 351
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_nonzero line 370
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_affine line 374
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_euler line 385
  33. def OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian line 402
  34. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_smooth line 406
  35. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_nonzero line 412
  36. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_fderiv line 420
  37. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_euler line 430
  38. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_J line 439
  39. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousQuadricCone_isInvertible line 448
  40. def OAI.PackingSufficiencySupport.Hamiltonian.infinitySign line 463
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.infinitySign_unit line 468
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexDiagonal_infinity_fixed line 472
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.phaseUnitDiagonal_infinity_fixed line 484
  44. def OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousInfinityOutputSign line 500
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousInfinityOutputSign_unit line 504
  46. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousPolynomial_infinity line 509
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_diagonal line 517
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_circle line 529
  49. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.homogeneousCartesian_infinity line 538