Games generated from finite uniform samples

Unlike SeededGame, the seed and the two question alphabets may differ. This is needed for typed games, whose seed is an edge and a common vector.

noncomputable def MIPRE.SampledGame.dist {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] (qA : S → X) (qB : S → Y) (x : X) (y : Y) : ℝ

Push forward the uniform law by the two question maps.

Equations

• MIPRE.SampledGame.dist qA qB x y = (↑(Fintype.card S))⁻¹ * ∑ s : S, if (qA s, qB s) = (x, y) then 1 else 0

theorem MIPRE.SampledGame.dist_eq_card {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] (qA : S → X) (qB : S → Y) (x : X) (y : Y) : dist qA qB x y = ↑{s : S | qA s = x ∧ qB s = y}.card / ↑(Fintype.card S)

The sample law is the normalized cardinality of each question pair's fibre.

theorem MIPRE.SampledGame.sum_dist_mul {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] (qA : S → X) (qB : S → Y) (f : X → Y → ℝ) : ∑ x : X, ∑ y : Y, dist qA qB x y * f x y = (∑ s : S, f (qA s) (qB s)) / ↑(Fintype.card S)

Averages over questions are averages over the common sample.

theorem MIPRE.SampledGame.dist_nonneg {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] (qA : S → X) (qB : S → Y) (x : X) (y : Y) : 0 ≤ dist qA qB x y

A uniform sample law is nonnegative.

theorem MIPRE.SampledGame.sum_dist {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] [Nonempty S] (qA : S → X) (qB : S → Y) : ∑ x : X, ∑ y : Y, dist qA qB x y = 1

A nonempty sample space gives a probability distribution.

noncomputable def MIPRE.SampledGame.game {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] [Nonempty S] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (qA : S → X) (qB : S → Y) (D : X → Y → A → B → Bool) : Game X Y A B

The finite game generated by the question maps and decision predicate.

Equations

• MIPRE.SampledGame.game qA qB D = { μ := MIPRE.SampledGame.dist qA qB, μ_nonneg := ⋯, μ_sum_one := ⋯, D := D }

theorem MIPRE.SampledGame.one_sub_value {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] [Nonempty S] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (qA : S → X) (qB : S → Y) (D : X → Y → A → B → Bool) (R : TensorProductStrategy (game qA qB D)) : 1 - R.value = (∑ s : S, R.failAt (qA s) (qB s)) / ↑(Fintype.card S)

The failure probability of a strategy is the uniform average of its conditional failures.