OAI/Probability/ThorpRouting/Casimir/Distance.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 13) line 13
  2. def OAI.ThorpNine.Casimir.Thorp.distance line 16
  3. def OAI.ThorpNine.Casimir.Thorp.mixingTime line 20
  4. def OAI.ThorpNine.Casimir.Thorp.supportTimeBound line 23
  5. def OAI.ThorpNine.Casimir.Thorp.OptimalOrder line 27
  6. def OAI.ThorpNine.Casimir.Thorp.finiteLaw line 37
  7. lemma OAI.ThorpNine.Casimir.Thorp.sum_card_fibers line 41
  8. lemma OAI.ThorpNine.Casimir.Thorp.finiteLaw_nonneg line 47
  9. lemma OAI.ThorpNine.Casimir.Thorp.finiteLaw_sum line 51
  10. lemma OAI.ThorpNine.Casimir.Thorp.finiteLaw_eq_zero_of_not_mem line 60
  11. lemma OAI.ThorpNine.Casimir.Thorp.event_le_totalVariation line 67
  12. lemma OAI.ThorpNine.Casimir.Thorp.finiteLaw_support_bound line 81
  13. lemma OAI.ThorpNine.Casimir.Thorp.card_positions line 105
  14. lemma OAI.ThorpNine.Casimir.Thorp.card_permutations line 108
  15. lemma OAI.ThorpNine.Casimir.Thorp.card_coins_succ line 111
  16. lemma OAI.ThorpNine.Casimir.Thorp.card_tapes_succ line 114
  17. lemma OAI.ThorpNine.Casimir.Thorp.law_eq_finiteLaw line 117
  18. lemma OAI.ThorpNine.Casimir.Thorp.law_nonneg line 123
  19. lemma OAI.ThorpNine.Casimir.Thorp.law_sum line 127
  20. lemma OAI.ThorpNine.Casimir.Thorp.physical_support_bound_succ line 131
  21. lemma OAI.ThorpNine.Casimir.Thorp.step_succ_formula line 138
  22. lemma OAI.ThorpNine.Casimir.Thorp.distance_nonneg line 144
  23. lemma OAI.ThorpNine.Casimir.Thorp.physical_support_bound line 148
  24. lemma OAI.ThorpNine.Casimir.Thorp.supportTimeBound_le_of_distance_le line 164
  25. lemma OAI.ThorpNine.Casimir.Thorp.supportTimeBound_le_mixingTime line 186
  26. lemma OAI.ThorpNine.Casimir.Thorp.log_factorial_lower line 191
  27. lemma OAI.ThorpNine.Casimir.Thorp.log_three_quarters_lower line 200
  28. lemma OAI.ThorpNine.Casimir.Thorp.linear_le_supportTimeBound line 209
  29. lemma OAI.ThorpNine.Casimir.Thorp.linear_le_time_of_distance_le line 235
  30. lemma OAI.ThorpNine.Casimir.Thorp.entropy_chord line 242
  31. lemma OAI.ThorpNine.Casimir.Thorp.split_entropy_lower line 253
  32. def OAI.ThorpNine.Casimir.Thorp.childMarks line 285
  33. lemma OAI.ThorpNine.Casimir.Thorp.card_childMarks line 288
  34. lemma OAI.ThorpNine.Casimir.Thorp.card_childMarks_add line 298
  35. def OAI.ThorpNine.Casimir.Thorp.topMeetings line 305
  36. lemma OAI.ThorpNine.Casimir.Thorp.card_topMeetings_le line 310
  37. def OAI.ThorpNine.Casimir.Thorp.encounters line 319
  38. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_encounters line 324
  39. lemma OAI.ThorpNine.Casimir.Thorp.prod_split_at line 348
  40. lemma OAI.ThorpNine.Casimir.Thorp.prod_split_two line 355
  41. lemma OAI.ThorpNine.Casimir.Thorp.swap_average_product line 368
  42. def OAI.ThorpNine.Casimir.Thorp.CylinderBound line 404
  43. lemma OAI.ThorpNine.Casimir.Thorp.CylinderBound.fair_swap line 407
  44. def OAI.ThorpNine.Casimir.Thorp.inclusionMoment line 420
  45. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_nonneg line 425
  46. lemma OAI.ThorpNine.Casimir.Thorp.indicator_subset_prod line 431
  47. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_const line 440
  48. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_const line 447
  49. def OAI.ThorpNine.Casimir.Thorp.fairSetSwap line 455
  50. lemma OAI.ThorpNine.Casimir.Thorp.subset_swap_image_iff line 459
  51. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_fairSetSwap line 470
  52. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_fairSetSwap line 481
  53. def OAI.ThorpNine.Casimir.Thorp.SwitchSamples line 491
  54. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 495) line 495
  55. instance OAI.ThorpNine.Casimir.Thorp.(instance at line 500) line 500
  56. def OAI.ThorpNine.Casimir.Thorp.switchedSet line 505
  57. lemma OAI.ThorpNine.Casimir.Thorp.switchedSet_cylinder line 510
  58. inductive OAI.ThorpNine.Casimir.Thorp.QueryTree line 518
  59. def OAI.ThorpNine.Casimir.Thorp.QueryTree.queries line 528
  60. def OAI.ThorpNine.Casimir.Thorp.QueryTree.Fresh line 534
  61. def OAI.ThorpNine.Casimir.Thorp.QueryTree.weighted line 540
  62. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.weighted_nonneg line 547
  63. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.weighted_congr line 554
  64. def OAI.ThorpNine.Casimir.Thorp.QueryTree.flipCoin line 569
  65. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.flipCoin_apply_eq line 577
  66. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.flipCoin_apply_ne line 581
  67. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.weighted_flip_of_not_mem line 586
  68. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.mean_indicator_bit line 592
  69. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.mean_weighted_le_one line 611
  70. def OAI.ThorpNine.Casimir.Thorp.QueryTree.succeeds line 645
  71. def OAI.ThorpNine.Casimir.Thorp.QueryTree.charge line 651
  72. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.weighted_eq line 658
  73. lemma OAI.ThorpNine.Casimir.Thorp.QueryTree.success_probability_le line 671
  74. def OAI.ThorpNine.Casimir.Thorp.encodeButterfly line 692
  75. lemma OAI.ThorpNine.Casimir.Thorp.decode_encodeButterfly line 697
  76. lemma OAI.ThorpNine.Casimir.Thorp.encode_decodeButterfly line 707
  77. def OAI.ThorpNine.Casimir.Thorp.butterflyCoinEquiv line 717
  78. def OAI.ThorpNine.Casimir.Thorp.routeDomain line 723
  79. def OAI.ThorpNine.Casimir.Thorp.routeValue line 730