OAI/Probability/ThorpRouting/Smoothing/RotationCharge.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Smoothing.Thorp.card_cycleFiber line 14
  2. lemma OAI.ThorpNine.Smoothing.Thorp.terminal_mean line 19
  3. lemma OAI.ThorpNine.Smoothing.Thorp.slotWeight_antitone line 33
  4. lemma OAI.ThorpNine.Smoothing.Thorp.rotationMeeting_mean line 42
  5. lemma OAI.ThorpNine.Smoothing.Thorp.pathWeight_sum line 75
  6. lemma OAI.ThorpNine.Smoothing.Thorp.withinWeight_sum_bound line 92
  7. def OAI.ThorpNine.Smoothing.Thorp.rotationCharge line 114
  8. lemma OAI.ThorpNine.Smoothing.Thorp.rotationCharge_mean_bound line 118
  9. lemma OAI.ThorpNine.Smoothing.Thorp.rotation_exp_bound line 136
  10. def OAI.ThorpNine.Smoothing.Thorp.orbitSet line 158
  11. lemma OAI.ThorpNine.Smoothing.Thorp.mem_orbitSet line 161
  12. lemma OAI.ThorpNine.Smoothing.Thorp.orbitSet_nonempty line 166
  13. lemma OAI.ThorpNine.Smoothing.Thorp.orbitSet_eq line 169
  14. lemma OAI.ThorpNine.Smoothing.Thorp.orbitSet_apply line 175
  15. lemma OAI.ThorpNine.Smoothing.Thorp.orbitSet_eq_or_disjoint line 179
  16. lemma OAI.ThorpNine.Smoothing.Thorp.perm_minimalPeriod_pos line 190
  17. lemma OAI.ThorpNine.Smoothing.Thorp.orbitSet_card line 194
  18. def OAI.ThorpNine.Smoothing.Thorp.walkSet line 213
  19. lemma OAI.ThorpNine.Smoothing.Thorp.mem_walkSet line 217
  20. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_zero line 222
  21. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_succ_last line 226
  22. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_succ_first line 231
  23. lemma OAI.ThorpNine.Smoothing.Thorp.not_mem_short_walk line 245
  24. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_period line 254
  25. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_card line 268
  26. lemma OAI.ThorpNine.Smoothing.Thorp.walkSet_subset_orbit line 277
  27. def OAI.ThorpNine.Smoothing.Thorp.cycleTrace line 284
  28. lemma OAI.ThorpNine.Smoothing.Thorp.cycleTrace_walk line 289
  29. lemma OAI.ThorpNine.Smoothing.Thorp.cycleTrace_orbit line 323
  30. def OAI.ThorpNine.Smoothing.Thorp.exposedPaths line 345
  31. lemma OAI.ThorpNine.Smoothing.Thorp.exposedPaths_empty line 349
  32. lemma OAI.ThorpNine.Smoothing.Thorp.exposedPaths_insert line 353
  33. def OAI.ThorpNine.Smoothing.Thorp.terminalCharge line 358
  34. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.followPath_stale_charge line 363
  35. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycle_semantics line 375
  36. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycle_orbit line 405
  37. lemma OAI.ThorpNine.Smoothing.Thorp.mem_exposedPaths line 420
  38. lemma OAI.ThorpNine.Smoothing.Thorp.terminalCharge_sum line 432
  39. def OAI.ThorpNine.Smoothing.Thorp.priorPaths line 454
  40. lemma OAI.ThorpNine.Smoothing.Thorp.mem_priorPaths line 457
  41. lemma OAI.ThorpNine.Smoothing.Thorp.terminalCharge_prior_sum line 462
  42. lemma OAI.ThorpNine.Smoothing.Thorp.rotationMeeting_eq_slot_sum line 479
  43. lemma OAI.ThorpNine.Smoothing.Thorp.rotationCharge_eq_terminal_sum line 531
  44. lemma OAI.ThorpNine.Smoothing.Thorp.priorPaths_zero line 538
  45. lemma OAI.ThorpNine.Smoothing.Thorp.priorPaths_succ line 543
  46. lemma OAI.ThorpNine.Smoothing.Thorp.priorPaths_disjoint line 558
  47. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycles_owned line 570
  48. def OAI.ThorpNine.Smoothing.Thorp.ValidCycleSlots line 619
  49. abbrev OAI.ThorpNine.Smoothing.Thorp.CycleSlots line 625
  50. instance OAI.ThorpNine.Smoothing.Thorp.(instance at line 628) line 628
  51. lemma OAI.ThorpNine.Smoothing.Thorp.CycleSlots.terminal_nonempty line 631
  52. lemma OAI.ThorpNine.Smoothing.Thorp.owner_ext line 637
  53. abbrev OAI.ThorpNine.Smoothing.Thorp.RootedSlots line 649
  54. def OAI.ThorpNine.Smoothing.Thorp.rootedStart line 652
  55. lemma OAI.ThorpNine.Smoothing.Thorp.rootedStart_injective line 658
  56. lemma OAI.ThorpNine.Smoothing.Thorp.sum_comp_injective_le line 671
  57. lemma OAI.ThorpNine.Smoothing.Thorp.rooted_weight_sum_le line 679
  58. def OAI.ThorpNine.Smoothing.Thorp.rotationLower line 705
  59. def OAI.ThorpNine.Smoothing.Thorp.collectionWeight line 708
  60. lemma OAI.ThorpNine.Smoothing.Thorp.collectionWeight_pos line 711
  61. lemma OAI.ThorpNine.Smoothing.Thorp.collection_rotation_lower line 715
  62. lemma OAI.ThorpNine.Smoothing.Thorp.cycleSlots_weighted_moment line 743
  63. lemma OAI.ThorpNine.Smoothing.Thorp.cycleSlots_moment line 776
  64. lemma OAI.ThorpNine.Smoothing.Thorp.collectionWeight_eq_sqrt line 782
  65. lemma OAI.ThorpNine.Smoothing.Thorp.butterfly_cycleSlots_moment line 807
  66. abbrev OAI.ThorpNine.Smoothing.Thorp.SelectedCycle line 821
  67. instance OAI.ThorpNine.Smoothing.Thorp.(instance at line 824) line 824
  68. lemma OAI.ThorpNine.Smoothing.Thorp.SelectedCycle.nonempty line 827
  69. lemma OAI.ThorpNine.Smoothing.Thorp.SelectedCycle.orbit_eq line 833
  70. lemma OAI.ThorpNine.Smoothing.Thorp.SelectedCycle.eq_of_mem line 839
  71. abbrev OAI.ThorpNine.Smoothing.Thorp.SlotAssignment line 844
  72. instance OAI.ThorpNine.Smoothing.Thorp.(instance at line 847) line 847
  73. def OAI.ThorpNine.Smoothing.Thorp.slotsToAssignment line 850
  74. def OAI.ThorpNine.Smoothing.Thorp.assignmentOwner line 864
  75. lemma OAI.ThorpNine.Smoothing.Thorp.assignmentOwner_eq_some line 869