MaskMomentLemmas.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Assembling private decoders from an actual finite advice experiment.

The left response law accepts only the left observation and the right law only the right observation. Their samples are independent conditional on those observations. A positive conditional agreement bound on a positive-mass event therefore gives ordinary deterministic local strategies, by finite averaging. No hidden matrix, witness, or opposite-player observation is an argument of either response law.

def OAI.UniqueGamesTheorem.Clean.bernoulli line 21

Source documentation

true is the singleton branch.

def bernoulli (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    FiniteDistribution Bool where
…

def OAI.UniqueGamesTheorem.Clean.maskCount line 28
Source documentation
The exact mask, including the empty mask at k = 0.
```
def maskCount {k : ℕ} (mask : Fin k → Bool) : ℕ :=
…
```
theorem OAI.UniqueGamesTheorem.Clean.product_mask line 31

theorem OAI.UniqueGamesTheorem.Clean.iid_product_moment line 37

Source documentation

The finite product identity underlying the binomial generating function.

theorem iid_product_moment {Ω : Type*} [Fintype Ω]
    (μ : FiniteDistribution Ω) (f : Ω → ℝ) (k : ℕ) :
    (μ.iid k).expectation (fun x => ∏ i, f (x i)) = μ.expectation f ^ k := by
…

theorem OAI.UniqueGamesTheorem.Clean.bernoulli_mask_moment line 47
def OAI.UniqueGamesTheorem.Clean.cleanProbability line 64
theorem OAI.UniqueGamesTheorem.Clean.cleanProbability_nonneg line 68
theorem OAI.UniqueGamesTheorem.Clean.cleanProbability_le_one line 72
def OAI.UniqueGamesTheorem.Clean.singletonSlopeLaw line 80
Source documentation
Independent singleton choice and uniform advice slope.
```
def singletonSlopeLaw (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) :
    FiniteDistribution (Bool × E) :=
…
```
def OAI.UniqueGamesTheorem.Clean.cleanBit line 86
Source documentation
origin is instantiated by the zero advice slope. Keeping it explicit also shows that every specified slope has exactly the same chance.
```
def cleanBit (origin : E) (sample : Bool × E) : Bool := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.clean_pushforward line 90
theorem OAI.UniqueGamesTheorem.Clean.clean_mask_law line 111
Source documentation
In particular, the whole mask has the independent Bernoulli law.
```
theorem clean_mask_law (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k : ℕ) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).pushforward
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.singletonSlopeLaw
theorem OAI.UniqueGamesTheorem.Clean.clean_mask_moment line 119
theorem OAI.UniqueGamesTheorem.Clean.cleanProbability_ge_of_card_le line 129
theorem OAI.UniqueGamesTheorem.Clean.cleanProbability_ge_dimension line 135

theorem OAI.UniqueGamesTheorem.Clean.mask_rate_antitone line 143

Source documentation

Larger clean probability decreases the moment for a rate in [0,1].

theorem mask_rate_antitone {p q ρ : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1)
    (hqp : q ≤ p) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (k : ℕ) :
    (1 - p * (1 - ρ)) ^ k ≤ (1 - q * (1 - ρ)) ^ k := by
…

theorem OAI.UniqueGamesTheorem.Clean.clean_mask_moment_le line 153
Source documentation
Section 5's numerical specialization. A bound on the number of possible advice slopes gives a uniform bound over every fixed advice map.
```
theorem clean_mask_moment_le (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k : ℕ) {N : ℝ} (hcard : (Fintype.card E : ℝ) ≤ N) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).expectation
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.singletonSlopeLaw

theorem OAI.UniqueGamesTheorem.Clean.clean_mask_moment_le_dimension line 169

Source documentation

2^(dim W + r_s) is chosen before the particular advice-map rank.

theorem clean_mask_moment_le_dimension (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k dimW rs : ℕ) (hcard : Fintype.card E ≤ 2 ^ (dimW + rs)) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).expectation
…

Mentions: OAI.UniqueGamesTheorem.Clean.singletonSlopeLaw

theorem OAI.UniqueGamesTheorem.Clean.mask_rate_le_exp line 180
Source documentation
The exponential estimate uses nonnegativity of 1 - x before raising to a natural power. It also covers the empty mask.
```
theorem mask_rate_le_exp {x : ℝ} (hx : x ≤ 1) (k : ℕ) :
    (1 - x) ^ k ≤ Real.exp (-(k : ℝ) * x) := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.clean_mask_moment_le_exp line 190
theorem OAI.UniqueGamesTheorem.Clean.cube_singleton_probability_nonneg line 206
theorem OAI.UniqueGamesTheorem.Clean.cube_singleton_probability_le_one line 209
theorem OAI.UniqueGamesTheorem.Clean.cube_mask_rate_le_exp line 219
Source documentation
On cubes, k = n^3 and beta = n^(-2), so k * beta = n. The advice-space size bound N is fixed independently of n.
```
theorem cube_mask_rate_le_exp {n : ℕ} (hn : 1 ≤ n) {N : ℝ} (hN : 1 ≤ N) :
    (1 - ((1 / (n : ℝ)) ^ 2 / N) / 3600) ^ (n ^ 3) ≤
      Real.exp (-(n : ℝ) / (3600 * N)) := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.exists_cube_exponential_lt line 242
Source documentation
A repetition cube can be selected after fixing only the advice-space size bound and the required error. This is a scalar fact, not a game-value theorem.
```
theorem exists_cube_exponential_lt {N error : ℝ} (hN : 0 < N) (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ Real.exp (-(n : ℝ) / (3600 * N)) < error := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.exists_cube_mask_rate_lt line 261
def OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.observedGame line 295
def OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.conditionalAgreement line 301
theorem OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.conditionalAgreement_nonnegative line 307
theorem OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.conditionalAgreement_le_one line 314
theorem OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.stochasticSuccess_eq_actual_expectation line 320

theorem OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.good_data_mass_lower line 343

Source documentation

Averaging conditional independent decoder success over the actual advice draw multiplies the two positive lower bounds.

theorem good_data_mass_lower
    [DecidableEq Q₁] [DecidableEq Q₂]
    (law : FiniteDistribution Ω) (leftObservation : Ω → Q₁)
    (rightObservation : Ω → Q₂) (accepts : Q₁ → Q₂ → A₁ → A₂ → Bool)
    (left : Q₁ → FiniteDistribution A₁) (right : Q₂ → FiniteDistribution A₂)
    (good : Ω → Bool) (γ₁ γ₂ : ℝ) (hγ₂ : 0 ≤ γ₂)
    (hmass : γ₁ ≤ law.probability good)
    (hagreement : ∀ ω, good ω = true → γ₂ ≤
      conditionalAgreement left right accepts (leftObservation ω) (rightObservation ω)) :
    γ₁ * γ₂ ≤
      (observedGame law leftObservation rightObservation accepts).stochasticSuccess left right := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.conditionalAgreement, OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.observedGame

theorem OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.exists_local_deterministic_strategies line 371

Source documentation

The final strategies receive precisely their local observations. Private sampling is eliminated by the existing finite response-table construction.

theorem exists_local_deterministic_strategies
    [DecidableEq Q₁] [DecidableEq Q₂] [Nonempty A₁] [Nonempty A₂]
    (law : FiniteDistribution Ω) (leftObservation : Ω → Q₁)
    (rightObservation : Ω → Q₂) (accepts : Q₁ → Q₂ → A₁ → A₂ → Bool)
    (left : Q₁ → FiniteDistribution A₁) (right : Q₂ → FiniteDistribution A₂)
    (good : Ω → Bool) (γ₁ γ₂ : ℝ) (hγ₂ : 0 ≤ γ₂)
    (hmass : γ₁ ≤ law.probability good)
    (hagreement : ∀ ω, good ω = true → γ₂ ≤
      conditionalAgreement left right accepts (leftObservation ω) (rightObservation ω)) :
    ∃ leftStrategy : Q₁ → A₁, ∃ rightStrategy : Q₂ → A₂,
      γ₁ * γ₂ ≤ law.probability (fun ω => accepts
        (leftObservation ω) (rightObservation ω)
…

Mentions: OAI.UniqueGamesTheorem.Decoder.StrategyAssembly.conditionalAgreement