OAI/Combinatorics/HalvingLines/Packing.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.RankLimits.commonDirection line 11
  2. lemma OAI.PlanarHalving.RankLimits.commonDirection_independent line 13
  3. lemma OAI.PlanarHalving.RankLimits.common_frame line 17
  4. def OAI.PlanarHalving.RankLimits.commonChart line 53
  5. lemma OAI.PlanarHalving.RankLimits.commonChart_symm line 58
  6. lemma OAI.PlanarHalving.RankLimits.commonChart_source line 62
  7. lemma OAI.PlanarHalving.RankLimits.commonChart_target line 67
  8. lemma OAI.PlanarHalving.RankLimits.Converges.radial_ae line 78
  9. lemma OAI.PlanarHalving.RankLimits.normalized_commonChart line 124
  10. lemma OAI.PlanarHalving.RankLimits.enhancement_points_ae line 131
  11. lemma OAI.PlanarHalving.RankLimits.normalized_points_graph line 139
  12. lemma OAI.PlanarHalving.RankLimits.support_graph_subseq line 155
  13. lemma OAI.PlanarHalving.RankLimits.Converges.spatial_impossible line 171
  14. lemma OAI.PlanarHalving.RankLimits.common_finite_eventually line 225
  15. lemma OAI.PlanarHalving.RankLimits.joint_shift line 237
  16. lemma OAI.PlanarHalving.RankLimits.Converges.analytic_ready line 243
  17. lemma OAI.PlanarHalving.RankLimits.Converges.impossible line 275
  18. lemma OAI.PlanarHalving.RankLimits.normalized_sequence_impossible line 316
  19. theorem OAI.PlanarHalving.RankLimits.uniform_batch_saving line 329
  20. def OAI.PlanarHalving.Sweep.greedyConfiguration line 348
  21. def OAI.PlanarHalving.Sweep.greedyConfiguration_embedding line 362
  22. lemma OAI.PlanarHalving.Sweep.distance_saving line 371
  23. theorem OAI.PlanarHalving.Sweep.activity_saving_cubic line 412