OAI/Computability/DirectedFeedback/RankGraph/CloneGap.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.CloneGap.cart line 11
  2. theorem OAI.DFVSGames.Reduction.CloneGap.count_const line 14
  3. theorem OAI.DFVSGames.Reduction.CloneGap.count_cart line 18
  4. theorem OAI.DFVSGames.Reduction.CloneGap.length_cart line 30
  5. theorem OAI.DFVSGames.Reduction.CloneGap.count_cart_left line 35
  6. theorem OAI.DFVSGames.Reduction.CloneGap.count_cart_right line 39
  7. theorem OAI.DFVSGames.Reduction.CloneGap.count_cart_le line 43
  8. theorem OAI.DFVSGames.Reduction.CloneGap.count_union_le line 57
  9. theorem OAI.DFVSGames.Reduction.CloneGap.count_remove line 65
  10. abbrev OAI.DFVSGames.Reduction.CloneGap.Index line 73
  11. def OAI.DFVSGames.Reduction.CloneGap.indices line 74
  12. def OAI.DFVSGames.Reduction.CloneGap.triples line 75
  13. def OAI.DFVSGames.Reduction.CloneGap.collision line 76
  14. def OAI.DFVSGames.Reduction.CloneGap.distinctTriples line 78
  15. theorem OAI.DFVSGames.Reduction.CloneGap.length_indices line 80
  16. theorem OAI.DFVSGames.Reduction.CloneGap.length_triples line 81
  17. theorem OAI.DFVSGames.Reduction.CloneGap.count_index_eq_le line 84
  18. theorem OAI.DFVSGames.Reduction.CloneGap.count_collision_le line 94
  19. theorem OAI.DFVSGames.Reduction.CloneGap.majority_exists line 123
  20. def OAI.DFVSGames.Reduction.CloneGap.allAgree line 137
  21. theorem OAI.DFVSGames.Reduction.CloneGap.count_agree_distinct line 140
  22. structure OAI.DFVSGames.Reduction.CloneGap.Equation line 157
  23. def OAI.DFVSGames.Reduction.CloneGap.satisfied line 165
  24. def OAI.DFVSGames.Reduction.CloneGap.clone line 168
  25. theorem OAI.DFVSGames.Reduction.CloneGap.lift_preserves line 171
  26. theorem OAI.DFVSGames.Reduction.CloneGap.clone_names_distinct line 174
  27. theorem OAI.DFVSGames.Reduction.CloneGap.agree_failure line 185
  28. theorem OAI.DFVSGames.Reduction.CloneGap.failed_occurrence_clones line 195
  29. def OAI.DFVSGames.Reduction.CloneGap.majorityBit line 211
  30. theorem OAI.DFVSGames.Reduction.CloneGap.majorityBit_count line 213
  31. def OAI.DFVSGames.Reduction.CloneGap.cloneList line 225
  32. theorem OAI.DFVSGames.Reduction.CloneGap.length_cloneList line 228
  33. theorem OAI.DFVSGames.Reduction.CloneGap.cloneList_failure_lower line 237
  34. theorem OAI.DFVSGames.Reduction.CloneGap.clone_gap line 256
  35. theorem OAI.DFVSGames.Reduction.CloneGap.clone_completeness_count line 275
  36. abbrev OAI.DFVSGames.Foundations.Hastad.FoldedEquation.Address line 301
  37. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.storedAssignment line 303
  38. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 307
  39. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.correction_eq line 311
  40. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equation line 318
  41. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.xor_corrections line 325
  42. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 332
  43. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 344
  44. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equation_indicator line 354
  45. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 365
  46. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 373
  47. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 383
  48. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 389
  49. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 395
  50. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 401
  51. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 413
  52. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 424
  53. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 437
  54. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 450
  55. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 456
  56. def OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 463
  57. theorem OAI.DFVSGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 470
  58. def OAI.DFVSGames.Foundations.Hastad.mapEquation line 489
  59. theorem OAI.DFVSGames.Foundations.Hastad.satisfied_mapEquation line 496
  60. abbrev OAI.DFVSGames.Foundations.Hastad.EmptyContext.Address line 504
  61. def OAI.DFVSGames.Foundations.Hastad.EmptyContext.storedAssignment line 506
  62. def OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation line 509
  63. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 516
  64. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_satisfied line 521
  65. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 530
  66. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_flip_first line 536
  67. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 542
  68. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 546
  69. def OAI.DFVSGames.Foundations.Hastad.EmptyContext.pairedEquations line 552
  70. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 556
  71. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 560
  72. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 564
  73. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 571
  74. def OAI.DFVSGames.Foundations.Hastad.EmptyContext.equationAcceptance line 579
  75. def OAI.DFVSGames.Foundations.Hastad.EmptyContext.equationBias line 582
  76. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 585
  77. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equation_indicator line 590
  78. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 596
  79. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 603
  80. theorem OAI.DFVSGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 614
  81. def OAI.DFVSGames.Reduction.FiniteNoise.realizedBit line 631
  82. def OAI.DFVSGames.Reduction.FiniteNoise.realizedNoise line 633
  83. theorem OAI.DFVSGames.Reduction.FiniteNoise.realizedBit_eq_true_iff line 636
  84. theorem OAI.DFVSGames.Reduction.FiniteNoise.coordinate_fiber_sum line 640
  85. theorem OAI.DFVSGames.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 664
  86. theorem OAI.DFVSGames.Reduction.FiniteNoise.fiber_product_eq_indicator line 676
  87. theorem OAI.DFVSGames.Reduction.FiniteNoise.expect_realizedNoise line 689
  88. theorem OAI.DFVSGames.Foundations.Hastad.dictator_test_parity line 723
  89. theorem OAI.DFVSGames.Foundations.Hastad.noise_coordinate_sign line 729
  90. theorem OAI.DFVSGames.Foundations.Hastad.noise_coordinate_false line 738
  91. theorem OAI.DFVSGames.Foundations.Hastad.testAcceptance_dictator line 751
  92. theorem OAI.DFVSGames.Foundations.Hastad.testAcceptance_folded_dictators line 769
  93. theorem OAI.DFVSGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 780
  94. theorem OAI.DFVSGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 796
  95. def OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance line 809
  96. theorem OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 814
  97. theorem OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance_dictator line 823
  98. theorem OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 829
  99. theorem OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 836
  100. theorem OAI.DFVSGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 846