OAI/Geometry/BallPacking/Toric/SixModelComparisonData.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.exists_six_model_comparison_data line 13
  2. theorem OAI.PackingSufficiencySupport.CubicModel.actual_six_cubic_inner_normal_packing_large line 86
  3. def OAI.PackingSufficiencySupport.Hamiltonian.complexBlocks line 161
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_add line 163
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_product line 166
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexBlocks_sq line 170
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexBlocks_area line 175
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.hopfPrimitive_complexBlocks line 190
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexBlocks_hasFDerivAt line 209
  10. abbrev OAI.PackingSufficiencySupport.FiniteMoment.Radial.DiskPair line 231
  11. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii line 233
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii_nonneg line 235
  13. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii_contDiff line 238
  14. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskDomain line 245
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskDomain_isOpen line 248
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii_mem_lower line 252
  17. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskForward line 256
  18. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse line 260
  19. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.normSq_real_smul line 264
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii_forward line 269
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.squaredRadii_inverse line 283
  22. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskForward_inverse line 303
  23. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.diskInverse_forward line 315
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_real_smul line 333
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexArea_power_derivative line 338
  26. def OAI.PackingSufficiencySupport.Hamiltonian.complexMonomial line 351
  27. def OAI.PackingSufficiencySupport.Hamiltonian.complexMonomialDerivative line 353
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMonomial_contDiff line 357
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMonomial_hasFDerivAt line 360
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMonomial_normSq line 370
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexMonomial_area line 374
  32. def OAI.PackingSufficiencySupport.Hamiltonian.toricLift line 392
  33. def OAI.PackingSufficiencySupport.Hamiltonian.toricLiftDifferential line 395
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricLift_sq line 399
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricLift_primitive line 405
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricLift_contDiff line 437
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricLift_fderiv line 444
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.toricLift_pullback_primitive line 465