OAI/Computability/UniqueGames/Games/CompletedSamplingLemmas.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.mixture_pushforward_base line 31
2. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.product_pushforward_eq_mixture_right line 38
3. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.product_product_pushforward_eq_mixture line 55
4. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.mixture_totalVariation_le line 67
5. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw line 81
6. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw_eq_pushforward line 85
7. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw_mixture line 99
8. abbrev OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.Seed line 113

   Source documentation

   The independent original seed and two full local completion tables.

   abbrev Seed (Γ X Y S U V : Type*) :=
   …

9. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.seedLaw line 116
10. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.left line 121
11. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.right line 124
12. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.completionKernel line 127
13. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw line 133

    Source documentation

    This is the shared-seed mixture used by Game.localEmbeddingLaw.

    def outputLaw (μ : FiniteDistribution (X × Y)) (γ : FiniteDistribution Γ)
        (sL : Γ → X → S) (sR : Γ → Y → S)
        (L : X × S → FiniteDistribution U) (R : Y × S → FiniteDistribution V) :
        FiniteDistribution (U × V) :=
    …

14. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw_eq_product_pushforward line 140
15. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw_eq_mixture line 152

    Source documentation

    The completion mixture is derived from actual local table reads.

    theorem outputLaw_eq_mixture
        (μ : FiniteDistribution (X × Y)) (γ : FiniteDistribution Γ)
        (sL : Γ → X → S) (sR : Γ → Y → S)
        (L : X × S → FiniteDistribution U) (R : Y × S → FiniteDistribution V) :
        outputLaw μ γ sL sR L R =
          (sharedOutputLaw μ γ sL sR).mixture (completionKernel L R) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.sharedOutputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.completionKernel

16. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw_completion_mixture line 181

    Source documentation

    The diagonal target uses the same selected label for both completion rows.

    theorem diagonalLaw_completion_mixture
        (σ : FiniteDistribution ((X × Y) × S))
        (L : X × S → FiniteDistribution U) (R : Y × S → FiniteDistribution V) :
        (diagonalLaw σ).mixture (completionKernel L R) =
          σ.mixture (fun z => (L (z.1.1, z.2)).product (R (z.1.2, z.2))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.completionKernel

17. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw_totalVariation_le line 189

    Source documentation

    Completing local outputs incurs no additional total-variation loss.

    theorem outputLaw_totalVariation_le
        (μ : FiniteDistribution (X × Y)) (γ : FiniteDistribution Γ)
        (sL : Γ → X → S) (sR : Γ → Y → S)
        (L : X × S → FiniteDistribution U) (R : Y × S → FiniteDistribution V)
        (σ : FiniteDistribution ((X × Y) × S)) :
        (outputLaw μ γ sL sR L R).totalVariation
            (σ.mixture (fun z => (L (z.1.1, z.2)).product (R (z.1.2, z.2)))) ≤
          (sharedOutputLaw μ γ sL sR).totalVariation (diagonalLaw σ) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.outputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.sharedOutputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.diagonalLaw

18. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateLeft line 209

    Source documentation

    Restore the left input coordinate even on completion tables of weight zero.

    def coordinateLeft (j : I) (sL : Γ → X → S)
        (seed : Seed Γ X Y S (I → X) (I → Y)) (x : X) : I → X :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.Seed

19. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateRight line 214

    Source documentation

    Restore the right input coordinate even on completion tables of weight zero.

    def coordinateRight (j : I) (sR : Γ → Y → S)
        (seed : Seed Γ X Y S (I → X) (I → Y)) (y : Y) : I → Y :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.Seed

20. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 220
21. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 227
22. def OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 232
23. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 241

    Source documentation

    Supported coordinate repair preserves the exact completion mixture.

    theorem coordinateOutputLaw_eq_mixture
        (μ : FiniteDistribution (X × Y)) (γ : FiniteDistribution Γ)
        (j : I) (sL : Γ → X → S) (sR : Γ → Y → S)
        (L : X × S → FiniteDistribution (I → X))
        (R : Y × S → FiniteDistribution (I → Y))
        (hL : ∀ q xs, (L q).weight xs ≠ 0 → xs j = q.1)
        (hR : ∀ q ys, (R q).weight ys ≠ 0 → ys j = q.1) :
        coordinateOutputLaw μ γ j sL sR L R =
          (sharedOutputLaw μ γ sL sR).mixture (completionKernel L R) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateOutputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.sharedOutputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.completionKernel

24. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 276
25. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 286
26. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.coordinate_probability_le_value_of_local_completion line 321
27. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.finiteDistribution_nonempty line 390
28. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedProfileFallback line 400
29. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftProfile line 408
30. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightProfile line 421
31. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftProfileError line 434
32. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightProfileError line 441
33. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftProfileError_le line 448
34. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightProfileError_le line 462
35. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSamplingTarget line 476
36. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSamplingTarget_left_error line 484
37. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSamplingTarget_right_error line 497
38. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionRadius_le_informationRadius line 526
39. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal_error_sum line 542
40. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedEmbeddingError line 552
41. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedEmbeddingError_nonnegative line 559
42. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftProfileError_sum line 568
43. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightProfileError_sum line 586
44. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedEmbeddingError_sum_le_fifteen line 604
45. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_coordinate_probability_le_value_add_error line 637
46. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.holenstein_conditionalCoordinateBound line 666
47. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.holenstein_repetition_success line 682

    Source documentation

    Holenstein's explicit constant-6000 repetition estimate, for the actual success probability of every finite deterministic repeated strategy.

    theorem holenstein_repetition_success
        (G : Game Q₁ Q₂ A₁ A₂) (n : Nat)
        (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
        {v ell : ℝ} (hvalue : G.value ≤ v) (hv : v < 1) (hell : 1 ≤ ell)
        (halphabet : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
        (G.repetition n).success strategy ≤
          (1 - (1 - v)^3 / 6000)^((n : ℝ) / ell) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo

48. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.holenstein_repetition_value line 694

    Source documentation

    Quantitative parallel repetition of the actual maximum game value. There is no repetition, embedding, information-budget, or independence premise.

    theorem holenstein_repetition_value
        (G : Game Q₁ Q₂ A₁ A₂) (n : Nat)
        {v ell : ℝ} (hvalue : G.value ≤ v) (hv : v < 1) (hell : 1 ≤ ell)
        (halphabet : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
        (G.repetition n).value ≤
          (1 - (1 - v)^3 / 6000)^((n : ℝ) / ell) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo