ExpectationComparisonLemmas.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

The real-valued finite-expectation argument in Lemma 6.3 and equation (6.11). The density's normalization and second-moment bound are inputs; the variance, Cauchy--Schwarz comparison, parameter error, and transferred signal are proved. The test is allowed to depend on every coordinate of the sampled map.

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.density_variance_identity line 25

Source documentation

Centering a normalized density subtracts exactly one from its second moment.

theorem density_variance_identity (s : Finset ι) (hs : s.Nonempty)
    (d : ι → ℝ) (hd : (𝔼 i ∈ s, d i) = 1) :
    (𝔼 i ∈ s, (d i - 1) ^ 2) = (𝔼 i ∈ s, d i ^ 2) - 1 := by
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.density_variance_le line 39
theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.bounded_test_second_moment line 46

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.bounded_test_centered_square line 54

Source documentation

Cauchy--Schwarz for an arbitrary whole-map test, in squared form.

theorem bounded_test_centered_square (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε : ℝ) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) :
    (𝔼 i ∈ s, H i * (d i - 1)) ^ 2 ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.bounded_test_expectation_comparison line 68

Source documentation

The actual difference of the two normalized finite expectations.

theorem bounded_test_expectation_comparison (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε : ℝ) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) :
    |(𝔼 i ∈ s, H i * d i) - (𝔼 i ∈ s, H i)| ≤ Real.sqrt ε := by
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.comparison_error_le_quarter line 83
Source documentation
The squared parameter inequality implies error at most θ/4.
```
theorem comparison_error_le_quarter (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2) : Real.sqrt ε ≤ θ / 4 := by
…
```
theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.parameter_error_le_quarter line 88
Source documentation
The real inequality selected by equation (4.4) gives its stated error.
```
theorem parameter_error_le_quarter (t k cap θ : ℝ) (hk : 0 < k)
    (hθ : 0 < θ) (hsize : 16 * t ^ 2 * cap / θ ^ 2 ≤ k) :
    Real.sqrt (t ^ 2 / k * cap) ≤ θ / 4 := by
…
```
theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.map_law_parameter_error line 98
theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.bounded_test_expectation_quarter line 105

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.transferred_signal_lower line 115

Source documentation

A signal at least θ under the uniform law stays at least θ/2 after transfer.

theorem transferred_signal_lower (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) (hsignal : θ ≤ (𝔼 i ∈ s, H i)) :
    θ / 2 ≤ (𝔼 i ∈ s, H i * d i) := by
…

def OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.wholeMapTest line 126

Source documentation

Equation (6.10), allowing the chosen index and sign to depend on the row.

def wholeMapTest {Map Row Column Index : Type*} (row : Map → Row)
    (column : Map → Column) (sign : Row → ℝ) (value : Row → Column → ℝ)
    (chosen : Row → Index) (character : Index → Column → ℝ) (M : Map) : ℝ :=
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.wholeMapTest_abs_le_one line 131

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.wholeMapTest_comparison line 149

Source documentation

Instantiate comparison with equation (6.10), including its row-dependent index.

theorem wholeMapTest_comparison {Map Row Column Index : Type*}
    (s : Finset Map) (hs : s.Nonempty) (d : Map → ℝ) (ε : ℝ)
    (row : Map → Row) (column : Map → Column) (sign : Row → ℝ)
    (value : Row → Column → ℝ) (chosen : Row → Index)
    (character : Index → Column → ℝ)
    (hd : (𝔼 M ∈ s, d M) = 1)
    (hsecond : (𝔼 M ∈ s, d M ^ 2) ≤ 1 + ε)
    (hsign : ∀ r, |sign r| ≤ 1) (hvalue : ∀ r c, |value r c| ≤ 1)
    (hcharacter : ∀ t c, |character t c| ≤ 1) :
    |(𝔼 M ∈ s, wholeMapTest row column sign value chosen character M * d M) -
      (𝔼 M ∈ s, wholeMapTest row column sign value chosen character M)|
      ≤ Real.sqrt ε := by
…

Mentions: OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.wholeMapTest

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.averaged_expectation_comparison line 167

Source documentation

Average a uniform per-U error, allowing the map sample space to depend on U.

theorem averaged_expectation_comparison {U : Type*} (Map : U → Type*)
    (us : Finset U) (hus : us.Nonempty) (maps : (u : U) → Finset (Map u))
    (hmaps : ∀ u ∈ us, (maps u).Nonempty)
    (d H : (u : U) → Map u → ℝ) (ε : ℝ)
    (hd : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M) = 1)
    (hsecond : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M ^ 2) ≤ 1 + ε)
    (hH : ∀ u ∈ us, ∀ M ∈ maps u, |H u M| ≤ 1) :
    |(𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M * d u M) -
      (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M)| ≤ Real.sqrt ε := by
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.averaged_transferred_signal_lower line 188

Source documentation

Equation (6.11): only the signal averaged over U is assumed large.

theorem averaged_transferred_signal_lower {U : Type*} (Map : U → Type*)
    (us : Finset U) (hus : us.Nonempty) (maps : (u : U) → Finset (Map u))
    (hmaps : ∀ u ∈ us, (maps u).Nonempty)
    (d H : (u : U) → Map u → ℝ) (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2)
    (hd : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M) = 1)
    (hsecond : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M ^ 2) ≤ 1 + ε)
    (hH : ∀ u ∈ us, ∀ M ∈ maps u, |H u M| ≤ 1)
    (hsignal : θ ≤ (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M)) :
    θ / 2 ≤ (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M * d u M) := by
…

theorem OAI.UniqueGamesTheorem.Soundness.ExpectationComparison.uniform_expect_eq_sum_div_card line 205
Source documentation
Uniform finite means in the quotient-of-sums convention.
```
theorem uniform_expect_eq_sum_div_card [Fintype ι] (f : ι → ℝ) :
    (𝔼 i, f i) = (∑ i, f i) / (Fintype.card ι : ℝ) :=
…
```
abbrev OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Triple line 217
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.xorTriple line 219
structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence line 221
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence.accepts line 225
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence.namedAccepts line 232
Source documentation
The incidence predicate as a game on the actual questions (o,n), with the retained slot left internal to the verifier.
```
def Incidence.namedAccepts {Occurrence Name : Type}
    (g : Incidence Occurrence Name) (o : Occurrence) (n : Name)
    (a : Triple) (b : Bool) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Triple
theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence.accepts_implies_namedAccepts line 237
theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence.namedAccepts_iff_accepts line 245
Source documentation
Distinct names make the named-variable predicate equivalent to the sampled retained-slot predicate, without revealing that slot to either strategy.
```
theorem Incidence.namedAccepts_iff_accepts {Occurrence Name : Type}
    (g : Incidence Occurrence Name)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (o : Occurrence) (i : Fin 3) (a : Triple) (b : Bool) :
    g.namedAccepts o (g.name o i) a b ↔ g.accepts o i a b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Triple
structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.FullPoint line 256
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.FullPoint.valid line 260
structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.PartnerPoint line 265
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.AugmentedAccepts line 270
Source comment
Only the single positions matter to the extracted incidence game.
```
def AugmentedAccepts {Position Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active : Position → Prop) (slot : Position → Fin 3)
    (eA : FullPoint Position) (eB : PartnerPoint Position) : Prop :=
…
```
Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.FullPoint, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.PartnerPoint
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.RepeatedAccepts line 277
theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.augmented_accepts_implies_repeated_accepts line 285
Source documentation
Acceptance of the augmented projection game implies acceptance of every incidence coordinate in any subset of the active positions.
```
theorem augmented_accepts_implies_repeated_accepts
    {Position Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active inside : Position → Prop) (slot : Position → Fin 3)
    (eA : FullPoint Position) (eB : PartnerPoint Position)
    (hinside : ∀ j, inside j → active j)
    (haccept : AugmentedAccepts g u active slot eA eB) :
    RepeatedAccepts g u slot inside eA.coords eB.single := by
…
```
Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.FullPoint, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.PartnerPoint, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.AugmentedAccepts, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.RepeatedAccepts

theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.augmented_accepts_implies_named_repeated_accepts line 302

Source documentation

The same containment stated on the occurrence/name question vectors actually given to the two repeated-game players.

theorem augmented_accepts_implies_named_repeated_accepts
    {Position RepeatPosition Occurrence Name : Type}
    (g : Incidence Occurrence Name) (u : Position → Occurrence)
    (active : Position → Prop) (slot : Position → Fin 3)
    (embed : RepeatPosition → Position)
    (eA : FullPoint Position) (eB : PartnerPoint Position)
    (hinside : ∀ r, active (embed r))
    (haccept : AugmentedAccepts g u active slot eA eB) :
    ∀ r, g.namedAccepts (u (embed r))
      (g.name (u (embed r)) (slot (embed r)))
      (eA.coords (embed r)) (eB.single (embed r)) := by
…

Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.FullPoint, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.PartnerPoint, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.AugmentedAccepts

structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Game line 328
structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Strategies line 331
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Strategies.wins line 335
structure OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation line 339
def OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation.induced line 351
theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation.induced_wins line 363
Source documentation
A local simulation transports every deterministic strategy and contains its winning event pointwise. No shared access to the questions is used.
```
theorem LocalSimulation.induced_wins
    {InnerQA InnerQB InnerA InnerB OuterQA OuterQB OuterA OuterB : Type}
    {inner : Game InnerQA InnerQB InnerA InnerB}
    {outer : Game OuterQA OuterQB OuterA OuterB}
    (r : LocalSimulation inner outer)
    (s : Strategies OuterQA OuterQB OuterA OuterB)
    (qa : InnerQA) (qb : InnerQB)
    (hwins : s.wins outer (r.questionA qa) (r.questionB qb)) :
    (r.induced s).wins inner qa qb :=
…
```
Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Game, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Strategies

theorem OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation.seeded_induced_wins line 376

Source documentation

Fixing strategy randomness gives another local deterministic strategy; the simulation proof applies to every seed, before any averaging.

theorem LocalSimulation.seeded_induced_wins
    {InnerQA InnerQB InnerA InnerB OuterQA OuterQB OuterA OuterB Seed : Type}
    {inner : Game InnerQA InnerQB InnerA InnerB}
    {outer : Game OuterQA OuterQB OuterA OuterB}
    (r : LocalSimulation inner outer)
    (strategy : Seed → Strategies OuterQA OuterQB OuterA OuterB)
    (seed : Seed) (qa : InnerQA) (qb : InnerQB)
    (hwins : (strategy seed).wins outer (r.questionA qa) (r.questionB qb)) :
    (r.induced (strategy seed)).wins inner qa qb :=
…

Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Game, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.LocalSimulation, OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Strategies