OAI/Computability/UniqueGames/Reduction/IncidenceProbabilityLemmas.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Actual finite incidence-game probabilities for Proposition 4.3. The referee samples an occurrence and one of three slots independently and uniformly. Alice sees its occurrence; Bob sees only its variable name.

  1. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.sum_bool_indicator_eq_count_ofFn line 30
  2. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.expect_bool_indicator_eq_count_ofFn line 39

    Source documentation

    Uniform Boolean-event probability is the indexed list's exact occurrence count.

    theorem expect_bool_indicator_eq_count_ofFn {n : Nat} (p : Fin n → Bool) :
    Finset.univ.expect (fun i : Fin n => if p i then (1 : ℚ) else 0) =
      ((List.ofFn p).countP id : ℚ) / n := by
…
  3. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.slotOfFin line 45
  4. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.slotPredicate line 48
  5. instance OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.(instance at line 53) line 53
  6. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.slotAcceptance line 56
  7. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.slot_predicate_is_question_predicate line 59
  8. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.sum_slot_acceptance line 67
  9. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.expect_slot_acceptance line 81
  10. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptanceProbability line 90
  11. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.failureProbability line 95
  12. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptance_probability_eq_expected_count line 99
  13. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptance_probability_nonnegative line 108
  14. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptance_probability_le_one line 116
  15. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptance_plus_failure_third_le_one line 124
  16. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.deterministic_soundness line 137
  17. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.failureCount_eq_countP line 144
  18. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.failure_count_finRange_eq_count_ofFn line 156
  19. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.failure_probability_eq_count_finRange line 167
  20. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.failure_gap_of_count_gap line 179
  21. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.soundness_from_count_gap line 190
  22. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.randomizedAcceptance line 199

    Source documentation

    A finite randomized strategy, with the common coin including both private coins.

    def randomizedAcceptance [Fintype Coin] (equations : Index → Equation Variable)
    (weight : Coin → ℚ) (alice : Coin → Index → Triple)
    (bob : Coin → Variable → Bool) : ℚ :=
…
  23. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.randomized_soundness line 204
  24. instance OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.tripleFintype line 221
  25. instance OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.tripleInhabited line 228
  26. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.deterministicValue line 231

    Source documentation

    The actual game value is the maximum over all deterministic local strategies.

    noncomputable def deterministicValue [Fintype Variable]
    (equations : Index → Equation Variable) : ℚ := by
…
  27. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.acceptance_le_value line 238
  28. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.value_attained line 246
  29. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.value_soundness line 255
  30. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.randomized_acceptance_le_value line 264
  31. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.randomized_value_attained line 280

    Source documentation

    Constant choices of an optimal strategy attain the value under any normalized coin law.

    theorem randomized_value_attained [Fintype Variable] [Fintype Coin]
    (equations : Index → Equation Variable) (weight : Coin → ℚ)
    (weight_sum : ∑ c, weight c = 1) :
    ∃ (alice : Coin → Index → Triple) (bob : Coin → Variable → Bool),
      randomizedAcceptance equations weight alice bob = deterministicValue equations := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.randomizedAcceptance, OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.deterministicValue

  32. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.cloned_failure_probability_gap line 289
  33. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.cloned_value_soundness line 299

    Source documentation

    Actual finite incidence-game value after the concrete 48-clone construction.

    theorem cloned_value_soundness (s : ActualSource.Source)
    (source_gap : ∀ A : Fin s.variables → Bool,
      s.sourceList.length ≤ 4 * s.sourceList.countP (fun e => !CloneGap.satisfied e A)) :
    deterministicValue (FiniteSource.incidenceEquation s) ≤ (191 : ℚ) / 192 := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied, OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.deterministicValue, OAI.UniqueGamesTheorem.Reduction.FiniteSource.incidenceEquation

  34. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.cloned_randomized_soundness line 305
  35. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.uniformDistribution line 324
  36. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.uniform_probability_eq_rat_expect line 332
  37. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.functionalTriple line 344
  38. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.functionalTriple_bitAt line 346
  39. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.extractionIncidence line 350
  40. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.DistinctNames line 355
  41. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.extraction_names_injective line 360
  42. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.foundationGame line 372
  43. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.foundation_success_eq_rat_acceptance line 381
  44. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.foundation_value_soundness line 411
  45. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.foundation_value_le_one_sub_gap_third line 423
  46. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.sourceEquation line 437
  47. def OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.sourceGame line 440
  48. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.source_failure_probability line 444
  49. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.source_value_le_one_sub_gap_third line 452
  50. theorem OAI.UniqueGamesTheorem.Reduction.IncidenceProbability.FoundationBridge.cloned_foundation_value_soundness line 461
  51. theorem OAI.UniqueGamesTheorem.Reduction.SourceProbability.Source_failure_eq_count line 481
  52. theorem OAI.UniqueGamesTheorem.Reduction.SourceProbability.ofList_failure line 502
  53. theorem OAI.UniqueGamesTheorem.Reduction.SourceProbability.count_complement line 509
  54. theorem OAI.UniqueGamesTheorem.Reduction.SourceProbability.failure_add_satisfaction line 516
  55. theorem OAI.UniqueGamesTheorem.Reduction.SourceProbability.quarter_gap_iff line 527
  56. def OAI.UniqueGamesTheorem.Reduction.Preprocessing.rounded line 555
  57. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.rounded_failure_add_value line 560
  58. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.rounded_complete line 570
  59. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.rounded_sound line 582
  60. def OAI.UniqueGamesTheorem.Reduction.Preprocessing.uniformSource line 595
  61. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.cloned_failure_eq line 598
  62. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.uniformSource_complete line 618
  63. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.uniformSource_distinct line 630
  64. theorem OAI.UniqueGamesTheorem.Reduction.Preprocessing.uniformSource_sound line 634