Quantum parallel repetition, part 12 #
theorem
QuantumParallelRepetition.unconditionalActualFairSourceRoundingData_exists_stoppedVerifier
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(alpha gamma : ℝ)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(gamma_positive : 0 < gamma)
(small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1)
(failure :
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2)
:
∃ (deviation : ℝ) (clipping : ℝ) (rounded : Strategy G),
deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) ∧ clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2) ∧ 1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 2 * √clipping) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_small
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(alpha gamma : ℝ)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(gamma_positive : 0 < gamma)
(small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1)
(failure :
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2)
:
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha
(martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.unconditionalSourceOneGameRounding_uniform :
∃ (K : ℝ),
1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
0 < (Finset.univ \ D).card →
0 < repeatedPostselectionMass G n S D →
∀ (alpha gamma : ℝ),
0 < alpha →
alpha ≤ 1 →
0 < gamma →
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 →
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D)
(exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.pdf_distributionUniformExponential_unconditional :
∃ (c : ℝ),
0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B),
Nonempty A →
Nonempty B →
0 < 1 - entangledValue G →
∀ (n : ℕ),
0 < n →
repeatedEntangledValue G n ≤ Real.exp
(-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)
theorem
QuantumParallelRepetition.distributionUniformExponential :
∃ (c : ℝ),
0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B),
Nonempty A →
Nonempty B →
0 < 1 - entangledValue G →
∀ (n : ℕ),
0 < n →
repeatedEntangledValue G n ≤ Real.exp
(-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)
A universal exponential upper bound for the repeated entangled value.