OAI/Geometry/BallPacking/Packings/ComplementPacking.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.actual_complement_packing line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_shifted_planar_embedding line 61
  3. def OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap line 94
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient_split_capacity line 97
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.headComplexAmbient_head_le line 101
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_capacity line 108
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_first line 113
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_smoothAt line 119
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_fderiv line 126
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_injOn line 139
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.headPlanarMap_form line 149
  12. theorem OAI.PackingSufficiencySupport.exists_distinguished_ball_embedding line 167
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_actual_normal_transfer line 215
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.actual_small_polynomial_packing line 292
  15. theorem OAI.PackingSufficiencySupport.hasPacking_small_enlarged line 341
  16. theorem OAI.PackingSufficiencySupport.hasPacking_small_normalized line 369
  17. theorem OAI.PackingSufficiencySupport.hasPacking_small line 380
  18. theorem OAI.PackingSufficiencySupport.hasPacking_large_enlarged line 393
  19. theorem OAI.PackingSufficiencySupport.HasPacking.reindex line 447
  20. theorem OAI.PackingSufficiencySupport.hasPacking_large_normalized line 454
  21. theorem OAI.PackingSufficiencySupport.hasPacking_dim_ge_four_normalized line 462
  22. theorem OAI.PackingSufficiencySupport.hasPacking_dim_ge_four line 496
  23. theorem OAI.PackingSufficiencySupport.hasPacking_six_large_normalized line 507
  24. theorem OAI.PackingSufficiencySupport.hasPacking_six_normalized line 537
  25. theorem OAI.PackingSufficiencySupport.hasPacking_of_inequalities line 566
  26. theorem OAI.HigherDimensionalBallPacking.HasPacking.subfamily line 588
  27. theorem OAI.HigherDimensionalBallPacking.HasPacking.two_balls line 595
  28. theorem OAI.HigherDimensionalBallPacking.HasPacking.two_balls_smaller_target line 610
  29. theorem OAI.HigherDimensionalBallPacking.HasPacking.unit_pair_counterexample line 616
  30. theorem OAI.HigherDimensionalBallPacking.hasPacking_of_inequalities_dim_ge_four line 632
  31. theorem OAI.HigherDimensionalBallPacking.hasPacking_all_small line 638
  32. theorem OAI.HigherDimensionalBallPacking.hasPacking_of_inequalities line 644
  33. theorem OAI.HigherDimensionalBallPacking.one_ball_main line 650