OAI/Geometry/BallPacking/Moments/ConvexWeights.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.FiniteMoment.convexHull_range_weights line 15
  2. def OAI.PackingSufficiencySupport.FiniteMoment.closedTrapezoid line 33
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.closedTrapezoid_mem_convexHull line 36
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.convex_affine_height_preimage line 67
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.convex_zero_height_preimage line 76
  6. def OAI.PackingSufficiencySupport.FiniteMoment.markedHeight line 82
  7. def OAI.PackingSufficiencySupport.FiniteMoment.heightGraph line 83
  8. def OAI.PackingSufficiencySupport.FiniteMoment.heightHull line 85
  9. def OAI.PackingSufficiencySupport.FiniteMoment.latticeIndex line 87
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.lattice_height_mem line 90
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.lattice_lower_mem line 94
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.lattice_upper_mem line 101
  13. theorem OAI.PackingSufficiencySupport.FiniteMoment.lower_height_mem line 108
  14. theorem OAI.PackingSufficiencySupport.FiniteMoment.convex_diagonal_segment line 137
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.convex_horizontal_segment line 150
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.convex_vertical_segment line 164
  17. theorem OAI.PackingSufficiencySupport.FiniteMoment.upper_height_mem line 182
  18. theorem OAI.PackingSufficiencySupport.FiniteMoment.markedHeight_feasible line 220
  19. theorem OAI.PackingSufficiencySupport.FiniteMoment.markedHeight_jensen line 234
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.marked_gibbs_error line 249
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_affine_height line 273
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_partition_primitive_mod_bump line 302
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_primitive_near_proper_compact line 404
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_zero_form line 469
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_sum line 474
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_sum line 484