OAI/Geometry/BallPacking/Normal/CubicToricAmbient.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.CubicModel.CubicConeModel line 14
  2. abbrev OAI.PackingSufficiencySupport.CubicModel.CubicConeSpace line 15
  3. abbrev OAI.PackingSufficiencySupport.CubicModel.CubicConeTarget line 16
  4. abbrev OAI.PackingSufficiencySupport.CubicModel.CubicAmbient line 17
  5. def OAI.PackingSufficiencySupport.CubicModel.ambientWeightedCoefficient line 19
  6. theorem OAI.PackingSufficiencySupport.CubicModel.ambientWeightedCoefficient_smooth line 23
  7. theorem OAI.PackingSufficiencySupport.CubicModel.ambientWeightedCoefficient_restrict line 28
  8. theorem OAI.PackingSufficiencySupport.CubicModel.ambientWeightedCoefficient_none line 31
  9. def OAI.PackingSufficiencySupport.CubicModel.conePolynomial line 34
  10. theorem OAI.PackingSufficiencySupport.CubicModel.conePolynomial_smooth line 38
  11. theorem OAI.PackingSufficiencySupport.CubicModel.conePolynomial_nonzero line 50
  12. def OAI.PackingSufficiencySupport.CubicModel.cubicConePrimitive line 63
  13. theorem OAI.PackingSufficiencySupport.CubicModel.cubicConePrimitive_smooth line 66
  14. def OAI.PackingSufficiencySupport.CubicModel.cubicNormalCoordinates line 74
  15. theorem OAI.PackingSufficiencySupport.CubicModel.cubicNormalCoordinates_smooth line 77
  16. def OAI.PackingSufficiencySupport.CubicModel.cubicAmbientPrimitive line 80
  17. def OAI.PackingSufficiencySupport.CubicModel.cubicAmbientForm line 83
  18. def OAI.PackingSufficiencySupport.CubicModel.centralCubicCoordinates line 86
  19. def OAI.PackingSufficiencySupport.CubicModel.centralCubicPrimitive line 88
  20. theorem OAI.PackingSufficiencySupport.CubicModel.centralCubicCoordinates_smooth line 91
  21. theorem OAI.PackingSufficiencySupport.CubicModel.exists_actual_cubic_exact_family_with_zero line 96
  22. theorem OAI.PackingSufficiencySupport.CubicModel.exists_actual_cubic_exact_family line 167
  23. def OAI.PackingSufficiencySupport.CubicModel.physicalDiskRecovery line 184
  24. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskRecovery_smooth line 187
  25. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskRecovery_left line 196
  26. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskRecovery_right line 205
  27. theorem OAI.PackingSufficiencySupport.CubicModel.physicalDiskCoordinates_isEmbedding line 212
  28. theorem OAI.PackingSufficiencySupport.CubicModel.exists_compact_physical_radial_bridge line 222
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackOneForm_comp_at line 301
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldPullbackOneForm_primitive_at line 311
  31. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_radial_primitive line 327
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.coupling_exterior_of_primitive_germ line 377
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.exact_path_local_transport_derivative line 400
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_short_exact_moser line 433