Experiment.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual sparse clean experiment

The explicit seed has an independent singleton coin and uniform single-column advice at each position. Additional independent data supply the intercept and both full-block columns. Unused columns are sampled and discarded, allowing a fixed finite product sample space. A local strategy may depend on the fixed seed; the bound consequently also covers the original, less informed players.

The only mathematical rate input below is the stated bound on the actual ordinary repeated game. No conditional distribution, local reconstruction, mask distribution, or averaging assertion is assumed.

abbrev OAI.UniqueGamesTheorem.Clean.Experiment.Coefficient line 35
abbrev OAI.UniqueGamesTheorem.Clean.Experiment.Additional line 36
abbrev OAI.UniqueGamesTheorem.Clean.Experiment.SparseSeed line 37
def OAI.UniqueGamesTheorem.Clean.Experiment.singletonSet line 39
def OAI.UniqueGamesTheorem.Clean.Experiment.coefficients line 42
theorem OAI.UniqueGamesTheorem.Clean.Experiment.zeroSet_eq_cleanMask line 52
Source documentation
The actual zero coefficient set is exactly the clean mask counted by the Bernoulli law. The homogeneous intercept and full columns never enter it.
```
theorem zeroSet_eq_cleanMask {k : ℕ} (extra : Additional k R) (seed : SparseSeed k R) :
    zeroSet (singletonSet seed) (coefficients extra seed) =
      Finset.univ.filter (fun i => cleanBit (ZeroInformation.zero : Coefficient R) (seed i) = true) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.Experiment.Additional, OAI.UniqueGamesTheorem.Clean.Experiment.SparseSeed, OAI.UniqueGamesTheorem.Clean.Experiment.singletonSet, OAI.UniqueGamesTheorem.Clean.Experiment.coefficients, OAI.UniqueGamesTheorem.Clean.cleanBit, OAI.UniqueGamesTheorem.Clean.Experiment.Coefficient
theorem OAI.UniqueGamesTheorem.Clean.Experiment.zeroSet_card line 63
abbrev OAI.UniqueGamesTheorem.Clean.Experiment.LocalStrategies line 69
def OAI.UniqueGamesTheorem.Clean.Experiment.success line 73
Source documentation
Exact nested finite expectation of the advice-agreement experiment.
```
def success (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.Experiment.Additional, OAI.UniqueGamesTheorem.Clean.Experiment.SparseSeed, OAI.UniqueGamesTheorem.Clean.Experiment.LocalStrategies
theorem OAI.UniqueGamesTheorem.Clean.Experiment.expectation_mono line 83
theorem OAI.UniqueGamesTheorem.Clean.Experiment.expectation_const line 89

theorem OAI.UniqueGamesTheorem.Clean.Experiment.success_le_of_repetition line 96

Source documentation

Exact clean-coordinate upper bound for arbitrary weighted occurrences. The sole external theorem input rate concerns the genuine classical repeated game, so its alphabet dependence cannot be concealed in this interface.

theorem success_le_of_repetition (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    success k μ g extraLaw β hβ₀ hβ₁ strategy ≤
      (1 - (β / (Fintype.card (Coefficient R) : ℝ)) * (1 - ρ)) ^ k := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.Experiment.Additional, OAI.UniqueGamesTheorem.Clean.Experiment.SparseSeed, OAI.UniqueGamesTheorem.Clean.Experiment.LocalStrategies, OAI.UniqueGamesTheorem.Clean.Experiment.success, OAI.UniqueGamesTheorem.Clean.Experiment.Coefficient

theorem OAI.UniqueGamesTheorem.Clean.Experiment.randomized_success_le_of_repetition line 125

Source documentation

Uniform finite private/shared strategy seeds are also covered by the same constant bound; the seed is sampled before the questions.

theorem randomized_success_le_of_repetition {Seed : Type*} [Fintype Seed]
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (seedLaw : FiniteDistribution Seed)
    (strategy : Seed → Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    seedLaw.expectation (fun seed => success k μ g extraLaw β hβ₀ hβ₁ (strategy seed)) ≤
      (1 - (β / (Fintype.card (Coefficient R) : ℝ)) * (1 - ρ)) ^ k := by
…