OAI/Computability/DirectedFeedback/Encoding/Finite.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Reduction.FiniteSource.Name line 58
  2. def OAI.DFVSGames.Reduction.FiniteSource.clonedSource line 60
  3. abbrev OAI.DFVSGames.Reduction.FiniteSource.Occurrence line 62
  4. def OAI.DFVSGames.Reduction.FiniteSource.occurrences line 64
  5. def OAI.DFVSGames.Reduction.FiniteSource.rawEquation line 67
  6. def OAI.DFVSGames.Reduction.FiniteSource.finiteName line 70
  7. def OAI.DFVSGames.Reduction.FiniteSource.mapEquation line 73
  8. def OAI.DFVSGames.Reduction.FiniteSource.equation line 76
  9. theorem OAI.DFVSGames.Reduction.FiniteSource.satisfied_map line 79
  10. theorem OAI.DFVSGames.Reduction.FiniteSource.mem_cart line 82
  11. theorem OAI.DFVSGames.Reduction.FiniteSource.distinctTriple_bounds line 92
  12. theorem OAI.DFVSGames.Reduction.FiniteSource.distinctTriples_nonempty line 99
  13. theorem OAI.DFVSGames.Reduction.FiniteSource.cloned_member_properties line 104
  14. theorem OAI.DFVSGames.Reduction.FiniteSource.raw_properties line 115
  15. theorem OAI.DFVSGames.Reduction.FiniteSource.finiteName_injective_on line 124
  16. theorem OAI.DFVSGames.Reduction.FiniteSource.names_distinct line 130
  17. theorem OAI.DFVSGames.Reduction.FiniteSource.raw_map_occurrences line 139
  18. theorem OAI.DFVSGames.Reduction.FiniteSource.occurrences_length line 143
  19. theorem OAI.DFVSGames.Reduction.FiniteSource.clonedSource_nonempty line 147
  20. instance OAI.DFVSGames.Reduction.FiniteSource.(instance at line 153) line 153
  21. theorem OAI.DFVSGames.Reduction.FiniteSource.indexed_failure_count line 156
  22. theorem OAI.DFVSGames.Reduction.FiniteSource.indexed_gap line 163
  23. theorem OAI.DFVSGames.Reduction.FiniteSource.indexed_completeness_count line 172
  24. def OAI.DFVSGames.Reduction.FiniteSource.incidenceEquation line 183
  25. theorem OAI.DFVSGames.Reduction.FiniteSource.incidence_question_predicate line 186
  26. theorem OAI.DFVSGames.Reduction.FiniteSource.incidence_failure_gap line 195
  27. theorem OAI.DFVSGames.Reduction.FiniteSource.incidence_soundness line 205
  28. def OAI.DFVSGames.Reduction.FiniteSource.nameEquiv line 213
  29. def OAI.DFVSGames.Reduction.FiniteSource.cloned line 216
  30. theorem OAI.DFVSGames.Reduction.FiniteSource.cloned_length line 222
  31. theorem OAI.DFVSGames.Reduction.FiniteSource.cloned_distinct line 227
  32. theorem OAI.DFVSGames.Reduction.FiniteSource.count_ofFn line 234
  33. theorem OAI.DFVSGames.Reduction.FiniteSource.cloned_gap line 241
  34. theorem OAI.DFVSGames.Reduction.FiniteSource.cloned_completeness_count line 256
  35. theorem OAI.DFVSGames.Reduction.IncidenceProbability.sum_bool_indicator_eq_count_ofFn line 276
  36. theorem OAI.DFVSGames.Reduction.IncidenceProbability.expect_bool_indicator_eq_count_ofFn line 284
  37. def OAI.DFVSGames.Reduction.IncidenceProbability.slotOfFin line 290
  38. def OAI.DFVSGames.Reduction.IncidenceProbability.slotPredicate line 293
  39. instance OAI.DFVSGames.Reduction.IncidenceProbability.(instance at line 298) line 298
  40. def OAI.DFVSGames.Reduction.IncidenceProbability.slotAcceptance line 301
  41. theorem OAI.DFVSGames.Reduction.IncidenceProbability.slot_predicate_is_question_predicate line 304
  42. theorem OAI.DFVSGames.Reduction.IncidenceProbability.sum_slot_acceptance line 312
  43. theorem OAI.DFVSGames.Reduction.IncidenceProbability.expect_slot_acceptance line 326
  44. def OAI.DFVSGames.Reduction.IncidenceProbability.acceptanceProbability line 335
  45. def OAI.DFVSGames.Reduction.IncidenceProbability.failureProbability line 340
  46. theorem OAI.DFVSGames.Reduction.IncidenceProbability.acceptance_probability_eq_expected_count line 344
  47. theorem OAI.DFVSGames.Reduction.IncidenceProbability.acceptance_probability_nonnegative line 353
  48. theorem OAI.DFVSGames.Reduction.IncidenceProbability.acceptance_probability_le_one line 361
  49. theorem OAI.DFVSGames.Reduction.IncidenceProbability.acceptance_plus_failure_third_le_one line 369
  50. theorem OAI.DFVSGames.Reduction.IncidenceProbability.deterministic_soundness line 382
  51. theorem OAI.DFVSGames.Reduction.IncidenceProbability.failureCount_eq_countP line 389
  52. theorem OAI.DFVSGames.Reduction.IncidenceProbability.failure_count_finRange_eq_count_ofFn line 401
  53. theorem OAI.DFVSGames.Reduction.IncidenceProbability.failure_probability_eq_count_finRange line 412
  54. theorem OAI.DFVSGames.Reduction.IncidenceProbability.failure_gap_of_count_gap line 424
  55. theorem OAI.DFVSGames.Reduction.IncidenceProbability.soundness_from_count_gap line 435
  56. def OAI.DFVSGames.Reduction.IncidenceProbability.randomizedAcceptance line 443
  57. theorem OAI.DFVSGames.Reduction.IncidenceProbability.randomized_soundness line 448
  58. instance OAI.DFVSGames.Reduction.IncidenceProbability.tripleFintype line 465
  59. instance OAI.DFVSGames.Reduction.IncidenceProbability.tripleInhabited line 472
  60. def OAI.DFVSGames.Reduction.IncidenceProbability.deterministicValue line 474
  61. theorem OAI.DFVSGames.Reduction.IncidenceProbability.acceptance_le_value line 481
  62. theorem OAI.DFVSGames.Reduction.IncidenceProbability.value_attained line 489
  63. theorem OAI.DFVSGames.Reduction.IncidenceProbability.value_soundness line 498
  64. theorem OAI.DFVSGames.Reduction.IncidenceProbability.randomized_acceptance_le_value line 507
  65. theorem OAI.DFVSGames.Reduction.IncidenceProbability.randomized_value_attained line 522
  66. theorem OAI.DFVSGames.Reduction.IncidenceProbability.cloned_failure_probability_gap line 531
  67. theorem OAI.DFVSGames.Reduction.IncidenceProbability.cloned_value_soundness line 540
  68. theorem OAI.DFVSGames.Reduction.IncidenceProbability.cloned_randomized_soundness line 546
  69. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.uniformDistribution line 565
  70. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.uniform_probability_eq_rat_expect line 573
  71. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple line 585
  72. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple_bitAt line 587
  73. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.extractionIncidence line 591
  74. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.DistinctNames line 596
  75. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.extraction_names_injective line 601
  76. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.foundationGame line 613
  77. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.foundation_success_eq_rat_acceptance line 622
  78. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_soundness line 652
  79. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_le_one_sub_gap_third line 664
  80. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.sourceEquation line 678
  81. def OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.sourceGame line 681
  82. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.source_failure_probability line 685
  83. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.source_value_le_one_sub_gap_third line 693
  84. theorem OAI.DFVSGames.Reduction.IncidenceProbability.FoundationBridge.cloned_foundation_value_soundness line 702
  85. theorem OAI.DFVSGames.Reduction.SourceProbability.Source_failure_eq_count line 721
  86. theorem OAI.DFVSGames.Reduction.SourceProbability.ofList_failure line 742
  87. theorem OAI.DFVSGames.Reduction.SourceProbability.count_complement line 749
  88. theorem OAI.DFVSGames.Reduction.SourceProbability.failure_add_satisfaction line 756
  89. theorem OAI.DFVSGames.Reduction.SourceProbability.quarter_gap_iff line 767
  90. def OAI.DFVSGames.Outer.HastadSource.success line 796
  91. def OAI.DFVSGames.Outer.HastadSource.asSource line 800
  92. theorem OAI.DFVSGames.Outer.HastadSource.failure_add_success line 803
  93. def OAI.DFVSGames.Outer.HastadSource.gapInput line 811
  94. def OAI.DFVSGames.Outer.HastadSource.sourceMap line 815
  95. def OAI.DFVSGames.Outer.HastadSource.output line 819
  96. theorem OAI.DFVSGames.Outer.HastadSource.complete line 823
  97. theorem OAI.DFVSGames.Outer.HastadSource.sound line 830
  98. def OAI.DFVSGames.Outer.HastadSource.roundMachine line 839
  99. theorem OAI.DFVSGames.Outer.HastadSource.roundMachine_finite line 842
  100. def OAI.DFVSGames.Outer.HastadSource.gapMachine line 847
  101. def OAI.DFVSGames.Outer.HastadSource.sourceMachine line 855
  102. def OAI.DFVSGames.Outer.HastadSource.computation line 861
  103. theorem OAI.DFVSGames.Outer.HastadSource.finiteAlphabet line 866
  104. structure OAI.DFVSGames.Outer.HastadSource.Reduction line 873
  105. theorem OAI.DFVSGames.Outer.HastadSource.exists_reduction line 880