OAI/Computability/MinUncut/Games/IncidenceProbability.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.sum_bool_indicator_eq_count_ofFn line 15
  2. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.expect_bool_indicator_eq_count_ofFn line 23
  3. def OAI.MinUncutGames.Reduction.IncidenceProbability.slotOfFin line 29
  4. def OAI.MinUncutGames.Reduction.IncidenceProbability.slotPredicate line 32
  5. instance OAI.MinUncutGames.Reduction.IncidenceProbability.(instance at line 37) line 37
  6. def OAI.MinUncutGames.Reduction.IncidenceProbability.slotAcceptance line 40
  7. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.slot_predicate_is_question_predicate line 43
  8. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.sum_slot_acceptance line 51
  9. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.expect_slot_acceptance line 65
  10. def OAI.MinUncutGames.Reduction.IncidenceProbability.acceptanceProbability line 74
  11. def OAI.MinUncutGames.Reduction.IncidenceProbability.failureProbability line 79
  12. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.acceptance_probability_eq_expected_count line 83
  13. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.acceptance_probability_nonnegative line 92
  14. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.acceptance_probability_le_one line 100
  15. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.acceptance_plus_failure_third_le_one line 108
  16. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.deterministic_soundness line 121
  17. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.failureCount_eq_countP line 128
  18. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.failure_count_finRange_eq_count_ofFn line 140
  19. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.failure_probability_eq_count_finRange line 151
  20. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.failure_gap_of_count_gap line 163
  21. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.soundness_from_count_gap line 174
  22. def OAI.MinUncutGames.Reduction.IncidenceProbability.randomizedAcceptance line 182
  23. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.randomized_soundness line 187
  24. instance OAI.MinUncutGames.Reduction.IncidenceProbability.tripleFintype line 204
  25. instance OAI.MinUncutGames.Reduction.IncidenceProbability.tripleInhabited line 211
  26. def OAI.MinUncutGames.Reduction.IncidenceProbability.deterministicValue line 213
  27. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.acceptance_le_value line 220
  28. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.value_attained line 228
  29. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.value_soundness line 237
  30. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.randomized_acceptance_le_value line 246
  31. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.randomized_value_attained line 261
  32. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.cloned_failure_probability_gap line 270
  33. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.cloned_value_soundness line 279
  34. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.cloned_randomized_soundness line 285
  35. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.uniformDistribution line 304
  36. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.uniform_probability_eq_rat_expect line 312
  37. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple line 324
  38. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.functionalTriple_bitAt line 326
  39. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.extractionIncidence line 330
  40. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.DistinctNames line 335
  41. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.extraction_names_injective line 340
  42. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.foundationGame line 352
  43. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_success_eq_rat_acceptance line 361
  44. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_soundness line 391
  45. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.foundation_value_le_one_sub_gap_third line 403
  46. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.sourceEquation line 417
  47. def OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.sourceGame line 420
  48. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.source_failure_probability line 424
  49. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.source_value_le_one_sub_gap_third line 432
  50. theorem OAI.MinUncutGames.Reduction.IncidenceProbability.FoundationBridge.cloned_foundation_value_soundness line 441
  51. theorem OAI.MinUncutGames.Reduction.SourceProbability.Source_failure_eq_count line 459
  52. theorem OAI.MinUncutGames.Reduction.SourceProbability.ofList_failure line 480
  53. theorem OAI.MinUncutGames.Reduction.SourceProbability.count_complement line 487
  54. theorem OAI.MinUncutGames.Reduction.SourceProbability.failure_add_satisfaction line 494
  55. theorem OAI.MinUncutGames.Reduction.SourceProbability.quarter_gap_iff line 505