The k-fold tailored product of a tailored game

Paper II, §6.3 (II:11377–11396), in its direct form: the k-fold product of a tailored game G is the tailored game G.repeat k on k-tuples of questions, with

• the product distribution ∏ᵢ μ(xᵢ, yᵢ);
• the variables at x⃗ the disjoint union of the variables at the coordinates, the readable ones first, as a tailored answer must have them: the readable variables of x₁, …, x_k, in this order, then their linear variables (varEquiv), so that lenR x⃗ = ∑ᵢ lenR xᵢ and lenL x⃗ = ∑ᵢ lenL xᵢ;
• the constraints at (x⃗, y⃗) those of every coordinate, each written over all the variables by padding it with zeros (padCons): the paper's "zero-padded to the global length and concatenated" (II:11380). A constraint of the wrong length becomes the rejecting constraint, as the canonical decider rejects it in the coordinate.

repeat_accepts_iff is the acceptance law: the canonical decider accepts a pair of answers exactly when they have the right lengths and every coordinate, read off by coord, is accepted. It rests on satisfies_padCons_iff, the padded constraint being satisfied by the whole answers exactly when the constraint is satisfied by the coordinate's.

The variables of a tuple of questions

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredGame.lenRSum {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : ℕ

The readable variables of the coordinates, in order.

Equations

• G.lenRSum x = ∑ i : Fin k, G.lenR (x i)

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredGame.lenLSum {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : ℕ

The linear variables of the coordinates, in order.

Equations

• G.lenLSum x = ∑ i : Fin k, G.lenL (x i)

def MIPRE.Tailored.TailoredGame.varEquiv {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : Fin (G.lenRSum x + G.lenLSum x) ≃ (i : Fin k) × Fin (G.len (x i))

The variables at x⃗: the readable variables of the coordinates, then their linear variables, matched with the pairs (i, v) of a coordinate and a variable v of the question xᵢ (readable v < lenR xᵢ first, as in G).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.TailoredGame.varEquiv_symm_castAdd {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) (v : Fin (G.lenR (x i))) : (G.varEquiv x).symm ⟨i, Fin.castAdd (G.lenL (x i)) v⟩ = Fin.castAdd (G.lenLSum x) (finSigmaFinEquiv ⟨i, v⟩)

The readable variable v of the coordinate i is the readable variable ∑_{j < i} lenR xⱼ + v of the tuple.

theorem MIPRE.Tailored.TailoredGame.varEquiv_symm_natAdd {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) (w : Fin (G.lenL (x i))) : (G.varEquiv x).symm ⟨i, Fin.natAdd (G.lenR (x i)) w⟩ = Fin.natAdd (G.lenRSum x) (finSigmaFinEquiv ⟨i, w⟩)

The linear variable w of the coordinate i is the linear variable ∑_{j < i} lenL xⱼ + w of the tuple, after all the readable ones.

theorem MIPRE.Tailored.TailoredGame.lt_lenRSum_iff {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (g : Fin (G.lenRSum x + G.lenLSum x)) : ↑g < G.lenRSum x ↔ ↑((G.varEquiv x) g).snd < G.lenR (x ((G.varEquiv x) g).fst)

Readable variables correspond: a variable of the tuple is readable exactly when it is a readable variable of its coordinate.

Coordinates of answers

def MIPRE.Tailored.TailoredGame.coord {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (a : Cost.BitStr) (i : Fin k) : Cost.BitStr

The answer to the coordinate i read off an answer a to the tuple x⃗.

Equations

• G.coord x a i = List.ofFn fun (v : Fin (G.len (x i))) => List.getD a (↑((G.varEquiv x).symm ⟨i, v⟩)) false

@[simp]

theorem MIPRE.Tailored.TailoredGame.length_coord {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (a : Cost.BitStr) (i : Fin k) : List.length (G.coord x a i) = G.len (x i)

def MIPRE.Tailored.TailoredGame.preR {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : ℕ

The readable variables of the coordinates before i.

Equations

• G.preR x i = ∑ j : Fin k with j < i, G.lenR (x j)

def MIPRE.Tailored.TailoredGame.preL {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : ℕ

The linear variables of the coordinates before i.

Equations

• G.preL x i = ∑ j : Fin k with j < i, G.lenL (x j)

def MIPRE.Tailored.TailoredGame.sufR {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : ℕ

The readable variables of the coordinates after i.

Equations

• G.sufR x i = G.lenRSum x - (G.preR x i + G.lenR (x i))

def MIPRE.Tailored.TailoredGame.sufL {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : ℕ

The linear variables of the coordinates after i.

Equations

• G.sufL x i = G.lenLSum x - (G.preL x i + G.lenL (x i))

theorem MIPRE.Tailored.TailoredGame.sum_castLE_eq_sum_filter {k : ℕ} (f : Fin k → ℕ) (i : Fin k) : ∑ j : Fin ↑i, f (Fin.castLE ⋯ j) = ∑ j : Fin k with j < i, f j

A sum over the coordinates before i, written over Fin i.

theorem MIPRE.Tailored.TailoredGame.val_finSigmaFinEquiv_R {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) (v : Fin (G.lenR (x i))) : ↑(finSigmaFinEquiv ⟨i, v⟩) = G.preR x i + ↑v

The position of a readable variable of the coordinate i among the readable variables.

theorem MIPRE.Tailored.TailoredGame.val_finSigmaFinEquiv_L {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) (w : Fin (G.lenL (x i))) : ↑(finSigmaFinEquiv ⟨i, w⟩) = G.preL x i + ↑w

The position of a linear variable of the coordinate i among the linear variables.

theorem MIPRE.Tailored.TailoredGame.preR_add_le {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : G.preR x i + G.lenR (x i) ≤ G.lenRSum x

theorem MIPRE.Tailored.TailoredGame.preL_add_le {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (i : Fin k) : G.preL x i + G.lenL (x i) ≤ G.lenLSum x

theorem MIPRE.Tailored.TailoredGame.coord_eq {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) {a : Cost.BitStr} (ha : List.length a = G.lenRSum x + G.lenLSum x) (i : Fin k) : G.coord x a i = List.take (G.lenR (x i)) (List.drop (G.preR x i) a) ++ List.take (G.lenL (x i)) (List.drop (G.lenRSum x + G.preL x i) a)

A coordinate of an answer is two blocks of it: its readable answers, at the coordinate's place among the readable variables, then its linear answers, at its place among the linear ones.

def MIPRE.Tailored.TailoredGame.coordR {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) (aR : Cost.BitStr) (i : Fin k) : Cost.BitStr

The readable answer to the coordinate i read off the readable part a^R of an answer: its block of lenR xᵢ bits after the readable variables of the coordinates before it.

Equations

• G.coordR x aR i = List.take (G.lenR (x i)) (List.drop (G.preR x i) aR)

theorem MIPRE.Tailored.TailoredGame.coordR_take {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) {a : Cost.BitStr} (ha : List.length a = G.lenRSum x + G.lenLSum x) (i : Fin k) : G.coordR x (List.take (G.lenRSum x) a) i = List.take (G.lenR (x i)) (G.coord x a i)

The readable part of a coordinate of an answer is the coordinate of its readable part.

Padding a constraint of a coordinate

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredGame.zeros (n : ℕ) : Cost.BitStr

n zero bits.

Equations

• MIPRE.Tailored.TailoredGame.zeros n = List.replicate n false

def MIPRE.Tailored.TailoredGame.padCons {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x y : Fin k → X) (i : Fin k) (c : Cost.BitStr) : Cost.BitStr

A constraint of the coordinate i, written over all the variables (II:11380): its blocks of coefficients — readable at xᵢ, linear at xᵢ, readable at yᵢ, linear at yᵢ, affine — each put at its coordinate's place among the variables of its kind, and zeros everywhere else. The blocks are cut with take and drop, so that they partition the constraint whatever its length: a constraint of the wrong length gives a padded vector of the wrong length, which the canonical decider rejects, as it rejects the constraint in its coordinate.

Equations

• One or more equations did not get rendered due to their size.

The product game

def MIPRE.Tailored.TailoredGame.repeat {X : Type u_1} [Fintype X] (G : TailoredGame X) (k : ℕ) : TailoredGame (Fin k → X)

The k-fold tailored product (II:11377): product distribution, the variables of the coordinates (readable first), and every coordinate's constraints padded to all the variables.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Tailored.TailoredGame.repeat_μ {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x y : Fin k → X) : (G.repeat k).μ x y = ∏ i : Fin k, G.μ (x i) (y i)

@[simp]

theorem MIPRE.Tailored.TailoredGame.repeat_lenR {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : (G.repeat k).lenR x = G.lenRSum x

@[simp]

theorem MIPRE.Tailored.TailoredGame.repeat_lenL {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : (G.repeat k).lenL x = G.lenLSum x

theorem MIPRE.Tailored.TailoredGame.repeat_len {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x : Fin k → X) : (G.repeat k).len x = G.lenRSum x + G.lenLSum x

Linear constraints after padding

theorem MIPRE.Tailored.TailoredGame.count_zipWith_append {p₁ p₂ v₁ v₂ : Cost.BitStr} (h : List.length p₁ = List.length v₁) : List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) (p₁ ++ p₂) (v₁ ++ v₂)) = List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) p₁ v₁) + List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) p₂ v₂)

The number of coincident ones of two concatenations, the first blocks of equal lengths, is the sum over the blocks.

@[simp]

theorem MIPRE.Tailored.TailoredGame.count_zipWith_zeros (n : ℕ) (m : Cost.BitStr) : List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) (zeros n) m) = 0

theorem MIPRE.Tailored.TailoredGame.eq_flatten_six (a : Cost.BitStr) (p₁ p₂ p₃ p₄ p₅ : ℕ) : a = [List.take p₁ a, List.take p₂ (List.drop p₁ a), List.take p₃ (List.drop (p₁ + p₂) a), List.take p₄ (List.drop (p₁ + p₂ + p₃) a), List.take p₅ (List.drop (p₁ + p₂ + p₃ + p₄) a), List.drop (p₁ + p₂ + p₃ + p₄ + p₅) a].flatten

A list is the concatenation of six consecutive blocks of it.

theorem MIPRE.Tailored.TailoredGame.eq_flatten_five (c : Cost.BitStr) (p₁ p₂ p₃ p₄ : ℕ) : c = [List.take p₁ c, List.take p₂ (List.drop p₁ c), List.take p₃ (List.drop (p₁ + p₂) c), List.take p₄ (List.drop (p₁ + p₂ + p₃) c), List.drop (p₁ + p₂ + p₃ + p₄) c].flatten

A list is the concatenation of five consecutive blocks of it.

theorem MIPRE.Tailored.TailoredGame.satisfies_pad_blocks (c a₁ a₂ a₃ a₄ a₅ a₆ b₁ b₂ b₃ b₄ b₅ b₆ : Cost.BitStr) {n₁ n₂ n₃ n₄ n₅ n₆ m₁ m₂ m₃ m₄ m₅ m₆ : ℕ} (h₁ : List.length a₁ = n₁) (h₂ : List.length a₂ = n₂) (h₃ : List.length a₃ = n₃) (h₄ : List.length a₄ = n₄) (h₅ : List.length a₅ = n₅) (h₆ : List.length a₆ = n₆) (g₁ : List.length b₁ = m₁) (g₂ : List.length b₂ = m₂) (g₃ : List.length b₃ = m₃) (g₄ : List.length b₄ = m₄) (g₅ : List.length b₅ = m₅) (g₆ : List.length b₆ = m₆) : Satisfies (zeros n₁ ++ List.take n₂ c ++ zeros n₃ ++ zeros n₄ ++ List.take n₅ (List.drop n₂ c) ++ zeros n₆ ++ zeros m₁ ++ List.take m₂ (List.drop (n₂ + n₅) c) ++ zeros m₃ ++ zeros m₄ ++ List.take m₅ (List.drop (n₂ + n₅ + m₂) c) ++ zeros m₆ ++ List.drop (n₂ + n₅ + m₂ + m₅) c) (a₁ ++ a₂ ++ a₃ ++ a₄ ++ a₅ ++ a₆ ++ (b₁ ++ b₂ ++ b₃ ++ b₄ ++ b₅ ++ b₆) ++ [true]) ↔ Satisfies c (a₂ ++ a₅ ++ (b₂ ++ b₅) ++ [true])

The padding lemma on blocks: a constraint cut into the blocks of two answers, with zeros against every other block, is satisfied exactly when the constraint is satisfied by the blocks it was cut against.

theorem MIPRE.Tailored.TailoredGame.satisfies_padCons_iff {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x y : Fin k → X) (i : Fin k) (c : Cost.BitStr) {a b : Cost.BitStr} (ha : List.length a = G.lenRSum x + G.lenLSum x) (hb : List.length b = G.lenRSum y + G.lenLSum y) : Satisfies (G.padCons x y i c) (a ++ b ++ [true]) ↔ Satisfies c (G.coord x a i ++ G.coord y b i ++ [true])

The padded constraint is satisfied by the whole answers exactly when the constraint is satisfied by the coordinate's answers.

theorem MIPRE.Tailored.TailoredGame.repeat_accepts_iff {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} (x y : Fin k → X) (a b : Cost.BitStr) : (G.repeat k).Accepts x y a b ↔ List.length a = (G.repeat k).len x ∧ List.length b = (G.repeat k).len y ∧ ∀ (i : Fin k), G.Accepts (x i) (y i) (G.coord x a i) (G.coord y b i)

The acceptance law of the product: the canonical decider accepts a pair of answers to (x⃗, y⃗) exactly when they have the right lengths and every coordinate is accepted.