OAI/Probability/ThorpRouting/Harmonic/Coins.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Harmonic.Thorp.Coins line 13

    Also declared: ComparatorChallenges/CoordinateTrace.lean:31 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:120 (same declaration text).

  2. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 17) line 17
  3. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 20) line 20
  4. def OAI.ThorpNine.Harmonic.Thorp.rotate line 23

    Also declared: ComparatorChallenges/CoordinateTrace.lean:41 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:130 (same declaration text).

  5. def OAI.ThorpNine.Harmonic.Thorp.step line 29

    Also declared: ComparatorChallenges/CoordinateTrace.lean:47 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:136 (same declaration text).

  6. def OAI.ThorpNine.Harmonic.Thorp.run line 33

    Also declared: ComparatorChallenges/CoordinateTrace.lean:51 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:140 (same declaration text).

  7. def OAI.ThorpNine.Harmonic.Thorp.law line 37

    Also declared: ComparatorChallenges/CoordinateTrace.lean:55 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:144 (same declaration text).

  8. def OAI.ThorpNine.Harmonic.Thorp.distance line 41
  9. def OAI.ThorpNine.Harmonic.Thorp.mixingTime line 45
  10. def OAI.ThorpNine.Harmonic.Thorp.supportTimeBound line 48
  11. def OAI.ThorpNine.Harmonic.Thorp.OptimalOrder line 52
  12. def OAI.ThorpNine.Harmonic.Thorp.finiteLaw line 62
  13. lemma OAI.ThorpNine.Harmonic.Thorp.sum_card_fibers line 66
  14. lemma OAI.ThorpNine.Harmonic.Thorp.finiteLaw_nonneg line 72
  15. lemma OAI.ThorpNine.Harmonic.Thorp.finiteLaw_sum line 76
  16. lemma OAI.ThorpNine.Harmonic.Thorp.finiteLaw_eq_zero_of_not_mem line 85
  17. lemma OAI.ThorpNine.Harmonic.Thorp.event_le_totalVariation line 92
  18. lemma OAI.ThorpNine.Harmonic.Thorp.finiteLaw_support_bound line 106
  19. lemma OAI.ThorpNine.Harmonic.Thorp.card_positions line 130

    Also declared: ComparatorChallenges/CoordinateTrace.lean:59 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:148 (same declaration text).

  20. lemma OAI.ThorpNine.Harmonic.Thorp.card_permutations line 133
  21. lemma OAI.ThorpNine.Harmonic.Thorp.card_coins_succ line 136
  22. lemma OAI.ThorpNine.Harmonic.Thorp.card_tapes_succ line 139
  23. lemma OAI.ThorpNine.Harmonic.Thorp.law_eq_finiteLaw line 142
  24. lemma OAI.ThorpNine.Harmonic.Thorp.law_nonneg line 148
  25. lemma OAI.ThorpNine.Harmonic.Thorp.law_sum line 152
  26. lemma OAI.ThorpNine.Harmonic.Thorp.physical_support_bound_succ line 156
  27. lemma OAI.ThorpNine.Harmonic.Thorp.step_succ_formula line 163
  28. lemma OAI.ThorpNine.Harmonic.Thorp.distance_nonneg line 169
  29. lemma OAI.ThorpNine.Harmonic.Thorp.physical_support_bound line 173
  30. lemma OAI.ThorpNine.Harmonic.Thorp.supportTimeBound_le_of_distance_le line 189
  31. lemma OAI.ThorpNine.Harmonic.Thorp.supportTimeBound_le_mixingTime line 211
  32. lemma OAI.ThorpNine.Harmonic.Thorp.log_factorial_lower line 216
  33. lemma OAI.ThorpNine.Harmonic.Thorp.log_three_quarters_lower line 225
  34. lemma OAI.ThorpNine.Harmonic.Thorp.linear_le_supportTimeBound line 234
  35. lemma OAI.ThorpNine.Harmonic.Thorp.linear_le_time_of_distance_le line 260
  36. lemma OAI.ThorpNine.Harmonic.Thorp.entropy_chord line 267
  37. lemma OAI.ThorpNine.Harmonic.Thorp.split_entropy_lower line 278
  38. def OAI.ThorpNine.Harmonic.Thorp.childMarks line 310
  39. lemma OAI.ThorpNine.Harmonic.Thorp.card_childMarks line 313
  40. lemma OAI.ThorpNine.Harmonic.Thorp.card_childMarks_add line 323
  41. def OAI.ThorpNine.Harmonic.Thorp.topMeetings line 330
  42. lemma OAI.ThorpNine.Harmonic.Thorp.card_topMeetings_le line 335
  43. def OAI.ThorpNine.Harmonic.Thorp.encounters line 344
  44. lemma OAI.ThorpNine.Harmonic.Thorp.butterfly_encounters line 349
  45. lemma OAI.ThorpNine.Harmonic.Thorp.prod_split_at line 373
  46. lemma OAI.ThorpNine.Harmonic.Thorp.prod_split_two line 380
  47. lemma OAI.ThorpNine.Harmonic.Thorp.swap_average_product line 393
  48. def OAI.ThorpNine.Harmonic.Thorp.CylinderBound line 429
  49. lemma OAI.ThorpNine.Harmonic.Thorp.CylinderBound.fair_swap line 432
  50. def OAI.ThorpNine.Harmonic.Thorp.inclusionMoment line 445
  51. lemma OAI.ThorpNine.Harmonic.Thorp.inclusionMoment_nonneg line 450
  52. lemma OAI.ThorpNine.Harmonic.Thorp.indicator_subset_prod line 456
  53. lemma OAI.ThorpNine.Harmonic.Thorp.inclusionMoment_const line 465
  54. lemma OAI.ThorpNine.Harmonic.Thorp.cylinder_const line 472
  55. def OAI.ThorpNine.Harmonic.Thorp.fairSetSwap line 480
  56. lemma OAI.ThorpNine.Harmonic.Thorp.subset_swap_image_iff line 484
  57. lemma OAI.ThorpNine.Harmonic.Thorp.inclusionMoment_fairSetSwap line 495
  58. lemma OAI.ThorpNine.Harmonic.Thorp.cylinder_fairSetSwap line 506
  59. def OAI.ThorpNine.Harmonic.Thorp.SwitchSamples line 516
  60. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 520) line 520
  61. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 525) line 525
  62. def OAI.ThorpNine.Harmonic.Thorp.switchedSet line 530
  63. lemma OAI.ThorpNine.Harmonic.Thorp.switchedSet_cylinder line 535
  64. inductive OAI.ThorpNine.Harmonic.Thorp.QueryTree line 543
  65. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.queries line 553
  66. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.Fresh line 559
  67. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.weighted line 565
  68. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.weighted_nonneg line 572
  69. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.weighted_congr line 579
  70. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.flipCoin line 594
  71. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.flipCoin_apply_eq line 602
  72. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.flipCoin_apply_ne line 606
  73. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.weighted_flip_of_not_mem line 611
  74. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.mean_indicator_bit line 617
  75. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.mean_weighted_le_one line 636
  76. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.succeeds line 670
  77. def OAI.ThorpNine.Harmonic.Thorp.QueryTree.charge line 676
  78. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.weighted_eq line 683
  79. lemma OAI.ThorpNine.Harmonic.Thorp.QueryTree.success_probability_le line 696
  80. def OAI.ThorpNine.Harmonic.Thorp.encodeButterfly line 717
  81. lemma OAI.ThorpNine.Harmonic.Thorp.decode_encodeButterfly line 722
  82. lemma OAI.ThorpNine.Harmonic.Thorp.encode_decodeButterfly line 732
  83. def OAI.ThorpNine.Harmonic.Thorp.butterflyCoinEquiv line 742
  84. def OAI.ThorpNine.Harmonic.Thorp.routeDomain line 748
  85. def OAI.ThorpNine.Harmonic.Thorp.routeValue line 755