ValueLemmas.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Question-dependent stochastic responses are derandomized by sampling complete answer tables independently before the questions. The table law, marginal law, and mixture identity are proved from finite products and sums. No derandomization principle is assumed as a hypothesis or axiom.

def OAI.UniqueGamesTheorem.Foundations.Games.Game.value line 22
Source documentation
A maximum of the finitely many actual deterministic success probabilities.
```
def value (G : Game Q₁ Q₂ A₁ A₂) : ℝ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_le_value line 26
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.value_le_iff line 31
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.exists_optimal_strategy line 36
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.value_nonnegative line 43
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.value_le_one line 48
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.randomized_success_le_value line 53
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.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.Strategy
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_repetition_zero line 66
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.value_repetition_zero line 75
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.pow_value_le_repetition_value line 83
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.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.Game.value
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.value_le_of_localSimulation line 89
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 130
def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table line 141
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.UniqueGamesTheorem.Foundations.Games.FiniteDistribution
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_table_eval line 152
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table_eval_pushforward line 180
def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.product line 194
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_product line 203
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_comm line 209
theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_congr line 222
def OAI.UniqueGamesTheorem.Foundations.Games.Game.responseTableLaw line 235
def OAI.UniqueGamesTheorem.Foundations.Games.Game.stochasticSuccess line 241
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_eq_question_expectation line 250
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.table_success_eq_stochastic line 257
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.stochasticSuccess_le_value line 295
theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.exists_deterministic_ge_stochastic line 303