OAI/Geometry/BallPacking/Models/RationalSlack.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.exists_rational_above_in_open line 15
  2. theorem OAI.PackingSufficiencySupport.rational_small_slack line 29
  3. theorem OAI.PackingSufficiencySupport.rational_packing_slack line 43
  4. theorem OAI.PackingSufficiencySupport.exists_rational_below_in_open line 58
  5. theorem OAI.PackingSufficiencySupport.rational_truncation_1d line 72
  6. theorem OAI.PackingSufficiencySupport.rational_truncation_2d line 85
  7. theorem OAI.PackingSufficiencySupport.smul_momentSimplex line 104
  8. def OAI.PackingSufficiencySupport.smallModelGap line 119
  9. theorem OAI.PackingSufficiencySupport.continuous_smallModelGap line 122
  10. theorem OAI.PackingSufficiencySupport.smallModelGap_eq_cappedAffine line 127
  11. theorem OAI.PackingSufficiencySupport.integral_smallModelGap line 134
  12. theorem OAI.PackingSufficiencySupport.exists_small_model_comparison_data line 149
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.actual_small_normal_packing line 211
  14. def OAI.PackingSufficiencySupport.CubicModel.physicalParameter line 293
  15. theorem OAI.PackingSufficiencySupport.CubicModel.physicalParameter_smooth line 295
  16. def OAI.PackingSufficiencySupport.CubicModel.cubicExhaustion line 299
  17. theorem OAI.PackingSufficiencySupport.CubicModel.cubicExhaustion_compact line 302
  18. def OAI.PackingSufficiencySupport.CubicModel.physicalPrimitive line 305
  19. def OAI.PackingSufficiencySupport.CubicModel.physicalArea line 310
  20. theorem OAI.PackingSufficiencySupport.CubicModel.physicalArea_continuous line 313
  21. theorem OAI.PackingSufficiencySupport.CubicModel.exists_physicalPrimitive_extension line 317
  22. theorem OAI.PackingSufficiencySupport.CubicModel.physicalPrimitive_extension_curvature line 336
  23. theorem OAI.PackingSufficiencySupport.CubicModel.physicalArea_uniform line 351
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.FormNeighborhoodEmbedding.congr_target_near line 379
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_congr_joint line 397
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_congr_near line 408
  27. theorem OAI.PackingSufficiencySupport.CubicModel.physicalArea_pos line 432
  28. theorem OAI.PackingSufficiencySupport.CubicModel.actual_cubic_representative_packing line 446