OAI/Geometry/BallPacking/Necessity/PackingNecessity.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.normalized_two_ball_obstruction line 41
  2. def OAI.HigherDimensionalBallPacking.Rigidity.symplecticBilin line 59
  3. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticBilin_nondegenerate line 89
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.abs_det_of_standardForm line 101
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_volume_closedBall line 124
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_real_smul line 148
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.closedBall_eq_smul_unit line 154
  8. theorem OAI.HigherDimensionalBallPacking.Rigidity.volume_closedBall_capacity line 171
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.unit_capacity_volume_pos line 179
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.packing_exists_smaller_capacity line 185
  11. theorem OAI.HigherDimensionalBallPacking.packing_volume_obstruction line 217
  12. def OAI.HigherDimensionalBallPacking.Rigidity.packingDilation line 262
  13. theorem OAI.HigherDimensionalBallPacking.Rigidity.packingDilation_apply line 265
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.packingDilation_symm_apply line 267
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.capacity_smul_real line 270
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.standardForm_smul_real_same line 274
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.symplecticOn_dilation line 278
  18. theorem OAI.HigherDimensionalBallPacking.packing_dilation line 305
  19. theorem OAI.HigherDimensionalBallPacking.packing_reindex line 349
  20. theorem OAI.HigherDimensionalBallPacking.packing_two_of_pair line 355
  21. theorem OAI.HigherDimensionalBallPacking.two_ball_obstruction line 366
  22. theorem OAI.HigherDimensionalBallPacking.packing_pair_obstruction line 381
  23. theorem OAI.HigherDimensionalBallPacking.packing_necessity line 402

    Distinct definitions of this name: ComparatorChallenges/BallPackingNecessity.lean:38 (different declaration text). Qualify references as OAI.HigherDimensionalBallPacking.packing_necessity@path.