OAI/Probability/ThorpRouting/Casimir/AssignmentSlots.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.assignmentOwner_eq_some line 14
  2. lemma OAI.ThorpNine.Casimir.Thorp.assignmentOwner_fiber line 32
  3. def OAI.ThorpNine.Casimir.Thorp.assignmentToSlots line 37
  4. def OAI.ThorpNine.Casimir.Thorp.cycleSlotsEquivAssignments line 51
  5. abbrev OAI.ThorpNine.Casimir.Thorp.LengthClass line 72
  6. def OAI.ThorpNine.Casimir.Thorp.slotClass line 74
  7. abbrev OAI.ThorpNine.Casimir.Thorp.SlotsOfLength line 77
  8. abbrev OAI.ThorpNine.Casimir.Thorp.CyclesOfLength line 78
  9. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 81) line 81
  10. abbrev OAI.ThorpNine.Casimir.Thorp.GroupedAssignments line 84
  11. def OAI.ThorpNine.Casimir.Thorp.assignmentToGroups line 87
  12. def OAI.ThorpNine.Casimir.Thorp.groupsEmbedding line 92
  13. def OAI.ThorpNine.Casimir.Thorp.groupsToAssignment line 99
  14. def OAI.ThorpNine.Casimir.Thorp.assignmentEquivGroups line 104
  15. lemma OAI.ThorpNine.Casimir.Thorp.card_cycleSlots_factorial line 119
  16. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_factorial_moment line 128
  17. def OAI.ThorpNine.Casimir.Thorp.assignmentRelabel line 142
  18. lemma OAI.ThorpNine.Casimir.Thorp.card_cycleSlots_relabel line 151
  19. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_cycleSlots_moment_all line 157
  20. abbrev OAI.ThorpNine.Casimir.Thorp.ShortCycle line 167
  21. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 170) line 170
  22. def OAI.ThorpNine.Casimir.Thorp.shortCycleLength line 173
  23. lemma OAI.ThorpNine.Casimir.Thorp.shortCycleLength_add_one line 177
  24. def OAI.ThorpNine.Casimir.Thorp.shortEmbeddingEquiv line 183
  25. lemma OAI.ThorpNine.Casimir.Thorp.shortCycle_factorial_eq line 209
  26. lemma OAI.ThorpNine.Casimir.Thorp.factorial_mgf line 222
  27. lemma OAI.ThorpNine.Casimir.Thorp.inv_sqrt_step line 259
  28. lemma OAI.ThorpNine.Casimir.Thorp.sum_inv_sqrt line 267
  29. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_shortCycle_moment line 282
  30. def OAI.ThorpNine.Casimir.Thorp.cycleMass line 301
  31. lemma OAI.ThorpNine.Casimir.Thorp.cycleMass_le line 304
  32. lemma OAI.ThorpNine.Casimir.Thorp.shortCycle_card_le line 322
  33. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_shortCycle_mgf line 331
  34. abbrev OAI.ThorpNine.Casimir.Thorp.LongCycle line 345
  35. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 347) line 347
  36. lemma OAI.ThorpNine.Casimir.Thorp.selectedCycle_card_split line 350
  37. lemma OAI.ThorpNine.Casimir.Thorp.longCycle_card_bound line 356
  38. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_pos line 372
  39. lemma OAI.ThorpNine.Casimir.Thorp.longCycle_pow_bound line 378
  40. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_cycle_log_mgf line 391
  41. structure OAI.ThorpNine.Casimir.Thorp.RoutingNetwork line 438
  42. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.card_switches_using line 465
  43. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.switch_incidence_sum line 474
  44. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.weighted_switch_min_bound line 501
  45. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.cycleFiber line 517
  46. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.mem_cycleFiber line 522
  47. abbrev OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.Terminal line 527
  48. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.slotWeight line 529
  49. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.pathWeight line 532
  50. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.withinWeight line 537
  51. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.rotationMeeting line 542
  52. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.card_cycleFiber line 551
  53. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.terminal_mean line 556
  54. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.slotWeight_antitone line 571
  55. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.rotationMeeting_mean line 580
  56. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.pathWeight_sum line 614
  57. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.withinWeight_sum_bound line 631
  58. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.rotationCharge line 653
  59. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.rotationCharge_mean_bound line 657
  60. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.rotation_exp_bound line 675
  61. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycle line 697
  62. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycle_raw_charge line 704
  63. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycles line 724
  64. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycles_raw_charge line 729
  65. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.cycles_weighted_success line 742
  66. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.exposedPaths line 766
  67. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.exposedPaths_empty line 770
  68. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.exposedPaths_insert line 774
  69. def OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.terminalCharge line 779
  70. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycle_semantics line 785
  71. lemma OAI.ThorpNine.Casimir.Thorp.RoutingNetwork.QueryTree.seekCycle_orbit line 814