OAI/Computability/UniqueGames/Foundations/KernelSampling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact sampling of two conditional kernels from one finite weighted shared seed. The seed consists of independent full response tables and is independent of the questions. Supported-coordinate repairs preserve the sampled laws and enforce the designated coordinate even on seeds of weight zero. The seed is not claimed to be uniform: the kernel weights may be arbitrary real numbers.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 22
  2. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.product_pushforward line 38

    Source documentation

    Applying separate maps to independent samples preserves their independence.

    theorem product_pushforward
    {Ω Γ A B : Type*} [Fintype Ω] [Fintype Γ] [Fintype A] [Fintype B]
    (μ : FiniteDistribution Ω) (ν : FiniteDistribution Γ)
    (f : Ω → A) (g : Γ → B) :
    (μ.product ν).pushforward (fun z => (f z.1, g z.2)) =
      (μ.pushforward f).product (ν.pushforward g) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.product

  3. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 56

    Source documentation

    A full response table of nonzero weight uses a supported answer in every row.

    theorem table_row_weight_ne_zero
    {Q A : Type*} [Fintype Q] [Fintype A] [DecidableEq Q]
    (responses : Q → FiniteDistribution A) (answers : Q → A)
    (h : (table responses).weight answers ≠ 0) (q : Q) :
    (responses q).weight (answers q) ≠ 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table

  4. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table_repair_pushforward line 67

    Source documentation

    Repairing table entries only off each row's support leaves its exact law intact.

    theorem table_repair_pushforward
    {Q A : Type*} [Fintype Q] [Fintype A] [DecidableEq Q]
    (responses : Q → FiniteDistribution A) (repair : Q → A → A)
    (hrepair : ∀ q a, (responses q).weight a ≠ 0 → repair q a = a) (q : Q) :
    (table responses).pushforward (fun answers => repair q (answers q)) =
      responses q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table, OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward

  5. abbrev OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.Seed line 85

    Source documentation

    A single seed supplies a full local table to each side.

    abbrev Seed (Q₁ Q₂ A B : Type*) := (Q₁ → A) × (Q₂ → B)
  6. def OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readLeft line 87
  7. def OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readRight line 88
  8. def OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.seedLaw line 91

    Source documentation

    The fixed weighted seed law; it does not depend on the sampled questions.

    def seedLaw {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B) :
    FiniteDistribution (Seed Q₁ Q₂ A B) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.Seed

  9. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.read_joint_pushforward line 99

    Source documentation

    The two reads have exactly the product of the requested conditional laws.

    theorem read_joint_pushforward {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B)
    (x : Q₁) (y : Q₂) :
    (seedLaw left right).pushforward (fun seed => (readLeft seed x, readRight seed y)) =
      (left x).product (right y) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.seedLaw, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readLeft, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readRight

  10. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.repaired_joint_pushforward line 113

    Source documentation

    Separate supported repairs retain the exact joint product law.

    theorem repaired_joint_pushforward {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B)
    (repairLeft : Q₁ → A → A) (repairRight : Q₂ → B → B)
    (hleft : ∀ x a, (left x).weight a ≠ 0 → repairLeft x a = a)
    (hright : ∀ y b, (right y).weight b ≠ 0 → repairRight y b = b)
    (x : Q₁) (y : Q₂) :
    (seedLaw left right).pushforward (fun seed =>
      (repairLeft x (readLeft seed x), repairRight y (readRight seed y))) =
      (left x).product (right y) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.seedLaw, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readLeft, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.readRight

  11. def OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedLeft line 136

    Source documentation

    Restore the designated coordinate on every left table read.

    def completedLeft (j : I)
    (seed : Seed (A × S) (B × S) (I → A) (I → B)) (q : A × S) : I → A :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.Seed

  12. def OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedRight line 141

    Source documentation

    Restore the designated coordinate on every right table read.

    def completedRight (j : I)
    (seed : Seed (A × S) (B × S) (I → A) (I → B)) (q : B × S) : I → B :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.Seed

  13. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedLeft_coordinate line 145
  14. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedRight_coordinate line 149
  15. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.update_eq_of_coordinate line 153
  16. theorem OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completed_joint_pushforward line 161

    Source documentation

    Exact conditional completion from a finite weighted shared seed. The reads always restore the specified coordinates, including on seeds of weight zero; the support hypotheses ensure that this repair preserves the requested laws.

    theorem completed_joint_pushforward
    [Fintype I] [Fintype A] [Fintype B] [Fintype S]
    [DecidableEq A] [DecidableEq B] [DecidableEq S]
    (left : (A × S) → FiniteDistribution (I → A))
    (right : (B × S) → FiniteDistribution (I → B)) (j : I)
    (hleft : ∀ q xs, (left q).weight xs ≠ 0 → xs j = q.1)
    (hright : ∀ q ys, (right q).weight ys ≠ 0 → ys j = q.1)
    (x : A × S) (y : B × S) :
    (seedLaw left right).pushforward
        (fun seed => (completedLeft j seed x, completedRight j seed y)) =
      (left x).product (right y) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.seedLaw, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedLeft, OAI.UniqueGamesTheorem.Foundations.Games.KernelSampling.completedRight