OAI/Probability/ThorpRouting/Contact/Coins.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Contact.Thorp.Coins line 13
  2. instance OAI.ThorpNine.Contact.Thorp.(instance at line 17) line 17
  3. instance OAI.ThorpNine.Contact.Thorp.(instance at line 20) line 20
  4. def OAI.ThorpNine.Contact.Thorp.rotate line 23
  5. def OAI.ThorpNine.Contact.Thorp.step line 29
  6. def OAI.ThorpNine.Contact.Thorp.run line 33
  7. def OAI.ThorpNine.Contact.Thorp.law line 37
  8. def OAI.ThorpNine.Contact.Thorp.distance line 41
  9. def OAI.ThorpNine.Contact.Thorp.mixingTime line 45
  10. def OAI.ThorpNine.Contact.Thorp.supportTimeBound line 48
  11. def OAI.ThorpNine.Contact.Thorp.OptimalOrder line 52
  12. def OAI.ThorpNine.Contact.Thorp.finiteLaw line 62
  13. lemma OAI.ThorpNine.Contact.Thorp.sum_card_fibers line 66
  14. lemma OAI.ThorpNine.Contact.Thorp.finiteLaw_nonneg line 72
  15. lemma OAI.ThorpNine.Contact.Thorp.finiteLaw_sum line 76
  16. lemma OAI.ThorpNine.Contact.Thorp.finiteLaw_eq_zero_of_not_mem line 85
  17. lemma OAI.ThorpNine.Contact.Thorp.event_le_totalVariation line 92
  18. lemma OAI.ThorpNine.Contact.Thorp.finiteLaw_support_bound line 106
  19. lemma OAI.ThorpNine.Contact.Thorp.card_positions line 130
  20. lemma OAI.ThorpNine.Contact.Thorp.card_permutations line 133
  21. lemma OAI.ThorpNine.Contact.Thorp.card_coins_succ line 136
  22. lemma OAI.ThorpNine.Contact.Thorp.card_tapes_succ line 139
  23. lemma OAI.ThorpNine.Contact.Thorp.law_eq_finiteLaw line 142
  24. lemma OAI.ThorpNine.Contact.Thorp.law_nonneg line 148
  25. lemma OAI.ThorpNine.Contact.Thorp.law_sum line 152
  26. lemma OAI.ThorpNine.Contact.Thorp.physical_support_bound_succ line 156
  27. lemma OAI.ThorpNine.Contact.Thorp.step_succ_formula line 163
  28. lemma OAI.ThorpNine.Contact.Thorp.distance_nonneg line 169
  29. lemma OAI.ThorpNine.Contact.Thorp.physical_support_bound line 173
  30. lemma OAI.ThorpNine.Contact.Thorp.supportTimeBound_le_of_distance_le line 189
  31. lemma OAI.ThorpNine.Contact.Thorp.supportTimeBound_le_mixingTime line 211
  32. lemma OAI.ThorpNine.Contact.Thorp.log_factorial_lower line 216
  33. lemma OAI.ThorpNine.Contact.Thorp.log_three_quarters_lower line 225
  34. lemma OAI.ThorpNine.Contact.Thorp.linear_le_supportTimeBound line 234
  35. lemma OAI.ThorpNine.Contact.Thorp.linear_le_time_of_distance_le line 260
  36. lemma OAI.ThorpNine.Contact.Thorp.entropy_chord line 267
  37. lemma OAI.ThorpNine.Contact.Thorp.split_entropy_lower line 278
  38. def OAI.ThorpNine.Contact.Thorp.childMarks line 310
  39. lemma OAI.ThorpNine.Contact.Thorp.card_childMarks line 313
  40. lemma OAI.ThorpNine.Contact.Thorp.card_childMarks_add line 323
  41. def OAI.ThorpNine.Contact.Thorp.topMeetings line 330
  42. lemma OAI.ThorpNine.Contact.Thorp.card_topMeetings_le line 335
  43. def OAI.ThorpNine.Contact.Thorp.encounters line 344
  44. lemma OAI.ThorpNine.Contact.Thorp.butterfly_encounters line 349
  45. lemma OAI.ThorpNine.Contact.Thorp.prod_split_at line 373
  46. lemma OAI.ThorpNine.Contact.Thorp.prod_split_two line 380
  47. lemma OAI.ThorpNine.Contact.Thorp.swap_average_product line 393
  48. def OAI.ThorpNine.Contact.Thorp.CylinderBound line 429
  49. lemma OAI.ThorpNine.Contact.Thorp.CylinderBound.fair_swap line 432
  50. def OAI.ThorpNine.Contact.Thorp.finiteMean line 445
  51. def OAI.ThorpNine.Contact.Thorp.inclusionMoment line 448
  52. lemma OAI.ThorpNine.Contact.Thorp.inclusionMoment_nonneg line 453
  53. lemma OAI.ThorpNine.Contact.Thorp.indicator_subset_prod line 459
  54. lemma OAI.ThorpNine.Contact.Thorp.inclusionMoment_const line 468
  55. lemma OAI.ThorpNine.Contact.Thorp.cylinder_const line 475
  56. def OAI.ThorpNine.Contact.Thorp.fairSetSwap line 483
  57. lemma OAI.ThorpNine.Contact.Thorp.subset_swap_image_iff line 487
  58. lemma OAI.ThorpNine.Contact.Thorp.inclusionMoment_fairSetSwap line 498
  59. lemma OAI.ThorpNine.Contact.Thorp.cylinder_fairSetSwap line 509
  60. def OAI.ThorpNine.Contact.Thorp.SwitchSamples line 519
  61. instance OAI.ThorpNine.Contact.Thorp.(instance at line 523) line 523
  62. instance OAI.ThorpNine.Contact.Thorp.(instance at line 528) line 528
  63. def OAI.ThorpNine.Contact.Thorp.switchedSet line 533
  64. lemma OAI.ThorpNine.Contact.Thorp.switchedSet_cylinder line 538
  65. inductive OAI.ThorpNine.Contact.Thorp.QueryTree line 546
  66. def OAI.ThorpNine.Contact.Thorp.QueryTree.queries line 556
  67. def OAI.ThorpNine.Contact.Thorp.QueryTree.Fresh line 562
  68. def OAI.ThorpNine.Contact.Thorp.QueryTree.weighted line 568
  69. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.weighted_nonneg line 575
  70. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.weighted_congr line 582
  71. def OAI.ThorpNine.Contact.Thorp.QueryTree.flipCoin line 597
  72. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.flipCoin_apply_eq line 605
  73. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.flipCoin_apply_ne line 609
  74. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.weighted_flip_of_not_mem line 614
  75. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.mean_indicator_bit line 620
  76. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.mean_weighted_le_one line 639
  77. def OAI.ThorpNine.Contact.Thorp.QueryTree.succeeds line 673
  78. def OAI.ThorpNine.Contact.Thorp.QueryTree.charge line 679
  79. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.weighted_eq line 686
  80. lemma OAI.ThorpNine.Contact.Thorp.QueryTree.success_probability_le line 699
  81. def OAI.ThorpNine.Contact.Thorp.encodeButterfly line 720
  82. lemma OAI.ThorpNine.Contact.Thorp.decode_encodeButterfly line 725
  83. lemma OAI.ThorpNine.Contact.Thorp.encode_decodeButterfly line 735
  84. def OAI.ThorpNine.Contact.Thorp.butterflyCoinEquiv line 745
  85. def OAI.ThorpNine.Contact.Thorp.routeDomain line 751
  86. def OAI.ThorpNine.Contact.Thorp.routeValue line 758