The repetition bound in the form the pipeline consumes

The soundness half of thm:parallel-repetition at the level of games. The vendored theorem MIPRE.Repetition.quantumValue_repeat_le (thm:direct-repetition-q) bounds val*(G^{⊗k}) by exp(-c ε^{13} k / (ε + log(|𝒜||ℬ|))) with ε = 1 - val*(G). The structure MIPRE.Repetition asks for exp(-c' ε^{13} k / (B + 1)) for answer alphabets of strings of length at most B (Verifier.Answers B) and a hypothesis val*(G) ≤ 1 - ε that need not be tight:

• |Answers B| ≤ 3^{B+1} (card_answers_le, by Answers.getElem?_injective), so log(|𝒜||ℬ|) ≤ 2(B + 1) log 3, and ε ≤ 1 ≤ B + 1, so the denominator is at most (B + 1)(1 + 2 log 3); c' = c / (1 + 2 log 3) (repConst).
• The exponent is monotone in the gap, so 1 - val*(G) ≥ ε suffices.

quantumValue_repeat_le_soundBound is the statement the assembly of Repetition ℓ uses.

noncomputable def MIPRE.Repetition.repConst₀ : ℝ

The universal constant of thm:direct-repetition-q.

Equations

• MIPRE.Repetition.repConst₀ = MIPRE.Repetition.quantumValue_repeat_le.choose

theorem MIPRE.Repetition.repConst₀_pos : 0 < repConst₀

theorem MIPRE.Repetition.quantumValue_repeat_le_spec (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hA : Nonempty A) (hB : Nonempty B) (hε : 0 < 1 - quantumValue G) (n : ℕ) (hn : 0 < n) : quantumValue (G.repeat n) ≤ Real.exp (-(repConst₀ * ((1 - quantumValue G) ^ 13 / (1 - quantumValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

noncomputable def MIPRE.Repetition.repConst : ℝ

The constant of the repetition bound for answers of bounded length: c / (1 + 2 log 3).

Equations

• MIPRE.Repetition.repConst = MIPRE.Repetition.repConst₀ / (1 + 2 * Real.log 3)

theorem MIPRE.Repetition.one_add_two_log_three_pos : 0 < 1 + 2 * Real.log 3

theorem MIPRE.Repetition.repConst_pos : 0 < repConst

theorem MIPRE.Repetition.card_answers_le (T : ℕ) : Fintype.card (Verifier.Answers T) ≤ 3 ^ (T + 1)

|Answers T| ≤ 3^{T + 1}.

theorem MIPRE.Repetition.log_card_answers_mul_le (T : ℕ) : Real.log (↑(Fintype.card (Verifier.Answers T)) * ↑(Fintype.card (Verifier.Answers T))) ≤ 2 * (↑T + 1) * Real.log 3

theorem MIPRE.Repetition.exp_le_soundBound {c₀ ε ε' : ℝ} (hc₀ : 0 < c₀) (hε : 0 < ε) (hεε' : ε ≤ ε') (hε'1 : ε' ≤ 1) {p : ℕ} (hp : ε ^ 13 ≤ ε' ^ p) (B k : ℕ) : Real.exp (-(c₀ * (ε' ^ p / (ε' + Real.log (↑(Fintype.card (Verifier.Answers B)) * ↑(Fintype.card (Verifier.Answers B)))))) * ↑k) ≤ soundBound (c₀ / (1 + 2 * Real.log 3)) ε k B

The arithmetic of both repetition bounds. For answers of length at most B, a gap ε' ∈ [ε, 1] and ε^13 ≤ ε'^p, the bound exp(-c₀ (ε'^p / (ε' + log(|𝒜||ℬ|))) k) of a direct repetition theorem is at most soundBound (c₀ / (1 + 2 log 3)) ε k B: the denominator is at most (B + 1)(1 + 2 log 3) (log_card_answers_mul_le). The tensor-product theorem has p = 13; the commuting-operator one has p = 7, and ε^13 ≤ ε^7 for ε ≤ 1.

theorem MIPRE.Repetition.quantumValue_repeat_le_soundBound {X : Type} [Fintype X] {B : ℕ} (G : Game X X (Verifier.Answers B) (Verifier.Answers B)) {ε : ℝ} (hε : 0 < ε) (hG : quantumValue G ≤ 1 - ε) {k : ℕ} (hk : 0 < k) : quantumValue (G.repeat k) ≤ soundBound repConst ε k B

Game-level soundness of direct repetition, in the form of Repetition.soundness: for a game with answers of length at most B, val*(G) ≤ 1 - ε gives val*(G^{⊗k}) ≤ exp(-c' ε^{13} k / (B + 1)).

def MIPRE.Repetition.GameSoundIn (ω : ValueModel) (c : ℝ) : Prop

The direct repetition bound in a value model, at the constant c: for every game on a nonempty question set with answers of length at most B, ω(G) ≤ 1 - ε gives ω(G^{⊗k}) ≤ exp(-c ε^13 k / (B + 1)) for every k ≥ 1. The verifier-level soundness of parallel repetition in ω is this and nothing else (MIPRE.val_repVerifier_le). The tensor-product model has it at repConst (gameSoundIn_tensor), the commuting-operator model at repConstCo (gameSoundIn_commuting, in VerifierCo.lean).

Equations

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

theorem MIPRE.Repetition.GameSoundIn.mono {ω : ValueModel} {c c' : ℝ} (h : GameSoundIn ω c') (hc : c ≤ c') : GameSoundIn ω c

The direct repetition bound survives lowering the constant.

theorem MIPRE.Repetition.gameSoundIn_tensor : GameSoundIn ValueModel.tensor repConst

The tensor-product model has the direct repetition bound at repConst.