OAI/Probability/ThorpRouting/Dense/AssignmentSlots.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.assignmentOwner_fiber line 14
  2. def OAI.ThorpNine.Dense.Thorp.assignmentToSlots line 19
  3. def OAI.ThorpNine.Dense.Thorp.cycleSlotsEquivAssignments line 33
  4. abbrev OAI.ThorpNine.Dense.Thorp.LengthClass line 54
  5. def OAI.ThorpNine.Dense.Thorp.slotClass line 56
  6. abbrev OAI.ThorpNine.Dense.Thorp.SlotsOfLength line 59
  7. abbrev OAI.ThorpNine.Dense.Thorp.CyclesOfLength line 60
  8. instance OAI.ThorpNine.Dense.Thorp.(instance at line 63) line 63
  9. abbrev OAI.ThorpNine.Dense.Thorp.GroupedAssignments line 66
  10. def OAI.ThorpNine.Dense.Thorp.assignmentToGroups line 69
  11. def OAI.ThorpNine.Dense.Thorp.groupsEmbedding line 74
  12. def OAI.ThorpNine.Dense.Thorp.groupsToAssignment line 81
  13. def OAI.ThorpNine.Dense.Thorp.assignmentEquivGroups line 86
  14. lemma OAI.ThorpNine.Dense.Thorp.card_cycleSlots_factorial line 101
  15. lemma OAI.ThorpNine.Dense.Thorp.butterfly_factorial_moment line 110
  16. def OAI.ThorpNine.Dense.Thorp.assignmentRelabel line 124
  17. lemma OAI.ThorpNine.Dense.Thorp.card_cycleSlots_relabel line 133
  18. lemma OAI.ThorpNine.Dense.Thorp.butterfly_cycleSlots_moment_all line 139
  19. abbrev OAI.ThorpNine.Dense.Thorp.ShortCycle line 149
  20. instance OAI.ThorpNine.Dense.Thorp.(instance at line 152) line 152
  21. def OAI.ThorpNine.Dense.Thorp.shortCycleLength line 155
  22. lemma OAI.ThorpNine.Dense.Thorp.shortCycleLength_add_one line 159
  23. def OAI.ThorpNine.Dense.Thorp.shortEmbeddingEquiv line 165
  24. lemma OAI.ThorpNine.Dense.Thorp.shortCycle_factorial_eq line 191
  25. lemma OAI.ThorpNine.Dense.Thorp.factorial_mgf line 204
  26. lemma OAI.ThorpNine.Dense.Thorp.inv_sqrt_step line 241
  27. lemma OAI.ThorpNine.Dense.Thorp.sum_inv_sqrt line 249
  28. lemma OAI.ThorpNine.Dense.Thorp.butterfly_shortCycle_moment line 264
  29. def OAI.ThorpNine.Dense.Thorp.cycleMass line 283
  30. lemma OAI.ThorpNine.Dense.Thorp.cycleMass_le line 286
  31. lemma OAI.ThorpNine.Dense.Thorp.shortCycle_card_le line 304
  32. lemma OAI.ThorpNine.Dense.Thorp.butterfly_shortCycle_mgf line 313
  33. abbrev OAI.ThorpNine.Dense.Thorp.LongCycle line 327
  34. instance OAI.ThorpNine.Dense.Thorp.(instance at line 329) line 329
  35. lemma OAI.ThorpNine.Dense.Thorp.selectedCycle_card_split line 332
  36. lemma OAI.ThorpNine.Dense.Thorp.longCycle_card_bound line 338
  37. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_pos line 354
  38. lemma OAI.ThorpNine.Dense.Thorp.longCycle_pow_bound line 360
  39. lemma OAI.ThorpNine.Dense.Thorp.butterfly_cycle_log_mgf line 373
  40. structure OAI.ThorpNine.Dense.Thorp.RoutingNetwork line 420
  41. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.card_switches_using line 447
  42. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.switch_incidence_sum line 456
  43. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.weighted_switch_min_bound line 483
  44. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.cycleFiber line 499
  45. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.mem_cycleFiber line 504
  46. abbrev OAI.ThorpNine.Dense.Thorp.RoutingNetwork.Terminal line 509
  47. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.slotWeight line 511
  48. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.pathWeight line 514
  49. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.withinWeight line 519
  50. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.rotationMeeting line 524
  51. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.card_cycleFiber line 533
  52. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.terminal_mean line 538
  53. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.slotWeight_antitone line 553
  54. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.rotationMeeting_mean line 562
  55. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.pathWeight_sum line 596
  56. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.withinWeight_sum_bound line 613
  57. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.rotationCharge line 635
  58. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.rotationCharge_mean_bound line 639
  59. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.rotation_exp_bound line 657
  60. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycle line 679
  61. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycle_raw_charge line 686
  62. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycles line 706
  63. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycles_raw_charge line 711
  64. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.cycles_weighted_success line 724
  65. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.exposedPaths line 748
  66. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.exposedPaths_empty line 752
  67. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.exposedPaths_insert line 756
  68. def OAI.ThorpNine.Dense.Thorp.RoutingNetwork.terminalCharge line 761
  69. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycle_semantics line 767
  70. lemma OAI.ThorpNine.Dense.Thorp.RoutingNetwork.QueryTree.seekCycle_orbit line 796