OAI/Probability/ThorpRouting/Smoothing/ExposedCoins.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Smoothing.Thorp.xor_eq_iff line 12
  2. lemma OAI.ThorpNine.Smoothing.Thorp.butterfly_endpoint_iff line 15
  3. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_congr line 50
  4. lemma OAI.ThorpNine.Smoothing.Thorp.mean_coinCylinder line 56
  5. def OAI.ThorpNine.Smoothing.Thorp.exposedCoins line 82
  6. lemma OAI.ThorpNine.Smoothing.Thorp.mean_coinCylinder_exposed line 85
  7. lemma OAI.ThorpNine.Smoothing.Thorp.butterfly_closure_probability line 117
  8. lemma OAI.ThorpNine.Smoothing.Thorp.butterfly_single_card_uniform line 140
  9. def OAI.ThorpNine.Smoothing.Thorp.switchUsers line 150
  10. lemma OAI.ThorpNine.Smoothing.Thorp.switchUsers_ne line 159
  11. lemma OAI.ThorpNine.Smoothing.Thorp.cons_eq_iff line 174
  12. lemma OAI.ThorpNine.Smoothing.Thorp.mem_routeDomain_iff_user line 183
  13. lemma OAI.ThorpNine.Smoothing.Thorp.card_switches_using line 222
  14. lemma OAI.ThorpNine.Smoothing.Thorp.switch_incidence_sum line 233
  15. lemma OAI.ThorpNine.Smoothing.Thorp.weighted_switch_min_bound line 260
  16. lemma OAI.ThorpNine.Smoothing.Thorp.mem_childMarks line 274
  17. lemma OAI.ThorpNine.Smoothing.Thorp.mem_topMeetings line 287
  18. lemma OAI.ThorpNine.Smoothing.Thorp.encounters_eq_switch_sum line 303
  19. lemma OAI.ThorpNine.Smoothing.Thorp.marked_switch_entropy_bound line 331
  20. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.memo line 349
  21. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.memo_queries_disjoint line 360
  22. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.memo_fresh line 383
  23. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.update_agrees line 409
  24. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.memo_succeeds line 420
  25. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.freshCharge line 448
  26. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.memo_charge line 455
  27. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.mean_freshCharge_le_one line 483
  28. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.followPath line 498
  29. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.followPath_succeeds line 507
  30. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.followPath_charge line 523
  31. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.forceList line 555
  32. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.forceList_succeeds line 560
  33. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.forceList_charge line 569
  34. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.staleCharge line 599
  35. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.fresh_add_stale line 607
  36. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.followPath_raw_charge line 622
  37. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.forceList_raw_charge line 639
  38. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.closePath line 649
  39. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.closePath_succeeds line 653
  40. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.closePath_raw_charge line 661
  41. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.closePath_fresh_charge line 668
  42. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.closePath_stale_charge line 677
  43. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycle line 689
  44. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycle_raw_charge line 696
  45. def OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycles line 716
  46. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.seekCycles_raw_charge line 721
  47. lemma OAI.ThorpNine.Smoothing.Thorp.QueryTree.cycles_weighted_success line 734
  48. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_add line 759
  49. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_mul_const line 763
  50. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_sum line 769
  51. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_mono line 774
  52. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_equiv line 778
  53. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_prod_left line 786
  54. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_pi_eval line 793
  55. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_eq_indicator line 804
  56. lemma OAI.ThorpNine.Smoothing.Thorp.exp_finiteMean_le line 808
  57. def OAI.ThorpNine.Smoothing.Thorp.cycleFiber line 820
  58. lemma OAI.ThorpNine.Smoothing.Thorp.mem_cycleFiber line 824
  59. abbrev OAI.ThorpNine.Smoothing.Thorp.Terminal line 829
  60. def OAI.ThorpNine.Smoothing.Thorp.slotWeight line 831
  61. def OAI.ThorpNine.Smoothing.Thorp.pathWeight line 834
  62. def OAI.ThorpNine.Smoothing.Thorp.withinWeight line 839
  63. def OAI.ThorpNine.Smoothing.Thorp.rotationMeeting line 844