OAI/Probability/ThorpRouting/Adaptive/ExposedCoins.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Adaptive.Thorp.card_routeDomain line 12
  2. lemma OAI.ThorpNine.Adaptive.Thorp.xor_eq_iff line 24
  3. lemma OAI.ThorpNine.Adaptive.Thorp.butterfly_endpoint_iff line 27
  4. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_congr line 62
  5. lemma OAI.ThorpNine.Adaptive.Thorp.mean_coinCylinder line 68
  6. def OAI.ThorpNine.Adaptive.Thorp.exposedCoins line 94
  7. lemma OAI.ThorpNine.Adaptive.Thorp.mean_coinCylinder_exposed line 97
  8. lemma OAI.ThorpNine.Adaptive.Thorp.butterfly_closure_probability line 129
  9. lemma OAI.ThorpNine.Adaptive.Thorp.butterfly_single_card_uniform line 152
  10. def OAI.ThorpNine.Adaptive.Thorp.switchUsers line 162
  11. lemma OAI.ThorpNine.Adaptive.Thorp.switchUsers_ne line 171
  12. lemma OAI.ThorpNine.Adaptive.Thorp.cons_eq_iff line 186
  13. lemma OAI.ThorpNine.Adaptive.Thorp.mem_routeDomain_iff_user line 195
  14. lemma OAI.ThorpNine.Adaptive.Thorp.card_switches_using line 234
  15. lemma OAI.ThorpNine.Adaptive.Thorp.switch_incidence_sum line 245
  16. lemma OAI.ThorpNine.Adaptive.Thorp.weighted_switch_min_bound line 272
  17. lemma OAI.ThorpNine.Adaptive.Thorp.mem_childMarks line 286
  18. lemma OAI.ThorpNine.Adaptive.Thorp.mem_topMeetings line 299
  19. lemma OAI.ThorpNine.Adaptive.Thorp.encounters_eq_switch_sum line 315
  20. lemma OAI.ThorpNine.Adaptive.Thorp.marked_switch_entropy_bound line 343
  21. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.memo line 361
  22. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.memo_queries_disjoint line 372
  23. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.memo_fresh line 395
  24. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.update_agrees line 421
  25. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.memo_succeeds line 432
  26. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.freshCharge line 460
  27. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.memo_charge line 467
  28. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.mean_freshCharge_le_one line 495
  29. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.followPath line 510
  30. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.followPath_succeeds line 519
  31. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.followPath_charge line 535
  32. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.forceList line 567
  33. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.forceList_succeeds line 572
  34. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.forceList_charge line 581
  35. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.staleCharge line 611
  36. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.fresh_add_stale line 619
  37. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.followPath_raw_charge line 634
  38. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.forceList_raw_charge line 651
  39. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.closePath line 661
  40. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.closePath_succeeds line 665
  41. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.closePath_raw_charge line 673
  42. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.closePath_fresh_charge line 680
  43. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.closePath_stale_charge line 689
  44. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycle line 701
  45. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycle_raw_charge line 708
  46. def OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycles line 728
  47. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycles_raw_charge line 733
  48. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.cycles_weighted_success line 746
  49. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_add line 771
  50. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_mul_const line 775
  51. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_sum line 781
  52. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_mono line 786
  53. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_equiv line 790
  54. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_prod_left line 798
  55. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_pi_eval line 805
  56. lemma OAI.ThorpNine.Adaptive.Thorp.finiteMean_eq_indicator line 816
  57. lemma OAI.ThorpNine.Adaptive.Thorp.exp_finiteMean_le line 820
  58. def OAI.ThorpNine.Adaptive.Thorp.cycleFiber line 832
  59. lemma OAI.ThorpNine.Adaptive.Thorp.mem_cycleFiber line 836
  60. abbrev OAI.ThorpNine.Adaptive.Thorp.Terminal line 841
  61. def OAI.ThorpNine.Adaptive.Thorp.slotWeight line 843
  62. def OAI.ThorpNine.Adaptive.Thorp.pathWeight line 846
  63. def OAI.ThorpNine.Adaptive.Thorp.withinWeight line 851