OAI/Combinatorics/HalvingLines/Batches.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.Batches.transport line 12
  2. lemma OAI.PlanarHalving.Batches.transport_of_mem line 39
  3. lemma OAI.PlanarHalving.Batches.transport_of_not_mem line 43
  4. def OAI.PlanarHalving.Batches.matching line 48
  5. lemma OAI.PlanarHalving.Batches.matching_unique line 52
  6. structure OAI.PlanarHalving.Batches.System line 63
  7. def OAI.PlanarHalving.Batches.System.loss line 73
  8. def OAI.PlanarHalving.Batches.System.gain line 75
  9. lemma OAI.PlanarHalving.Batches.System.card_loss line 78
  10. lemma OAI.PlanarHalving.Batches.System.card_gain line 80
  11. def OAI.PlanarHalving.Batches.System.lossIndex line 84
  12. def OAI.PlanarHalving.Batches.System.gainIndex line 86
  13. def OAI.PlanarHalving.Batches.System.match line 89
  14. def OAI.PlanarHalving.Batches.System.transition line 92
  15. def OAI.PlanarHalving.Batches.System.tokenState line 96
  16. lemma OAI.PlanarHalving.Batches.System.tokenState_zero line 100
  17. lemma OAI.PlanarHalving.Batches.System.tokenState_succ line 103
  18. lemma OAI.PlanarHalving.Batches.System.edge_right line 108
  19. lemma OAI.PlanarHalving.Batches.System.edge_slope line 113
  20. lemma OAI.PlanarHalving.Batches.fin_between_le line 126
  21. structure OAI.PlanarHalving.Batches.ConvexPath line 143
  22. lemma OAI.PlanarHalving.Batches.projection_step line 151
  23. lemma OAI.PlanarHalving.Batches.ConvexPath.x_mono line 160
  24. lemma OAI.PlanarHalving.Batches.ConvexPath.support_vertex line 167
  25. lemma OAI.PlanarHalving.Batches.ConvexPath.support_segment line 211
  26. lemma OAI.PlanarHalving.Batches.System.token_step line 226
  27. def OAI.PlanarHalving.Batches.System.tokenPath line 241