OAI/Computability/MaxCut/PCP/CompletedSampling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.mixture_pushforward_base line 27
2. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.product_pushforward_eq_mixture_right line 34
3. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.product_product_pushforward_eq_mixture line 51
4. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.mixture_totalVariation_le line 63
5. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw line 77
6. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_eq_pushforward line 81
7. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_mixture line 95
8. abbrev OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.Seed line 109

   Source documentation

   The independent original seed and two full local completion tables.

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

9. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.seedLaw line 112
10. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.left line 117
11. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.right line 120
12. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.completionKernel line 123
13. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw line 129

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_product_pushforward line 136
15. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_mixture line 148

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw, OAI.MaxCutGames.Foundations.Repetition.sharedOutputLaw, OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.completionKernel

16. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_completion_mixture line 177

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw, OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.completionKernel

17. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw_totalVariation_le line 185

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.outputLaw, OAI.MaxCutGames.Foundations.Repetition.sharedOutputLaw, OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.diagonalLaw

18. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateLeft line 203

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.Seed

19. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateRight line 208

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.Seed

20. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 214
21. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 221
22. def OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 226
23. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 235

    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.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw, OAI.MaxCutGames.Foundations.Repetition.sharedOutputLaw, OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.completionKernel

24. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 270
25. theorem OAI.MaxCutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 280
26. def OAI.MaxCutGames.Foundations.Games.Game.localEmbeddingLaw line 315
27. theorem OAI.MaxCutGames.Foundations.Games.Game.success_le_value_add_embedding_distance line 325

    Source documentation

    Any finite shared-randomness local embedding yields a valid base-game strategy after the seed is fixed. Total variation pays exactly for changing the resulting question distribution to the desired one.

    theorem success_le_value_add_embedding_distance
        (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
        (seedLaw : FiniteDistribution Seed)
        (left : Seed → Q₁ → R₁) (right : Seed → Q₂ → R₂)
        (answerLeft : Seed → Q₁ → B₁ → A₁)
        (answerRight : Seed → Q₂ → B₂ → A₂)
        (acceptance : ∀ seed x y a b,
          H.accepts (left seed x) (right seed y) a b = true →
          G.accepts x y (answerLeft seed x a) (answerRight seed y b) = true)
        (strategy : Strategy R₁ R₂ B₁ B₂) :
        H.success strategy ≤ G.value +
          H.questions.totalVariation (G.localEmbeddingLaw seedLaw left right) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.Strategy

28. def OAI.MaxCutGames.Foundations.Games.Game.coordinateGame line 355

    Source documentation

    A single tested coordinate under an arbitrary full-tuple question law.

    def coordinateGame (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
        (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂))) :
        Game (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) where
    …

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.FiniteDistribution

29. theorem OAI.MaxCutGames.Foundations.Games.Game.coordinate_probability_le_value_add_embedding_distance line 364

    Source documentation

    The strategy-extraction step used for a surviving coordinate after conditioning on successes at other coordinates. It preserves full local question dependence and uses no independence assumption on the target law.

    theorem coordinate_probability_le_value_add_embedding_distance
        (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
        (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂)))
        (seedLaw : FiniteDistribution Seed)
        (left : Seed → Q₁ → Fin n → Q₁) (right : Seed → Q₂ → Fin n → Q₂)
        (left_preserves : ∀ seed x, left seed x coordinate = x)
        (right_preserves : ∀ seed y, right seed y coordinate = y)
        (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
        law.probability (G.coordinateWin strategy coordinate) ≤ G.value +
          law.totalVariation (G.localEmbeddingLaw seedLaw left right) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.Strategy

30. theorem OAI.MaxCutGames.Foundations.Games.Game.coordinate_probability_le_value_of_approximate_embeddings line 382

    Source documentation

    Finite samplers may have an arbitrarily small exhaustion error. Passing to the limit in the numerical bound does not require an infinite seed or a claim that any finite sampler terminates with probability one.

    theorem coordinate_probability_le_value_of_approximate_embeddings
        {SeedFamily : Nat → Type*} [∀ t, Fintype (SeedFamily t)]
        (G : Game Q₁ Q₂ A₁ A₂) {n : Nat} (coordinate : Fin n)
        (law : FiniteDistribution ((Fin n → Q₁) × (Fin n → Q₂)))
        (seedLaw : (t : Nat) → FiniteDistribution (SeedFamily t))
        (left : (t : Nat) → SeedFamily t → Q₁ → Fin n → Q₁)
        (right : (t : Nat) → SeedFamily t → Q₂ → Fin n → Q₂)
        (left_preserves : ∀ t seed x, left t seed x coordinate = x)
        (right_preserves : ∀ t seed y, right t seed y coordinate = y)
        (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
        (distance : ℝ)
        (close : ∀ η : ℝ, 0 < η → ∃ t,
    …

    Mentions: OAI.MaxCutGames.Foundations.Games.Game, OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.Strategy

31. theorem OAI.MaxCutGames.Foundations.Repetition.coordinate_probability_le_value_of_local_completion line 421