OAI/Computability/MaxCut/Games/Basic.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Finite two-player games with actual joint question distributions.

An answer function receives only its own player's question. In a repeated game, that question is the entire tuple, so a repeated strategy need not act separately on coordinates. The predicate may reject invalid answers depending on questions. All probabilities below are actual finite sums of real weights.

  1. structure OAI.MaxCutGames.Foundations.Games.FiniteDistribution line 21
  2. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation line 30
  3. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability line 33
  4. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 36
  5. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_le_one line 44
  6. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_true line 53
  7. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_false line 57
  8. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_mono line 61
  9. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.pushforward line 74

    Source documentation

    Pushforward counts all preimages, including collisions.

    def pushforward (μ : FiniteDistribution Ω) (f : Ω → Γ) : FiniteDistribution Γ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution

  10. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_pushforward line 86
  11. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.transport line 98
  12. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_transport line 103
  13. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.iid line 110

    Source documentation

    Independent repeated sampling, including the single empty tuple at n=0.

    def iid (μ : FiniteDistribution Ω) (n : Nat) : FiniteDistribution (Fin n → Ω) where
…

    Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution

  14. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_iid_all line 115
  15. abbrev OAI.MaxCutGames.Foundations.Games.Strategy line 134
  16. structure OAI.MaxCutGames.Foundations.Games.Game line 136
  17. def OAI.MaxCutGames.Foundations.Games.Game.wins line 148
  18. def OAI.MaxCutGames.Foundations.Games.Game.success line 152
  19. theorem OAI.MaxCutGames.Foundations.Games.Game.success_nonnegative line 155
  20. theorem OAI.MaxCutGames.Foundations.Games.Game.success_le_one line 159
  21. def OAI.MaxCutGames.Foundations.Games.Game.simulatedStrategy line 166

    Source documentation

    Local question reconstruction and answer decoding never expose the other player's question to a strategy. Any fixed advice is an ordinary fixed parameter of these functions.

    def simulatedStrategy {R₁ R₂ B₁ B₂ : Type*}
    (questionMap₁ : Q₁ → R₁) (questionMap₂ : Q₂ → R₂)
    (answerMap₁ : Q₁ → B₁ → A₁) (answerMap₂ : Q₂ → B₂ → A₂)
    (strategy : Strategy R₁ R₂ B₁ B₂) : Strategy Q₁ Q₂ A₁ A₂ :=
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Strategy

  22. theorem OAI.MaxCutGames.Foundations.Games.Game.success_le_of_localSimulation line 175

    Source documentation

    An acceptance implication under an exact question-law pushforward gives an actual success-probability comparison for every pair of local strategies.

    theorem success_le_of_localSimulation {R₁ R₂ B₁ B₂ : Type*}
    [Fintype R₁] [Fintype R₂] [Fintype B₁] [Fintype B₂]
    (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
    (questionMap₁ : Q₁ → R₁) (questionMap₂ : Q₂ → R₂)
    (answerMap₁ : Q₁ → B₁ → A₁) (answerMap₂ : Q₂ → B₂ → A₂)
    (questionLaw : H.questions =
      G.questions.pushforward (fun q => (questionMap₁ q.1, questionMap₂ q.2)))
    (acceptance : ∀ x y a b,
      H.accepts (questionMap₁ x) (questionMap₂ y) a b = true →
      G.accepts x y (answerMap₁ x a) (answerMap₂ y b) = true)
    (strategy : Strategy R₁ R₂ B₁ B₂) :
    H.success strategy ≤
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Strategy

  23. def OAI.MaxCutGames.Foundations.Games.Game.tupleQuestionEquiv line 194
  24. def OAI.MaxCutGames.Foundations.Games.Game.repetition line 202

    Source documentation

    Parallel repetition retains arbitrary dependence on each full local tuple.

    def repetition (G : Game Q₁ Q₂ A₁ A₂) (n : Nat) :
    Game (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game

  25. def OAI.MaxCutGames.Foundations.Games.Game.repeatStrategy line 211

    Source documentation

    Playing a fixed base strategy separately in each coordinate is one permitted repeated strategy, though repeated strategies are more general.

    def repeatStrategy (strategy : Strategy Q₁ Q₂ A₁ A₂) (n : Nat) :
    Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Strategy

  26. theorem OAI.MaxCutGames.Foundations.Games.Game.success_repeatStrategy line 215
  27. theorem OAI.MaxCutGames.Foundations.Games.Game.repetition_question_weight line 223
  28. theorem OAI.MaxCutGames.Foundations.Games.Game.repetition_accepts_iff line 228
  29. def OAI.MaxCutGames.Foundations.Games.Game.coordinateWin line 236

    Source documentation

    One coordinate's success may depend on the entire local question tuples.

    def coordinateWin (G : Game Q₁ Q₂ A₁ A₂) {n : Nat}
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (coordinate : Fin n) (questions : (Fin n → Q₁) × (Fin n → Q₂)) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Strategy

  30. def OAI.MaxCutGames.Foundations.Games.Game.selectedWins line 242
  31. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedWins_mono line 248
  32. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedWins_empty line 259
  33. theorem OAI.MaxCutGames.Foundations.Games.Game.selectedWins_univ line 265
  34. def OAI.MaxCutGames.Foundations.Games.Game.value line 279

    Source documentation

    A maximum of the finitely many actual deterministic success probabilities.

    def value (G : Game Q₁ Q₂ A₁ A₂) : ℝ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game

  35. theorem OAI.MaxCutGames.Foundations.Games.Game.success_le_value line 283
  36. theorem OAI.MaxCutGames.Foundations.Games.Game.value_le_iff line 288
  37. theorem OAI.MaxCutGames.Foundations.Games.Game.exists_optimal_strategy line 293
  38. theorem OAI.MaxCutGames.Foundations.Games.Game.value_nonnegative line 300
  39. theorem OAI.MaxCutGames.Foundations.Games.Game.value_le_one line 305
  40. theorem OAI.MaxCutGames.Foundations.Games.Game.randomized_success_le_value line 310

    Source documentation

    Any fixed finite random seed merely chooses a deterministic strategy pair. Separate private seeds are covered by taking their pair as Seed.

    theorem randomized_success_le_value (G : Game Q₁ Q₂ A₁ A₂)
    {Seed : Type*} [Fintype Seed] (seedLaw : FiniteDistribution Seed)
    (strategies : Seed → Strategy Q₁ Q₂ A₁ A₂) :
    seedLaw.expectation (fun seed => G.success (strategies seed)) ≤ G.value := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.Strategy

  41. theorem OAI.MaxCutGames.Foundations.Games.Game.success_repetition_zero line 323
  42. theorem OAI.MaxCutGames.Foundations.Games.Game.value_repetition_zero line 332
  43. theorem OAI.MaxCutGames.Foundations.Games.Game.pow_value_le_repetition_value line 340

    Source documentation

    The product strategy supplies a lower bound, not an upper bound, for parallel repetition. A genuine decay upper bound needs a separate theorem.

    theorem pow_value_le_repetition_value (G : Game Q₁ Q₂ A₁ A₂) (n : Nat) :
    G.value ^ n ≤ (G.repetition n).value := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.Game.value

  44. theorem OAI.MaxCutGames.Foundations.Games.Game.value_le_of_localSimulation line 346
  45. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 375
  46. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table line 386

    Source documentation

    Independently sample one response for each possible private question.

    def table [DecidableEq Q] (responses : Q → FiniteDistribution A) :
    FiniteDistribution (Q → A) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution

  47. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 397
  48. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 425
  49. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.product line 439
  50. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation_product line 448
  51. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation_comm line 454
  52. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation_congr line 467
  53. def OAI.MaxCutGames.Foundations.Games.Game.responseTableLaw line 480
  54. def OAI.MaxCutGames.Foundations.Games.Game.stochasticSuccess line 486
  55. theorem OAI.MaxCutGames.Foundations.Games.Game.success_eq_question_expectation line 495
  56. theorem OAI.MaxCutGames.Foundations.Games.Game.table_success_eq_stochastic line 502
  57. theorem OAI.MaxCutGames.Foundations.Games.Game.stochasticSuccess_le_value line 540
  58. theorem OAI.MaxCutGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 548
  59. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.iid_pushforward line 569
  60. def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.uniform line 589
  61. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.iid_uniform line 598
  62. theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.expectation_uniform line 605