Quantum parallel repetition, part 04

@[reducible, inline]

abbrev QuantumParallelRepetition.SourceRemainingCoordinate {n : ℕ} (D : Finset (Fin n)) : Type

The type used to represent source remaining coordinate in the exact sampling construction.

Equations

• QuantumParallelRepetition.SourceRemainingCoordinate D = ↥(Finset.univ \ D)

theorem QuantumParallelRepetition.fin_sum_successive_sub {m : ℕ} (f : Fin (m + 1) → ℝ) : ∑ k : Fin m, (f k.succ - f k.castSucc) = f (Fin.last m) - f 0

def QuantumParallelRepetition.exactLeft {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : Finset M

The exact left construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactLeft coordinate partition = {j : M | j ≠ coordinate ∧ partition j = false}

def QuantumParallelRepetition.exactRight {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : Finset M

The exact right construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactRight coordinate partition = {j : M | j ≠ coordinate ∧ partition j = true}

theorem QuantumParallelRepetition.exactLeft_coordinate_not_mem {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : coordinate ∉ exactLeft coordinate partition

theorem QuantumParallelRepetition.exactRight_coordinate_not_mem {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : coordinate ∉ exactRight coordinate partition

structure QuantumParallelRepetition.ExactForwardSeed (M : Type u_1) [Fintype M] [DecidableEq M] : Type u_1

The coordinate, partition, orders, and cuts sampled by the exact forward process.

• coordinate : M

  The marked coordinate of the seed.

• partition : M → Bool

  The binary partition of coordinates carried by the seed.

• leftOrder : Equiv.Perm ↥(exactLeft self.coordinate self.partition)

  The ordering of coordinates on the left side of the partition.

• rightOrder : Equiv.Perm ↥(exactRight self.coordinate self.partition)

  The ordering of coordinates on the right side of the partition.

• leftCut : Fin ((exactLeft self.coordinate self.partition).card + 1)

  The reveal cut in the left-side ordering.

• rightCut : Fin ((exactRight self.coordinate self.partition).card + 1)

  The reveal cut in the right-side ordering.

@[instance_reducible]

instance QuantumParallelRepetition.instFintypeExactForwardSeed {M✝ : Type u_1} {inst✝ : Fintype M✝} {inst✝¹ : DecidableEq M✝} [Fintype M✝] : Fintype (ExactForwardSeed M✝)

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactRemainingSeed {n : ℕ} (D : Finset (Fin n)) : Type

The type used to represent exact remaining seed in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactRemainingSeed D = QuantumParallelRepetition.ExactForwardSeed (QuantumParallelRepetition.SourceRemainingCoordinate D)

noncomputable def QuantumParallelRepetition.exactLeftRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactLeft seed.coordinate seed.partition) ≃ Fin (exactLeft seed.coordinate seed.partition).card

The rank map for exact left.

Equations

• QuantumParallelRepetition.exactLeftRank seed = (Equiv.symm seed.leftOrder).trans (QuantumParallelRepetition.exactLeft seed.coordinate seed.partition).equivFin

noncomputable def QuantumParallelRepetition.exactRightRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactRight seed.coordinate seed.partition) ≃ Fin (exactRight seed.coordinate seed.partition).card

The rank map for exact right.

Equations

• QuantumParallelRepetition.exactRightRank seed = (Equiv.symm seed.rightOrder).trans (QuantumParallelRepetition.exactRight seed.coordinate seed.partition).equivFin

noncomputable def QuantumParallelRepetition.exactLeftPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : Finset M

The exact left prefix construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactRightPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : Finset M

The exact right prefix construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactLeftPrefix_subset {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactLeftPrefix seed ⊆ exactLeft seed.coordinate seed.partition

theorem QuantumParallelRepetition.exactRightPrefix_subset {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactRightPrefix seed ⊆ exactRight seed.coordinate seed.partition

noncomputable def QuantumParallelRepetition.exactSeedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ℝ

The probability weight for exact seed.

Equations

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

theorem QuantumParallelRepetition.exactSeedWeight_nonneg {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : 0 ≤ exactSeedWeight seed

theorem QuantumParallelRepetition.exactForwardSeed_sum {M : Type u_1} [Fintype M] [DecidableEq M] (f : ExactForwardSeed M → ℝ) : ∑ seed : ExactForwardSeed M, f seed = ∑ i : M, ∑ partition : M → Bool, ∑ leftOrder : Equiv.Perm ↥(exactLeft i partition), ∑ rightOrder : Equiv.Perm ↥(exactRight i partition), ∑ leftCut : Fin ((exactLeft i partition).card + 1), ∑ rightCut : Fin ((exactRight i partition).card + 1), f { coordinate := i, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder, leftCut := leftCut, rightCut := rightCut }

theorem QuantumParallelRepetition.exactUniform_sum {T : Type u_1} [Fintype T] (positive : 0 < Fintype.card T) : ∑ _t : T, 1 / ↑(Fintype.card T) = 1

theorem QuantumParallelRepetition.exactUniform_sum_mul {T : Type u_1} [Fintype T] (positive : 0 < Fintype.card T) (value : ℝ) : ∑ _t : T, value * (1 / ↑(Fintype.card T)) = value

theorem QuantumParallelRepetition.exactPrefixUniform_sum_mul (m : ℕ) (value : ℝ) : ∑ _k : Fin (m + 1), value * (1 / (↑m + 1)) = value

theorem QuantumParallelRepetition.exactPermutationUniform_sum_mul {T : Type u_1} [Fintype T] (value : ℝ) : ∑ _π : Equiv.Perm T, value * (1 / ↑(Fintype.card (Equiv.Perm T))) = value

theorem QuantumParallelRepetition.common_finite_purification_pair_jensen {ι : Type u_1} {κ : Type u_2} {d : Type u_3} [Fintype ι] [Fintype κ] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : κ → Matrix d d ℂ) (anchor : Matrix d d ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (a : ι), 0 ≤ weight a) (normalized : ∑ a : ι, weight a = 1) (mean : ∑ a : ι, weight a • F (choose a) = F meanIndex) : (∑ a : ι, weight a • cfc (fun (z : ℝ) => z * Real.log z) (F (choose a)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex) - ∑ a : ι, weight a • ((finitePurificationMatrix F anchor positive hanchor (choose a) - finitePurificationMatrix F anchor positive hanchor meanIndex).conjTranspose * (finitePurificationMatrix F anchor positive hanchor (choose a) - finitePurificationMatrix F anchor positive hanchor meanIndex))).PosSemidef

theorem QuantumParallelRepetition.commonFinitePurification_weighted_left_variation_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {ι : Type u_5} {κ : Type u_6} {eB : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [Fintype κ] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (weight : ι → ℝ) (F : κ → Matrix S.Alice S.Alice ℂ) (anchor : Matrix S.Alice S.Alice ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (a : ι), 0 ≤ weight a) (normalized : ∑ a : ι, weight a = 1) (mean : ∑ a : ι, weight a • F (choose a) = F meanIndex) (KB : Matrix eB S.Bob ℂ) : ∑ a : ι, weight a * ‖finiteLocalPurificationVector S (finitePurificationMatrix F anchor positive hanchor (choose a)) KB - finiteLocalPurificationVector S (finitePurificationMatrix F anchor positive hanchor meanIndex) KB‖ ^ 2 ≤ ((bornTracePairing S.state.matrix) (∑ a : ι, weight a • cfc (fun (z : ℝ) => z * Real.log z) (F (choose a)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex))) (KB.conjTranspose * KB)

theorem QuantumParallelRepetition.commonFinitePurification_weighted_right_variation_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {ι : Type u_5} {κ : Type u_6} {eA : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [Fintype κ] [Fintype eA] {G : Game X Y A B} (S : Strategy G) (weight : ι → ℝ) (F : κ → Matrix S.Bob S.Bob ℂ) (anchor : Matrix S.Bob S.Bob ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (b : ι), 0 ≤ weight b) (normalized : ∑ b : ι, weight b = 1) (mean : ∑ b : ι, weight b • F (choose b) = F meanIndex) (KA : Matrix eA S.Alice ℂ) : ∑ b : ι, weight b * ‖finiteLocalPurificationVector S KA (finitePurificationMatrix F anchor positive hanchor (choose b)) - finiteLocalPurificationVector S KA (finitePurificationMatrix F anchor positive hanchor meanIndex)‖ ^ 2 ≤ ((bornTracePairing S.state.matrix) (KA.conjTranspose * KA)) (∑ b : ι, weight b • cfc (fun (z : ℝ) => z * Real.log z) (F (choose b)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex))

theorem QuantumParallelRepetition.rectangular_matrix_quadratic_compression {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (K : Matrix e d ℂ) (E : Matrix e e ℂ) (z : EuclideanSpace ℂ d) : quadraticExpectation (Matrix.toEuclideanCLM E) (WithLp.toLp 2 (K.mulVec z.ofLp)) = quadraticExpectation (Matrix.toEuclideanCLM (K.conjTranspose * E * K)) z

theorem QuantumParallelRepetition.finiteLocalPurificationJointMatrix_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) (EA : Matrix eA eA ℂ) (EB : Matrix eB eB ℂ) : (finiteLocalPurificationJointMatrix S KA KB).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA 1) EB * finiteLocalPurificationJointMatrix S KA KB = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (KA.conjTranspose * EA * KA) 1) (KB.conjTranspose * EB * KB)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] [DecidableEq eA] [DecidableEq eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) (EA : Matrix eA eA ℂ) (EB : Matrix eB eB ℂ) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA 1) EB)) (finiteLocalPurificationVector S KA KB) = ((bornTracePairing S.state.matrix) (KA.conjTranspose * EA * KA)) (KB.conjTranspose * EB * KB)

noncomputable def QuantumParallelRepetition.conditionedAliceCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) (a : A) : Matrix S.Alice S.Alice ℂ

The measurement effect for conditioned alice coordinate.

Equations

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

noncomputable def QuantumParallelRepetition.conditionedBobCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) (b : B) : Matrix S.Bob S.Bob ℂ

The measurement effect for conditioned bob coordinate.

Equations

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

theorem QuantumParallelRepetition.conditionedAliceCoordinateEffect_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) (a : A) : (conditionedAliceCoordinateEffect G n S D α xs i a).PosSemidef

theorem QuantumParallelRepetition.conditionedBobCoordinateEffect_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) (b : B) : (conditionedBobCoordinateEffect G n S D β ys i b).PosSemidef

theorem QuantumParallelRepetition.conditionedAliceCoordinateEffect_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) : ∑ a : A, conditionedAliceCoordinateEffect G n S D α xs i a = conditionedAliceEffect G n S D α xs

theorem QuantumParallelRepetition.conditionedBobCoordinateEffect_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) : ∑ b : B, conditionedBobCoordinateEffect G n S D β ys i b = conditionedBobEffect G n S D β ys

structure QuantumParallelRepetition.ExactRevealHistory (X : Type u_5) (Y : Type u_6) [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Type (max u_5 u_6)

The exact conditioned transcript associated with a forward seed.

• aliceConditioned : ↥D → X

  Alice's questions on conditioned coordinates.

• bobConditioned : ↥D → Y

  Bob's questions on conditioned coordinates.

• aliceLeft : ↥(exactLeft seed.coordinate seed.partition) → X

  Alice's questions revealed on the left side.

• bobRight : ↥(exactRight seed.coordinate seed.partition) → Y

  Bob's questions revealed on the right side.

• bobLeftPrefix : ↥(exactLeftPrefix seed) → Y

  Bob's revealed prefix on the left side.

• aliceRightPrefix : ↥(exactRightPrefix seed) → X

  Alice's revealed prefix on the right side.

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactRevealHistoryTuple (X : Type u_5) (Y : Type u_6) {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Type (max u_5 u_5 u_6)

The type used to represent exact reveal history tuple in the exact sampling construction.

Equations

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

def QuantumParallelRepetition.exactRevealHistoryEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : ExactRevealHistory X Y D seed ≃ ExactRevealHistoryTuple X Y D seed

The finite equivalence encoding exact reveal history.

Equations

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

@[instance_reducible]

noncomputable instance QuantumParallelRepetition.exactRevealHistoryFintype {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Fintype (ExactRevealHistory X Y D seed)

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactFullQuestion (X : Type u_5) (Y : Type u_6) (n : ℕ) : Type (max u_5 u_6)

The type used to represent exact full question in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactFullQuestion X Y n = ((Fin n → X) × (Fin n → Y))

def QuantumParallelRepetition.exactRevealCode {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (q : ExactFullQuestion X Y n) : ExactRevealHistory X Y D seed

The finite encoding of exact reveal.

Equations

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

def QuantumParallelRepetition.exactPriorQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (q : ExactFullQuestion X Y n) : ℝ

The probability weight for exact prior question.

Equations

• QuantumParallelRepetition.exactPriorQuestionWeight G n q = (G.repeat n).questionWeight q.1 q.2

theorem QuantumParallelRepetition.exactPriorQuestionWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (q : ExactFullQuestion X Y n) : 0 ≤ exactPriorQuestionWeight G n q

theorem QuantumParallelRepetition.exactPriorQuestionWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : ∑ q : ExactFullQuestion X Y n, exactPriorQuestionWeight G n q = 1

noncomputable def QuantumParallelRepetition.exactRevealMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) : ℝ

The total probability mass of exact reveal.

Equations

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

theorem QuantumParallelRepetition.exactRevealMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) : 0 ≤ exactRevealMass G n D seed history

theorem QuantumParallelRepetition.exactRevealMass_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : ∑ history : ExactRevealHistory X Y D seed, exactRevealMass G n D seed history = 1

noncomputable def QuantumParallelRepetition.exactAliceQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) : ℝ

The total probability mass of exact alice question.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) : ℝ

The total probability mass of exact bob question.

Equations

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

noncomputable def QuantumParallelRepetition.exactJointQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : ℝ

The total probability mass of exact joint question.

Equations

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

theorem QuantumParallelRepetition.exactAliceQuestionMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) : 0 ≤ exactAliceQuestionMass G n D seed history x

theorem QuantumParallelRepetition.exactBobQuestionMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) : 0 ≤ exactBobQuestionMass G n D seed history y

noncomputable def QuantumParallelRepetition.exactAliceQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : Matrix S.Alice S.Alice ℂ

The spectral filter for exact alice question.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : Matrix S.Bob S.Bob ℂ

The spectral filter for exact bob question.

Equations

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

theorem QuantumParallelRepetition.exactAliceQuestionFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : (exactAliceQuestionFilter G n S D seed history answer x).PosSemidef

theorem QuantumParallelRepetition.exactBobQuestionFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : (exactBobQuestionFilter G n S D seed history answer y).PosSemidef

noncomputable def QuantumParallelRepetition.exactAliceMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (y : Y) : Matrix S.Alice S.Alice ℂ

The spectral filter for exact alice mean.

Equations

• QuantumParallelRepetition.exactAliceMeanFilter G n S D seed history answer y = ∑ x : X, G.conditionalXGivenY y x • QuantumParallelRepetition.exactAliceQuestionFilter G n S D seed history answer x

noncomputable def QuantumParallelRepetition.exactBobMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) : Matrix S.Bob S.Bob ℂ

The spectral filter for exact bob mean.

Equations

• QuantumParallelRepetition.exactBobMeanFilter G n S D seed history answer x = ∑ y : Y, G.conditionalYGivenX x y • QuantumParallelRepetition.exactBobQuestionFilter G n S D seed history answer y

theorem QuantumParallelRepetition.exactAliceMeanFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (y : Y) : (exactAliceMeanFilter G n S D seed history answer y).PosSemidef

theorem QuantumParallelRepetition.exactBobMeanFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) : (exactBobMeanFilter G n S D seed history answer x).PosSemidef

noncomputable def QuantumParallelRepetition.exactAliceCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (a : A) : Matrix S.Alice S.Alice ℂ

The spectral filter for exact alice coordinate.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) (b : B) : Matrix S.Bob S.Bob ℂ

The spectral filter for exact bob coordinate.

Equations

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

theorem QuantumParallelRepetition.exactAliceCoordinateFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (a : A) : (exactAliceCoordinateFilter G n S D seed history answer x a).PosSemidef

theorem QuantumParallelRepetition.exactBobCoordinateFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) (b : B) : (exactBobCoordinateFilter G n S D seed history answer y b).PosSemidef

theorem QuantumParallelRepetition.exactAliceCoordinateFilter_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : ∑ a : A, exactAliceCoordinateFilter G n S D seed history answer x a = exactAliceQuestionFilter G n S D seed history answer x

theorem QuantumParallelRepetition.exactBobCoordinateFilter_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : ∑ b : B, exactBobCoordinateFilter G n S D seed history answer y b = exactBobQuestionFilter G n S D seed history answer y

noncomputable def QuantumParallelRepetition.exactAlicePurificationFamily {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) : X ⊕ Y → Matrix S.Alice S.Alice ℂ

The exact alice purification family construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobPurificationFamily {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) : Y ⊕ X → Matrix S.Bob S.Bob ℂ

The exact bob purification family construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactAlicePurificationFamily_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : (exactAlicePurificationFamily G n S D seed history answer q).PosSemidef

theorem QuantumParallelRepetition.exactBobPurificationFamily_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : (exactBobPurificationFamily G n S D seed history answer q).PosSemidef

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactAliceLiftIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) : Type

The type used to represent exact alice lift index in the exact sampling construction.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactBobLiftIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) : Type

The type used to represent exact bob lift index in the exact sampling construction.

Equations

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

noncomputable def QuantumParallelRepetition.exactAlicePurificationMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : Matrix (ExactAliceLiftIndex G n S D seed history answer) S.Alice ℂ

The matrix representation of exact alice purification.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobPurificationMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : Matrix (ExactBobLiftIndex G n S D seed history answer) S.Bob ℂ

The matrix representation of exact bob purification.

Equations

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

theorem QuantumParallelRepetition.exactAlicePurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : (exactAlicePurificationMatrix G n S D seed history answer q).conjTranspose * exactAlicePurificationMatrix G n S D seed history answer q = exactAlicePurificationFamily G n S D seed history answer q

theorem QuantumParallelRepetition.exactBobPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : (exactBobPurificationMatrix G n S D seed history answer q).conjTranspose * exactBobPurificationMatrix G n S D seed history answer q = exactBobPurificationFamily G n S D seed history answer q

structure QuantumParallelRepetition.ExactHistoryFlag (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max u_5 u_6) u_7) u_8)

A seed and transcript together with the answers at its marked coordinate.

• seed : ExactRemainingSeed D

  The forward seed carried by the flag.

• history : ExactRevealHistory X Y D self.seed

  The exact reveal history carried by the flag.

• aliceAnswer : ↥D → A

  Alice's answer at the marked coordinate.

• bobAnswer : ↥D → B

  Bob's answer at the marked coordinate.

theorem QuantumParallelRepetition.ExactHistoryFlag.ext {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} {inst✝ : Fintype X} {inst✝¹ : Fintype Y} {inst✝² : Fintype A} {inst✝³ : Fintype B} {n : ℕ} {D : Finset (Fin n)} {x y : ExactHistoryFlag X Y A B D} (seed : x.seed = y.seed) (history : x.history ≍ y.history) (aliceAnswer : x.aliceAnswer = y.aliceAnswer) (bobAnswer : x.bobAnswer = y.bobAnswer) : x = y

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactHistoryFlagTuple (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) : Type (max (max u_8 u_7) u_6 u_5)

The type used to represent exact history flag tuple in the exact sampling construction.

Equations

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

def QuantumParallelRepetition.exactHistoryFlagEquiv {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ExactHistoryFlag X Y A B D ≃ ExactHistoryFlagTuple X Y A B D

The finite equivalence encoding exact history flag.

Equations

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

@[instance_reducible]

noncomputable instance QuantumParallelRepetition.exactHistoryFlagFintype {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Fintype (ExactHistoryFlag X Y A B D)

Equations

• QuantumParallelRepetition.exactHistoryFlagFintype D = Fintype.ofEquiv (QuantumParallelRepetition.ExactHistoryFlagTuple X Y A B D) (QuantumParallelRepetition.exactHistoryFlagEquiv D).symm

theorem QuantumParallelRepetition.exactHistoryFlag_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (f : ExactHistoryFlag X Y A B D → ℝ) : ∑ r : ExactHistoryFlag X Y A B D, f r = ∑ seed : ExactRemainingSeed D, ∑ history : ExactRevealHistory X Y D seed, ∑ aliceAnswer : ↥D → A, ∑ bobAnswer : ↥D → B, f { seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer }

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactAliceLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

The type used to represent exact alice local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactAliceLocalIndex G n S D r = (QuantumParallelRepetition.ExactAliceLiftIndex G n S D r.seed r.history r.aliceAnswer × S.Alice × S.Bob)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactBobLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

The type used to represent exact bob local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactBobLocalIndex G n S D r = QuantumParallelRepetition.ExactBobLiftIndex G n S D r.seed r.history r.bobAnswer

noncomputable def QuantumParallelRepetition.exactUnnormalizedPsi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

The exact unnormalized psi construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactUnnormalizedPhi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

The exact unnormalized phi construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactUnnormalizedGamma {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

The exact unnormalized gamma construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactUnnormalizedPsi_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2 = ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x)) (exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)

theorem QuantumParallelRepetition.exactAliceQuestionPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : (exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x)).conjTranspose * exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x) = exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x

theorem QuantumParallelRepetition.exactBobQuestionPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : (exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y)).conjTranspose * exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y) = exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y

noncomputable def QuantumParallelRepetition.exactAliceRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) : POVM A (ExactAliceLiftIndex G n S D r.seed r.history r.aliceAnswer)

The positive operator-valued measurement implementing exact alice refined.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) : POVM B (ExactBobLiftIndex G n S D r.seed r.history r.bobAnswer)

The positive operator-valued measurement implementing exact bob refined.

Equations

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

theorem QuantumParallelRepetition.exactAliceRefinedPOVM_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) (a : A) : (exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x)).conjTranspose * (exactAliceRefinedPOVM G n S D r a₀ x).effect a * exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x) = exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a

theorem QuantumParallelRepetition.exactBobRefinedPOVM_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) (b : B) : (exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y)).conjTranspose * (exactBobRefinedPOVM G n S D r b₀ y).effect b * exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y) = exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b

theorem QuantumParallelRepetition.exactRefinedPOVM_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (a : A) (b : B) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((exactAliceRefinedPOVM G n S D r a₀ x).effect a) 1) ((exactBobRefinedPOVM G n S D r b₀ y).effect b))) (exactUnnormalizedPsi G n S D r x y) = ((bornTracePairing S.state.matrix) (exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a)) (exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactPaddedLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

The type used to represent exact padded local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactPaddedLocalIndex G n S D r = (PUnit.{1} ⊕ QuantumParallelRepetition.ExactAliceLocalIndex G n S D r ⊕ QuantumParallelRepetition.ExactBobLocalIndex G n S D r)

def QuantumParallelRepetition.exactPaddedVector {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

The state vector representing exact padded.

Equations

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

theorem QuantumParallelRepetition.exactPaddedVector_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : ‖exactPaddedVector G n S D r z‖ = ‖z‖

theorem QuantumParallelRepetition.exactPaddedVector_sub {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (u v : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : exactPaddedVector G n S D r (u - v) = exactPaddedVector G n S D r u - exactPaddedVector G n S D r v

noncomputable def QuantumParallelRepetition.exactPaddedDefault {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

The exact padded default construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactPaddedDefault G n S D r = PiLp.single 2 (Sum.inl PUnit.unit, Sum.inl PUnit.unit) 1

theorem QuantumParallelRepetition.exactPaddedDefault_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : ‖exactPaddedDefault G n S D r‖ = 1

noncomputable def QuantumParallelRepetition.exactPsi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

The exact psi construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactPhi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

The exact phi construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactGamma {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

The exact gamma construction used in the quantum parallel-repetition argument.

Equations

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

def QuantumParallelRepetition.exactAliceQuestionCompatible {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (xs : Fin n → X) : Prop

The exact alice question compatible construction used in the quantum parallel-repetition argument.

Equations

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

def QuantumParallelRepetition.exactBobQuestionCompatible {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) (ys : Fin n → Y) : Prop

The exact bob question compatible construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactRevealCode_compatible_iff {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : exactRevealCode D seed (xs, ys) = history ∧ xs ↑seed.coordinate = x ∧ ys ↑seed.coordinate = y ↔ exactAliceQuestionCompatible D seed history x xs ∧ exactBobQuestionCompatible D seed history y ys

theorem QuantumParallelRepetition.exactCompatible_coordinate_eq_or {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') (j : Fin n) : xs j = xs' j ∨ ys j = ys' j

theorem QuantumParallelRepetition.exactQuestionWeight_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') : (G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys

noncomputable def QuantumParallelRepetition.exactFiberQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : ℝ

The probability weight for exact fiber question.

Equations

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

theorem QuantumParallelRepetition.exactFiberQuestionWeight_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) : exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x y xs' ys' = exactFiberQuestionWeight G n D seed history x y xs ys' * exactFiberQuestionWeight G n D seed history x y xs' ys

noncomputable def QuantumParallelRepetition.exactFiberQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : ℝ

The total probability mass of exact fiber question.

Equations

• QuantumParallelRepetition.exactFiberQuestionMass G n D seed history x y = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, QuantumParallelRepetition.exactFiberQuestionWeight G n D seed history x y xs ys

theorem QuantumParallelRepetition.exactFintypeCard_eq {T : Type u_1} (first second : Fintype T) : Fintype.card T = Fintype.card T

theorem QuantumParallelRepetition.exactSeedWeight_sum {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) : ∑ seed : ExactForwardSeed M, exactSeedWeight seed = 1

def QuantumParallelRepetition.HasExponentialBound (v : ℕ → ℝ) : Prop

The numerical bound for has exponential.

Equations

• QuantumParallelRepetition.HasExponentialBound v = ∃ (c : ℝ), 0 < c ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), v n ≤ C * Real.exp (-c * ↑n)

def QuantumParallelRepetition.HasSubexponentialWitness (v : ℕ → ℝ) : Prop

The has subexponential witness construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.HasSubexponentialWitness v = ∀ (c : ℝ), 0 < c → ∀ (C : ℝ), 0 < C → ∃ (n : ℕ), C * Real.exp (-c * ↑n) < v n

theorem QuantumParallelRepetition.not_hasExponentialBound_iff (v : ℕ → ℝ) : ¬HasExponentialBound v ↔ HasSubexponentialWitness v

theorem QuantumParallelRepetition.arbitrarily_large_witness_of_not_hasExponentialBound {v : ℕ → ℝ} (hv : ∀ (n : ℕ), v n ≤ 1) (h_no_bound : ¬HasExponentialBound v) {c : ℝ} (hc : 0 < c) (N : ℕ) : ∃ (n : ℕ), N < n ∧ Real.exp (-c * ↑n) < v n

def QuantumParallelRepetition.StandardQuantumParallelRepetition {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Prop

The standard exponential-decay statement for quantum parallel repetition.

Equations

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

theorem QuantumParallelRepetition.sum_positive_difference_eq_totalVariation {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) : ∑ i : ι, max (p i - q i) 0 = Pinsker.finiteTotalVariation p q

theorem QuantumParallelRepetition.finiteTotalVariation_comm {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : Pinsker.finiteTotalVariation p q = Pinsker.finiteTotalVariation q p

theorem QuantumParallelRepetition.expectation_le_add_totalVariation {ι : Type u_1} [Fintype ι] (p q f : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) (U : ℝ) (hfzero : ∀ (i : ι), 0 ≤ f i) (hfupper : ∀ (i : ι), f i ≤ U) : ∑ i : ι, p i * f i ≤ ∑ i : ι, q i * f i + U * Pinsker.finiteTotalVariation p q

theorem QuantumParallelRepetition.winning_expectation_transfer {ι : Type u_1} [Fintype ι] (p q win : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) (hzero : ∀ (i : ι), 0 ≤ win i) (hone : ∀ (i : ι), win i ≤ 1) : ∑ i : ι, q i * win i - Pinsker.finiteTotalVariation p q ≤ ∑ i : ι, p i * win i

def QuantumParallelRepetition.pureVerifierEffect {X Y A B dA dB : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (G : Game X Y A B) (z : EuclideanSpace ℂ (dA × dB)) (hz : ‖z‖ = 1) (PA : X → POVM A dA) (PB : Y → POVM B dB) (x : X) (y : Y) : Matrix (dA × dB) (dA × dB) ℂ

The measurement effect for pure verifier.

Equations

• QuantumParallelRepetition.pureVerifierEffect G z hz PA PB x y = (QuantumParallelRepetition.pureVectorStrategy G z hz PA PB).winningEffect x y

theorem QuantumParallelRepetition.pureVectorWinningProbability_eq {X Y A B dA dB : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (G : Game X Y A B) (z : EuclideanSpace ℂ (dA × dB)) (hz : ‖z‖ = 1) (PA : X → POVM A dA) (PB : Y → POVM B dB) : (pureVectorStrategy G z hz PA PB).winProbability = ∑ x : X, ∑ y : Y, G.questionWeight x y * quadraticExpectation (Matrix.toEuclideanCLM (pureVerifierEffect G z hz PA PB x y)) z

def QuantumParallelRepetition.flaggedQuestionWeight {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (flagWeight : J → ℝ) (ω : J × X × Y) : ℝ

The probability weight for flagged question.

Equations

• QuantumParallelRepetition.flaggedQuestionWeight G flagWeight ω = flagWeight ω.1 * G.questionWeight ω.2.1 ω.2.2

theorem QuantumParallelRepetition.flaggedQuestionWeight_nonneg {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (flagWeight : J → ℝ) (nonnegative : ∀ (j : J), 0 ≤ flagWeight j) (ω : J × X × Y) : 0 ≤ flaggedQuestionWeight G flagWeight ω

theorem QuantumParallelRepetition.flaggedQuestionWeight_sum {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] (G : Game X Y A B) (flagWeight : J → ℝ) (normalized : ∑ j : J, flagWeight j = 1) : ∑ ω : J × X × Y, flaggedQuestionWeight G flagWeight ω = 1

noncomputable def QuantumParallelRepetition.universalErrorCeiling (K₀ : ℝ) : ℝ

A universal upper bound for the accumulated rounding error.

Equations

• QuantumParallelRepetition.universalErrorCeiling K₀ = K₀ * (1 + 2 ^ (1 / 6)) + 2

noncomputable def QuantumParallelRepetition.totalSamplingLoss (K₀ α η lam : ℝ) : ℝ

The combined information-theoretic loss from the sampling steps.

Equations

• QuantumParallelRepetition.totalSamplingLoss K₀ α η lam = 5 * lam + 2 * (K₀ * (α ^ (1 / 12) + (32 * η) ^ (1 / 12)) + √(8 * η) + QuantumParallelRepetition.universalErrorCeiling K₀ * lam)

noncomputable def QuantumParallelRepetition.roundedWinningLowerBound (ε K₀ α η lam : ℝ) : ℝ

The numerical bound for rounded winning lower.

Equations

• QuantumParallelRepetition.roundedWinningLowerBound ε K₀ α η lam = 1 - ε / 2 - QuantumParallelRepetition.totalSamplingLoss K₀ α η lam

theorem QuantumParallelRepetition.totalSamplingLoss_tendsto_zero {ι : Type u_1} {l : Filter ι} (K₀ : ℝ) {α η lam : ι → ℝ} (hα : Filter.Tendsto α l (nhds 0)) (hη : Filter.Tendsto η l (nhds 0)) (hlam : Filter.Tendsto lam l (nhds 0)) : Filter.Tendsto (fun (i : ι) => totalSamplingLoss K₀ (α i) (η i) (lam i)) l (nhds 0)

theorem QuantumParallelRepetition.totalSamplingLoss_eventually_lt {ι : Type u_1} {l : Filter ι} (K₀ : ℝ) {α η lam : ι → ℝ} (hα : Filter.Tendsto α l (nhds 0)) (hη : Filter.Tendsto η l (nhds 0)) (hlam : Filter.Tendsto lam l (nhds 0)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, totalSamplingLoss K₀ (α i) (η i) (lam i) < ε

theorem QuantumParallelRepetition.source_equation_twenty_nine_contradiction {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : Strategy G) (K₀ α η lam : ℝ) (hbound : roundedWinningLowerBound (1 - entangledValue G) K₀ α η lam ≤ S.winProbability) (herror : totalSamplingLoss K₀ α η lam < (1 - entangledValue G) / 2) : False

theorem QuantumParallelRepetition.matched_payoff_discard_le {ι : Type u_1} [Fintype ι] (weight payoff : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (payoff_le_one : ∀ (i : ι), payoff i ≤ 1) (matched : ι → Bool) : (∑ i : ι, weight i * payoff i - ∑ i : ι, weight i * if matched i = true then 0 else 1) ≤ ∑ i : ι, weight i * if matched i = true then payoff i else 0

theorem QuantumParallelRepetition.squared_state_triangle {E : Type u_1} [NormedAddCommGroup E] (gamma psi phi : E) : ‖gamma - phi‖ ^ 2 ≤ 2 * (‖gamma - psi‖ ^ 2 + ‖psi - phi‖ ^ 2)

theorem QuantumParallelRepetition.source_equation_twenty_one {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] (weight : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (gamma psi phi : ι → E) (η : ℝ) (hgamma : ∑ i : ι, weight i * ‖gamma i - psi i‖ ^ 2 ≤ 8 * η) (hphi : ∑ i : ι, weight i * ‖psi i - phi i‖ ^ 2 ≤ 8 * η) : ∑ i : ι, weight i * ‖gamma i - phi i‖ ^ 2 ≤ 32 * η

theorem QuantumParallelRepetition.weighted_rpow_mean_le {ι : Type u_1} [Fintype ι] (weight value : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (value_nonnegative : ∀ (i : ι), 0 ≤ value i) {r : ℝ} (hrzero : 0 ≤ r) (hrone : r ≤ 1) : ∑ i : ι, weight i * value i ^ r ≤ (∑ i : ι, weight i * value i) ^ r

theorem QuantumParallelRepetition.fullHistoryRemaining_insert_conditioned {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) : fullHistoryRemaining n (insert i D) L = fullHistoryRemaining n D (insert i L)

theorem QuantumParallelRepetition.conditionedCoordinateEffects_born_expansion {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (β : ↥D → B) (xs : Fin n → X) (ys : Fin n → Y) (i : Fin n) (a : A) (b : B) : ((bornTracePairing S.state.matrix) (conditionedAliceCoordinateEffect G n S D α xs i a)) (conditionedBobCoordinateEffect G n S D β ys i b) = ∑ aa : Fin n → A, ∑ bb : Fin n → B, if (∀ (j : Fin n) (hj : j ∈ D), aa j = α ⟨j, hj⟩) ∧ aa i = a then if (∀ (j : Fin n) (hj : j ∈ D), bb j = β ⟨j, hj⟩) ∧ bb i = b then S.outcomeProbability xs ys aa bb else 0 else 0

noncomputable def QuantumParallelRepetition.normalizedPureVector {d : Type u_1} [Fintype d] (z : EuclideanSpace ℂ d) : EuclideanSpace ℂ d

The state vector representing normalized pure.

Equations

• QuantumParallelRepetition.normalizedPureVector z = ↑‖z‖⁻¹ • z

theorem QuantumParallelRepetition.quadraticExpectation_normalizedPureVector {d : Type u_1} [Fintype d] (W : EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d) (z : EuclideanSpace ℂ d) : quadraticExpectation W (normalizedPureVector z) = quadraticExpectation W z / ‖z‖ ^ 2

theorem QuantumParallelRepetition.exists_repeatedStrategy_of_lt_entangledValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {r : ℝ} (hr : 0 < r) (hvalue : r < repeatedEntangledValue G n) : ∃ (S : Strategy (G.repeat n)), r < S.winProbability

theorem QuantumParallelRepetition.exists_purifiedRepeatedStrategy_of_lt_entangledValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {r : ℝ} (hr : 0 < r) (hvalue : r < repeatedEntangledValue G n) : ∃ (S : Strategy (G.repeat n)), r < (purifiedStrategy S).winProbability

theorem QuantumParallelRepetition.arbitrarily_large_purifiedRepeatedStrategy_of_subexponentialWitness {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hwitness : HasSubexponentialWitness (repeatedEntangledValue G)) {c : ℝ} (hc : 0 < c) (N : ℕ) : ∃ (n : ℕ), N < n ∧ ∃ (S : Strategy (G.repeat n)), Real.exp (-c * ↑n) < (purifiedStrategy S).winProbability

theorem QuantumParallelRepetition.postselection_log_cost_le {θ p : ℝ} (hθ : 0 < θ) (hθp : θ ≤ p) : Real.log (1 / p) ≤ Real.log (1 / θ)

theorem QuantumParallelRepetition.greedy_terminal_of_log_cost {θ η : ℝ} {T : ℕ} (hθ : 0 < θ) (hη_one : η ≤ 1) (hcost : Real.log (1 / θ) < η * ↑T) : (1 - η) ^ T < θ

theorem QuantumParallelRepetition.divisorStopping_nat_bound {n q : ℕ} (hq : 0 < q) (hqn : q ≤ n) : n < 2 * (n / q) * q

theorem QuantumParallelRepetition.sourceRate_mul_lt_divisorStopping {n q : ℕ} (hq : 0 < q) (hqn : q ≤ n) {η : ℝ} (hη : 0 < η) : η / (4 * ↑q) * ↑n < η * ↑(n / q)

theorem QuantumParallelRepetition.repeatedStrategy_exists_divisor_greedy_conditioning {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) {η : ℝ} {q : ℕ} (hη : 0 < η) (hη_one : η ≤ 1) (hq : 0 < q) (hqn : q ≤ n) (hwitness : Real.exp (-(η / (4 * ↑q)) * ↑n) < S.winProbability) : ∃ (D : Finset (Fin n)), D.card < n / q ∧ S.winProbability ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) ∧ ∑ i ∈ Finset.univ \ D, (strategyEventLaw (G.repeat n) S).failureMass (repeatedCoordinateWin G n) D i < ↑(Finset.univ \ D).card * (η * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

theorem QuantumParallelRepetition.divisor_greedy_card_mul_lt {n q : ℕ} (hq : 0 < q) {D : Finset (Fin n)} (hD : D.card < n / q) : D.card * q < n

def QuantumParallelRepetition.postselectionMass {ι : Type u_1} {Ω : Type u_2} [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : ℝ

The total probability mass of postselection.

Equations

• QuantumParallelRepetition.postselectionMass law wins C = law.eventMass (QuantumParallelRepetition.FiniteEventLaw.winEvent wins C)

theorem QuantumParallelRepetition.allWinMass_le_postselectionMass {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : law.eventMass (FiniteEventLaw.winEvent wins Finset.univ) ≤ postselectionMass law wins C

theorem QuantumParallelRepetition.postselectionMass_le_one {ι : Type u_1} {Ω : Type u_2} [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : postselectionMass law wins C ≤ 1

noncomputable def QuantumParallelRepetition.conditionalCoordinateFailure {ι : Type u_1} {Ω : Type u_2} [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) (i : ι) : ℝ

The conditional coordinate failure construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.conditionalCoordinateFailure law wins C i = law.failureMass wins C i / QuantumParallelRepetition.postselectionMass law wins C

noncomputable def QuantumParallelRepetition.uniformRemainingFailure {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : ℝ

The uniform remaining failure construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.uniformRemainingFailure law wins C = (∑ i ∈ Finset.univ \ C, QuantumParallelRepetition.conditionalCoordinateFailure law wins C i) / ↑(Finset.univ \ C).card

theorem QuantumParallelRepetition.uniformRemainingFailure_lt_of_failure_sum {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) {η : ℝ} (hp : 0 < postselectionMass law wins C) (hm : 0 < (Finset.univ \ C).card) (hfailure : ∑ i ∈ Finset.univ \ C, law.failureMass wins C i < ↑(Finset.univ \ C).card * (η * postselectionMass law wins C)) : uniformRemainingFailure law wins C < η

def QuantumParallelRepetition.repeatedPostselectionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) : ℝ

The total probability mass of repeated postselection.

Equations

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

theorem QuantumParallelRepetition.repeated_winProbability_le_postselectionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) : S.winProbability ≤ repeatedPostselectionMass G n S C

theorem QuantumParallelRepetition.repeatedPostselectionMass_pos {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) (hwin : 0 < S.winProbability) : 0 < repeatedPostselectionMass G n S C

theorem QuantumParallelRepetition.remainingCoordinates_card {n : ℕ} (C : Finset (Fin n)) : (Finset.univ \ C).card = n - C.card

theorem QuantumParallelRepetition.repeatedStrategy_exists_conditioning {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) {η : ℝ} {q : ℕ} (hwin : 0 < S.winProbability) (hη_one : η ≤ 1) (hq : q ≤ n) (hterminal : (1 - η) ^ q < S.winProbability) : ∃ (C : Finset (Fin n)), C.card < q ∧ S.winProbability ≤ repeatedPostselectionMass G n S C ∧ 0 < repeatedPostselectionMass G n S C ∧ 0 < (Finset.univ \ C).card ∧ uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) C < η

theorem QuantumParallelRepetition.source_equation_nineteen_alice {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : -((bornTracePairing ρ.matrix) (cfc (fun (z : ℝ) => z * Real.log z) F)) G ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

theorem QuantumParallelRepetition.source_equation_nineteen_bob {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : -((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

noncomputable def QuantumParallelRepetition.postselectionLogCost {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The postselection log cost construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.postselectionLogCost G n S D = Real.log (1 / QuantumParallelRepetition.repeatedPostselectionMass G n S D)

noncomputable def QuantumParallelRepetition.answerLogCost {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ℝ

The answer log cost construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.answerLogCost D = ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

noncomputable def QuantumParallelRepetition.martingaleRate {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The error rate associated with martingale.

Equations

• QuantumParallelRepetition.martingaleRate G n S D = (QuantumParallelRepetition.postselectionLogCost G n S D + QuantumParallelRepetition.answerLogCost D) / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.answerCount_pos_of_postselection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : 0 < fullHistoryAnswerCount D

theorem QuantumParallelRepetition.martingale_log_cost_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D) = postselectionLogCost G n S D + answerLogCost D

theorem QuantumParallelRepetition.bornWeighted_normalized_distance {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] (fallback u v : E) (hfallback : ‖fallback‖ = 1) : ‖u‖ ^ 2 * ‖normalizeOrDefault fallback u - normalizeOrDefault fallback v‖ ^ 2 ≤ 4 * ‖u - v‖ ^ 2

noncomputable def QuantumParallelRepetition.sourceHistoryAcceptedMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The total probability mass of source history accepted.

Equations

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

theorem QuantumParallelRepetition.sourceHistoryQuadraticExpectation_matrix_sum {I : Type u_5} {d : Type u_6} [Fintype I] [Fintype d] [DecidableEq d] (M : I → Matrix d d ℂ) (z : EuclideanSpace ℂ d) : quadraticExpectation (Matrix.toEuclideanCLM (∑ i : I, M i)) z = ∑ i : I, quadraticExpectation (Matrix.toEuclideanCLM (M i)) z

theorem QuantumParallelRepetition.sourceHistoryAcceptedMass_eq_remaining_average {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : sourceHistoryAcceptedMass G n S D = (∑ i : SourceRemainingCoordinate D, (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert (↑i) D))) / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.sourceHistoryAcceptedMass_gt_of_greedy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) {η : ℝ} (hgreedy : ∑ i ∈ Finset.univ \ D, (strategyEventLaw (G.repeat n) S).failureMass (repeatedCoordinateWin G n) D i < ↑(Finset.univ \ D).card * (η * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))) : (1 - η) * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) < sourceHistoryAcceptedMass G n S D

noncomputable def QuantumParallelRepetition.taggedTensorVector {R : Type u_1} {ι : R → Type u_2} (r : R) (z : EuclideanSpace ℂ (ι r × ι r)) : EuclideanSpace ℂ ((PUnit.{1} ⊕ (r : R) × ι r) × (PUnit.{1} ⊕ (r : R) × ι r))

The state vector representing tagged tensor.

Equations

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

theorem QuantumParallelRepetition.taggedTensorVector_norm {R : Type u_1} [Fintype R] {ι : R → Type u_2} [(r : R) → Fintype (ι r)] (r : R) (z : EuclideanSpace ℂ (ι r × ι r)) : ‖taggedTensorVector r z‖ = ‖z‖

theorem QuantumParallelRepetition.taggedTensorVector_sub {R : Type u_1} {ι : R → Type u_2} (r : R) (u v : EuclideanSpace ℂ (ι r × ι r)) : taggedTensorVector r (u - v) = taggedTensorVector r u - taggedTensorVector r v

theorem QuantumParallelRepetition.martingaleRate_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) (hp : 0 < repeatedPostselectionMass G n S D) : 0 ≤ martingaleRate G n S D

theorem QuantumParallelRepetition.remainingCoordinate_card_pos {n : ℕ} (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) : 0 < Fintype.card (SourceRemainingCoordinate D)

theorem QuantumParallelRepetition.finiteTotalVariation_triangle {ι : Type u_5} [Fintype ι] (p q r : ι → ℝ) : Pinsker.finiteTotalVariation p r ≤ Pinsker.finiteTotalVariation p q + Pinsker.finiteTotalVariation q r

def QuantumParallelRepetition.weightedConditionalJoint {κ : Type u_5} {ι : Type u_6} (weight : κ → ℝ) (conditional : κ → ι → ℝ) : κ × ι → ℝ

The weighted conditional joint construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.weightedConditionalJoint weight conditional t = weight t.1 * conditional t.1 t.2

theorem QuantumParallelRepetition.weightedConditionalJoint_totalVariation {κ : Type u_5} {ι : Type u_6} [Fintype κ] [Fintype ι] (weight : κ → ℝ) (hweight : ∀ (k : κ), 0 ≤ weight k) (left right : κ → ι → ℝ) : Pinsker.finiteTotalVariation (weightedConditionalJoint weight left) (weightedConditionalJoint weight right) = ∑ k : κ, weight k * Pinsker.finiteTotalVariation (left k) (right k)

theorem QuantumParallelRepetition.finiteTotalVariation_equiv {ι : Type u_5} {κ : Type u_6} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p q : κ → ℝ) : Pinsker.finiteTotalVariation (p ∘ ⇑e) (q ∘ ⇑e) = Pinsker.finiteTotalVariation p q

@[reducible, inline]

abbrev QuantumParallelRepetition.LocalQuestionContext (X : Type u_5) (Y : Type u_6) {n : ℕ} (D : Finset (Fin n)) : Type (max u_6 u_5)

The type used to represent local question context in the exact sampling construction.

Equations

• QuantumParallelRepetition.LocalQuestionContext X Y D = (QuantumParallelRepetition.SourceRemainingCoordinate D × X × Y)

noncomputable def QuantumParallelRepetition.localQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (c : LocalQuestionContext X Y D) : ℝ

The probability weight for local question.

Equations

• QuantumParallelRepetition.localQuestionWeight G n D c = G.questionWeight c.2.1 c.2.2 / ↑(Fintype.card (QuantumParallelRepetition.SourceRemainingCoordinate D))

theorem QuantumParallelRepetition.localQuestionWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (c : LocalQuestionContext X Y D) : 0 ≤ localQuestionWeight G n D c

theorem QuantumParallelRepetition.localQuestionWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) : ∑ c : LocalQuestionContext X Y D, localQuestionWeight G n D c = 1

noncomputable def QuantumParallelRepetition.conditionedEventDistribution {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) : Ω → ℝ

The probability distribution for conditioned event.

Equations

• QuantumParallelRepetition.conditionedEventDistribution law event ω = if ω ∈ event then law.weight ω / law.eventMass event else 0

theorem QuantumParallelRepetition.conditionedEventDistribution_nonneg {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) (ω : Ω) : 0 ≤ conditionedEventDistribution law event ω

theorem QuantumParallelRepetition.conditionedEventDistribution_sum {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) : ∑ ω : Ω, conditionedEventDistribution law event ω = 1

theorem QuantumParallelRepetition.conditionedEventDistribution_absolute_continuity {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (ω : Ω) : law.weight ω = 0 → conditionedEventDistribution law event ω = 0

theorem QuantumParallelRepetition.conditionedEventDistribution_relativeEntropy {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) : Pinsker.finiteRelativeEntropy (conditionedEventDistribution law event) law.weight = Real.log (1 / law.eventMass event)

theorem QuantumParallelRepetition.conditionedEventDistribution_projection_relativeEntropy_le {Ω : Type u_5} {κ : Type u_6} [Fintype Ω] [Fintype κ] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) (projection : Ω → κ) : Pinsker.finiteRelativeEntropy (ClassicalInformation.groupedMass projection (conditionedEventDistribution law event)) (ClassicalInformation.groupedMass projection law.weight) ≤ Real.log (1 / law.eventMass event)

noncomputable def QuantumParallelRepetition.repeatedConditionedOutcomeLaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B) → ℝ

The finite probability law for repeated conditioned outcome.

Equations

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

theorem QuantumParallelRepetition.repeatedConditionedOutcomeLaw_relativeEntropy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Pinsker.finiteRelativeEntropy (repeatedConditionedOutcomeLaw G n S D) (strategyEventLaw (G.repeat n) S).weight = postselectionLogCost G n S D

noncomputable def QuantumParallelRepetition.finiteUniformWeight (Z : Type u_1) [Fintype Z] : ℝ

The probability weight for finite uniform.

Equations

• QuantumParallelRepetition.finiteUniformWeight Z = 1 / ↑(Fintype.card Z)

theorem QuantumParallelRepetition.finiteUniformWeight_pos {Z : Type u_1} [Fintype Z] (positive : 0 < Fintype.card Z) : 0 < finiteUniformWeight Z

theorem QuantumParallelRepetition.finiteUniformWeight_sum {Z : Type u_1} [Fintype Z] (positive : 0 < Fintype.card Z) : ∑ _z : Z, finiteUniformWeight Z = 1

theorem QuantumParallelRepetition.finiteProbability_le_one {Z : Type u_1} [Fintype Z] (p : Z → ℝ) (nonnegative : ∀ (z : Z), 0 ≤ p z) (normalized : ∑ z : Z, p z = 1) (z : Z) : p z ≤ 1

theorem QuantumParallelRepetition.finiteRelativeEntropy_uniform_le_log_card {Z : Type u_1} [Fintype Z] (p : Z → ℝ) (nonnegative : ∀ (z : Z), 0 ≤ p z) (normalized : ∑ z : Z, p z = 1) (positive : 0 < Fintype.card Z) : (Pinsker.finiteRelativeEntropy p fun (x : Z) => finiteUniformWeight Z) ≤ Real.log ↑(Fintype.card Z)

noncomputable def QuantumParallelRepetition.uniformFlagReference {Ω : Type u_1} {Z : Type u_2} [Fintype Z] (prior : Ω → ℝ) : Ω × Z → ℝ

The uniform flag reference construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.uniformFlagReference prior t = prior t.1 * QuantumParallelRepetition.finiteUniformWeight Z

theorem QuantumParallelRepetition.uniformFlagReference_nonneg {Ω : Type u_1} {Z : Type u_2} [Fintype Z] (prior : Ω → ℝ) (nonnegative : ∀ (ω : Ω), 0 ≤ prior ω) (positive : 0 < Fintype.card Z) (t : Ω × Z) : 0 ≤ uniformFlagReference prior t

theorem QuantumParallelRepetition.uniformFlagReference_sum {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) (normalized : ∑ ω : Ω, prior ω = 1) (positive : 0 < Fintype.card Z) : ∑ t : Ω × Z, uniformFlagReference prior t = 1

theorem QuantumParallelRepetition.uniformFlagReference_firstMarginal {Ω : Type u_1} {Z : Type u_2} [Fintype Z] (prior : Ω → ℝ) (positive : 0 < Fintype.card Z) : ClassicalInformation.jointFirstMarginal (uniformFlagReference prior) = prior

theorem QuantumParallelRepetition.uniformFlagReference_conditional {Ω : Type u_1} {Z : Type u_2} [Fintype Z] (prior : Ω → ℝ) (positive : 0 < Fintype.card Z) (ω : Ω) (hprior : prior ω ≠ 0) : ClassicalInformation.jointConditional (uniformFlagReference prior) ω = fun (x : Z) => finiteUniformWeight Z

theorem QuantumParallelRepetition.uniformFlagReference_absolute_continuity {Ω : Type u_1} {Z : Type u_2} [Fintype Z] (joint : Ω × Z → ℝ) (prior : Ω → ℝ) (hjoint : ∀ (t : Ω × Z), 0 ≤ joint t) (absolute_continuity : ∀ (ω : Ω), prior ω = 0 → ClassicalInformation.jointFirstMarginal joint ω = 0) (positive : 0 < Fintype.card Z) (t : Ω × Z) : uniformFlagReference prior t = 0 → joint t = 0

theorem QuantumParallelRepetition.uniformFlagRelativeEntropy_le {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (joint : Ω × Z → ℝ) (prior : Ω → ℝ) (hjoint : ∀ (t : Ω × Z), 0 ≤ joint t) (hprior : ∀ (ω : Ω), 0 ≤ prior ω) (joint_normalized : ∑ t : Ω × Z, joint t = 1) (prior_normalized : ∑ ω : Ω, prior ω = 1) (absolute_continuity : ∀ (ω : Ω), prior ω = 0 → ClassicalInformation.jointFirstMarginal joint ω = 0) (positive : 0 < Fintype.card Z) : Pinsker.finiteRelativeEntropy joint (uniformFlagReference prior) ≤ Pinsker.finiteRelativeEntropy (ClassicalInformation.jointFirstMarginal joint) prior + Real.log ↑(Fintype.card Z)

theorem QuantumParallelRepetition.finiteRelativeEntropy_nonneg {Ω : Type u_1} [Fintype Ω] (p q : Ω → ℝ) (hp : ∀ (ω : Ω), 0 ≤ p ω) (hq : ∀ (ω : Ω), 0 ≤ q ω) : 0 ≤ Pinsker.finiteRelativeEntropy p q

theorem QuantumParallelRepetition.groupedMass_nonneg {Ω : Type u_1} {κ : Type u_2} [Fintype Ω] [DecidableEq κ] (f : Ω → κ) (p : Ω → ℝ) (hp : ∀ (ω : Ω), 0 ≤ p ω) (a : κ) : 0 ≤ ClassicalInformation.groupedMass f p a

theorem QuantumParallelRepetition.groupedMass_absolute_continuity {Ω : Type u_1} {κ : Type u_2} [Fintype Ω] [DecidableEq κ] (f : Ω → κ) (p q : Ω → ℝ) (hq : ∀ (ω : Ω), 0 ≤ q ω) (absolute_continuity : ∀ (ω : Ω), q ω = 0 → p ω = 0) (a : κ) : ClassicalInformation.groupedMass f q a = 0 → ClassicalInformation.groupedMass f p a = 0

theorem QuantumParallelRepetition.groupedMass_comp {Ω : Type u_1} {κ : Type u_2} {θ : Type u_3} [Fintype Ω] [Fintype κ] [DecidableEq κ] [DecidableEq θ] (f : Ω → κ) (g : κ → θ) (p : Ω → ℝ) : ClassicalInformation.groupedMass g (ClassicalInformation.groupedMass f p) = ClassicalInformation.groupedMass (g ∘ f) p

theorem QuantumParallelRepetition.groupedMass_id {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : Ω → ℝ) : ClassicalInformation.groupedMass id p = p

def QuantumParallelRepetition.finitePrefixMask {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) (k : Fin (h + 1)) : Ω × (Fin h → Y) → Ω × (Fin h → Y)

The finite prefix mask construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.finitePrefixMask base k t = (t.1, fun (j : Fin h) => if ↑j < ↑k then t.2 j else base)

theorem QuantumParallelRepetition.finitePrefixMask_comp {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) (k : Fin h) : finitePrefixMask base k.castSucc ∘ finitePrefixMask base k.succ = finitePrefixMask base k.castSucc

theorem QuantumParallelRepetition.finitePrefixMask_last {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) : finitePrefixMask base (Fin.last h) = id

noncomputable def QuantumParallelRepetition.finitePrefixRelativeEntropy {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (base : Y) (k : Fin (h + 1)) : ℝ

The entropy quantity for finite prefix relative.

Equations

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

theorem QuantumParallelRepetition.finitePrefixRelativeEntropy_telescope {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (base : Y) : ∑ k : Fin h, (finitePrefixRelativeEntropy joint prior base k.succ - finitePrefixRelativeEntropy joint prior base k.castSucc) = Pinsker.finiteRelativeEntropy joint prior - finitePrefixRelativeEntropy joint prior base 0

theorem QuantumParallelRepetition.finitePrefixRelativeEntropy_budget {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (hjoint : ∀ (t : Ω × (Fin h → Y)), 0 ≤ joint t) (hprior : ∀ (t : Ω × (Fin h → Y)), 0 ≤ prior t) (base : Y) : ∑ k : Fin h, (finitePrefixRelativeEntropy joint prior base k.succ - finitePrefixRelativeEntropy joint prior base k.castSucc) ≤ Pinsker.finiteRelativeEntropy joint prior

theorem QuantumParallelRepetition.reversePartition_relativeEntropy_budget {M : Type u_1} [Fintype M] (nonempty : 0 < Fintype.card M) (increment : (s : Finset M) → Fin s.card → ℝ) {cost : ℝ} (hcost : 0 ≤ cost) (hbudget : ∀ (s : Finset M), ∑ k : Fin s.card, increment s k ≤ cost) : ∑ s : Finset M, reversePartitionWeight s * ((∑ k : Fin s.card, increment s k) / ↑s.card) ≤ 2 * cost / ↑(Fintype.card M)

theorem QuantumParallelRepetition.groupedMass_sum {Ω : Type u_5} {κ : Type u_6} [Fintype Ω] [Fintype κ] [DecidableEq κ] (projection : Ω → κ) (mass : Ω → ℝ) : ∑ a : κ, ClassicalInformation.groupedMass projection mass a = ∑ ω : Ω, mass ω

theorem QuantumParallelRepetition.groupedMass_first {Ω : Type u_5} {Z : Type u_6} [Fintype Ω] [Fintype Z] [DecidableEq Ω] (joint : Ω × Z → ℝ) : ClassicalInformation.groupedMass Prod.fst joint = ClassicalInformation.jointFirstMarginal joint

@[reducible, inline]

abbrev QuantumParallelRepetition.ConditionedAnswerFlag (A : Type u_5) (B : Type u_6) {n : ℕ} (D : Finset (Fin n)) : Type (max u_5 u_6)

The type used to represent conditioned answer flag in the exact sampling construction.

Equations

• QuantumParallelRepetition.ConditionedAnswerFlag A B D = ((↥D → A) × (↥D → B))

def QuantumParallelRepetition.repeatedConditionedAnswerFlag {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (_S : Strategy (G.repeat n)) (D : Finset (Fin n)) (ω : StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) : ConditionedAnswerFlag A B D

The repeated conditioned answer flag construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.repeatedConditionedAnswerFlag G n _S D ω = (fun (i : ↥D) => ω.2.2.1 ↑i, fun (i : ↥D) => ω.2.2.2 ↑i)

theorem QuantumParallelRepetition.conditionedAnswerFlag_card {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ↑(Fintype.card (ConditionedAnswerFlag A B D)) = fullHistoryAnswerCount D

theorem QuantumParallelRepetition.conditionedAnswerFlag_card_pos {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : 0 < Fintype.card (ConditionedAnswerFlag A B D)

theorem QuantumParallelRepetition.conditionedAnswerFlag_log_card {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Real.log ↑(Fintype.card (ConditionedAnswerFlag A B D)) = answerLogCost D

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactOutcome (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) (n : ℕ) : Type (max u_5 (max u_8 u_7) u_6)

The type used to represent exact outcome in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactOutcome X Y A B n = QuantumParallelRepetition.StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactJointOutcome (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max u_8 u_7) u_6) u_5)

The type used to represent exact joint outcome in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactJointOutcome X Y A B D = (QuantumParallelRepetition.ExactRemainingSeed D × QuantumParallelRepetition.ExactOutcome X Y A B n)

theorem QuantumParallelRepetition.exactRemainingSeedWeight_sum {n : ℕ} (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) : ∑ seed : ExactRemainingSeed D, exactSeedWeight seed = 1

noncomputable def QuantumParallelRepetition.exactPostselectedJointLaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (q : ExactJointOutcome X Y A B D) : ℝ

The finite probability law for exact postselected joint.

Equations

• QuantumParallelRepetition.exactPostselectedJointLaw G n S D q = QuantumParallelRepetition.exactSeedWeight q.1 * QuantumParallelRepetition.repeatedConditionedOutcomeLaw G n S D q.2

theorem QuantumParallelRepetition.exactPostselectedJointLaw_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (q : ExactJointOutcome X Y A B D) : 0 ≤ exactPostselectedJointLaw G n S D q

theorem QuantumParallelRepetition.exactPostselectedJointLaw_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) : ∑ q : ExactJointOutcome X Y A B D, exactPostselectedJointLaw G n S D q = 1

noncomputable def QuantumParallelRepetition.exactSourcePushforward {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (projection : ExactJointOutcome X Y A B D → K) : K → ℝ

The exact source pushforward construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactSourcePushforward_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (projection : ExactJointOutcome X Y A B D → K) (k : K) : 0 ≤ exactSourcePushforward G n S D projection k

theorem QuantumParallelRepetition.exactSourcePushforward_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} [Fintype K] (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) (projection : ExactJointOutcome X Y A B D → K) : ∑ k : K, exactSourcePushforward G n S D projection k = 1

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactLocallySampleableTuple (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max (max (max u_8 u_7) u_6) u_5) u_6) u_5)

The type used to represent exact locally sampleable tuple in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactLocallySampleableTuple X Y A B D = (QuantumParallelRepetition.SourceRemainingCoordinate D × X × Y × QuantumParallelRepetition.ExactHistoryFlag X Y A B D)

def QuantumParallelRepetition.exactHistoryCode {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (q : ExactJointOutcome X Y A B D) : ExactHistoryFlag X Y A B D

The finite encoding of exact history.

Equations

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

def QuantumParallelRepetition.exactLocallySampleableCode {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (q : ExactJointOutcome X Y A B D) : ExactLocallySampleableTuple X Y A B D

The finite encoding of exact locally sampleable.

Equations

• QuantumParallelRepetition.exactLocallySampleableCode D q = (q.1.coordinate, q.2.1 ↑q.1.coordinate, q.2.2.1 ↑q.1.coordinate, QuantumParallelRepetition.exactHistoryCode D q)

noncomputable def QuantumParallelRepetition.exactLocallySampleableLaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ExactLocallySampleableTuple X Y A B D → ℝ

The finite probability law for exact locally sampleable.

Equations

• QuantumParallelRepetition.exactLocallySampleableLaw G n S D = QuantumParallelRepetition.exactSourcePushforward G n S D (QuantumParallelRepetition.exactLocallySampleableCode D)

theorem QuantumParallelRepetition.exactLocallySampleableLaw_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (t : ExactLocallySampleableTuple X Y A B D) : 0 ≤ exactLocallySampleableLaw G n S D t

theorem QuantumParallelRepetition.exactLocallySampleableLaw_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t = 1

theorem QuantumParallelRepetition.exactLocallySampleableLaw_eq_zero_of_question_zero {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (zero : G.questionWeight x y = 0) : exactLocallySampleableLaw G n S D (i, x, y, r) = 0

noncomputable def QuantumParallelRepetition.exactAliceLocalMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (x : X) : ℝ

The total probability mass of exact alice local.

Equations

• QuantumParallelRepetition.exactAliceLocalMass D Q i x = ∑ r : QuantumParallelRepetition.ExactHistoryFlag X Y A B D, ∑ y : Y, Q (i, x, y, r)

noncomputable def QuantumParallelRepetition.exactBobLocalMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (y : Y) : ℝ

The total probability mass of exact bob local.

Equations

• QuantumParallelRepetition.exactBobLocalMass D Q i y = ∑ r : QuantumParallelRepetition.ExactHistoryFlag X Y A B D, ∑ x : X, Q (i, x, y, r)

theorem QuantumParallelRepetition.exactAliceLocalMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) : 0 ≤ exactAliceLocalMass D Q i x

theorem QuantumParallelRepetition.exactBobLocalMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (y : Y) : 0 ≤ exactBobLocalMass D Q i y

noncomputable def QuantumParallelRepetition.exactAliceLocalConditional {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (x : X) (r : ExactHistoryFlag X Y A B D) : ℝ

The exact alice local conditional construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactBobLocalConditional {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (y : Y) (r : ExactHistoryFlag X Y A B D) : ℝ

The exact bob local conditional construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactAliceLocalConditional_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) (r : ExactHistoryFlag X Y A B D) : 0 ≤ exactAliceLocalConditional D base Q i x r

theorem QuantumParallelRepetition.exactBobLocalConditional_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (y : Y) (r : ExactHistoryFlag X Y A B D) : 0 ≤ exactBobLocalConditional D base Q i y r

theorem QuantumParallelRepetition.exactAliceLocalMass_zero_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (zero : exactAliceLocalMass D Q i x = 0) : Q (i, x, y, r) = 0

theorem QuantumParallelRepetition.exactBobLocalMass_zero_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (zero : exactBobLocalMass D Q i y = 0) : Q (i, x, y, r) = 0

theorem QuantumParallelRepetition.exactAliceLocalConditional_zero_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (zero : exactAliceLocalConditional D base Q i x r = 0) : Q (i, x, y, r) = 0

theorem QuantumParallelRepetition.exactBobLocalConditional_zero_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (zero : exactBobLocalConditional D base Q i y r = 0) : Q (i, x, y, r) = 0

theorem QuantumParallelRepetition.exactAliceLocalConditional_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (x : X) : ∑ r : ExactHistoryFlag X Y A B D, exactAliceLocalConditional D base Q i x r = 1

theorem QuantumParallelRepetition.exactBobLocalConditional_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (i : SourceRemainingCoordinate D) (y : Y) : ∑ r : ExactHistoryFlag X Y A B D, exactBobLocalConditional D base Q i y r = 1

noncomputable def QuantumParallelRepetition.exactLocallySampleableJA {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

The exact locally sampleable ja construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactLocallySampleableJB {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

The exact locally sampleable jb construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactLocallySampleableJA_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : 0 ≤ exactLocallySampleableJA G n S D base t

theorem QuantumParallelRepetition.exactLocallySampleableJB_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : 0 ≤ exactLocallySampleableJB G n S D base t

theorem QuantumParallelRepetition.exactLocallySampleableJA_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableJA G n S D base t = 1

theorem QuantumParallelRepetition.exactLocallySampleableJB_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableJB G n S D base t = 1

theorem QuantumParallelRepetition.exactLocallySampleableLaw_absolute_continuous_JA {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : exactLocallySampleableJA G n S D base t = 0 → exactLocallySampleableLaw G n S D t = 0

theorem QuantumParallelRepetition.exactLocallySampleableLaw_absolute_continuous_JB {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) (t : ExactLocallySampleableTuple X Y A B D) : exactLocallySampleableJB G n S D base t = 0 → exactLocallySampleableLaw G n S D t = 0

theorem QuantumParallelRepetition.exactLocallySampleableJA_pinsker {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) : Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) ≤ √(Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) / 2)

theorem QuantumParallelRepetition.exactLocallySampleableJB_pinsker {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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) (base : ExactHistoryFlag X Y A B D) : Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) ≤ √(Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) / 2)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactLocalSamplerIndex (X : Type u_5) (Y : Type u_6) {n : ℕ} (D : Finset (Fin n)) : Type (max u_5 u_6)

The type used to represent exact local sampler index in the exact sampling construction.

Equations

• QuantumParallelRepetition.ExactLocalSamplerIndex X Y D = (QuantumParallelRepetition.SourceRemainingCoordinate D × X ⊕ QuantumParallelRepetition.SourceRemainingCoordinate D × Y)

noncomputable def QuantumParallelRepetition.exactLocalConditionalFamily {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (k : ExactLocalSamplerIndex X Y D) (r : ExactHistoryFlag X Y A B D) : ℝ

The exact local conditional family construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactLocalConditionalFamily D base Q (Sum.inl (i, x)) r = QuantumParallelRepetition.exactAliceLocalConditional D base Q i x r
• QuantumParallelRepetition.exactLocalConditionalFamily D base Q (Sum.inr (i, y)) r = QuantumParallelRepetition.exactBobLocalConditional D base Q i y r

theorem QuantumParallelRepetition.exactLocalConditionalFamily_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t) (k : ExactLocalSamplerIndex X Y D) (r : ExactHistoryFlag X Y A B D) : 0 ≤ exactLocalConditionalFamily D base Q k r

theorem QuantumParallelRepetition.exactLocalConditionalFamily_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (base : ExactHistoryFlag X Y A B D) (Q : ExactLocallySampleableTuple X Y A B D → ℝ) (k : ExactLocalSamplerIndex X Y D) : ∑ r : ExactHistoryFlag X Y A B D, exactLocalConditionalFamily D base Q k r = 1

noncomputable def QuantumParallelRepetition.exactConditionalQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : ℝ

The probability weight for exact conditional question.

Equations

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

theorem QuantumParallelRepetition.exactFiberQuestionMass_eq_jointQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : exactFiberQuestionMass G n D seed history x y = exactJointQuestionMass G n D seed history x y

noncomputable def QuantumParallelRepetition.exactJointAliceCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (y : Y) (a : A) : Matrix S.Alice S.Alice ℂ

The spectral filter for exact joint alice coordinate.

Equations

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

noncomputable def QuantumParallelRepetition.exactJointBobCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) (y : Y) (b : B) : Matrix S.Bob S.Bob ℂ

The spectral filter for exact joint bob coordinate.

Equations

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

theorem QuantumParallelRepetition.exactJointCoordinateFilter_born {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (aliceAnswer : ↥D → A) (bobAnswer : ↥D → B) (x : X) (y : Y) (a : A) (b : B) (nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0) : ((bornTracePairing S.state.matrix) (exactJointAliceCoordinateFilter G n S D seed history aliceAnswer x y a)) (exactJointBobCoordinateFilter G n S D seed history bobAnswer x y b) = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (conditionedAliceCoordinateEffect G n S D aliceAnswer xs (↑seed.coordinate) a)) (conditionedBobCoordinateEffect G n S D bobAnswer ys (↑seed.coordinate) b)

noncomputable def QuantumParallelRepetition.exactJointConditionalWinningMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (aliceAnswer : ↥D → A) (bobAnswer : ↥D → B) (x : X) (y : Y) : ℝ

The total probability mass of exact joint conditional winning.

Equations

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

theorem QuantumParallelRepetition.exactJointConditionalWinningMass_born {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (aliceAnswer : ↥D → A) (bobAnswer : ↥D → B) (x : X) (y : Y) (nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0) : exactJointConditionalWinningMass G n S D seed history aliceAnswer bobAnswer x y = ∑ a : A, ∑ b : B, if G.predicate x y a b = true then ∑ xs : Fin n → X, ∑ ys : Fin n → Y, exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (conditionedAliceCoordinateEffect G n S D aliceAnswer xs (↑seed.coordinate) a)) (conditionedBobCoordinateEffect G n S D bobAnswer ys (↑seed.coordinate) b) else 0

theorem QuantumParallelRepetition.exactFiberQuestionWeight_sum_bobQuestion {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (xs : Fin n → X) (ys : Fin n → Y) : ∑ y : Y, exactFiberQuestionWeight G n D seed history x y xs ys = if exactRevealCode D seed (xs, ys) = history ∧ xs ↑seed.coordinate = x then exactPriorQuestionWeight G n (xs, ys) else 0

theorem QuantumParallelRepetition.exactFiberQuestionWeight_sum_aliceQuestion {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : ∑ x : X, exactFiberQuestionWeight G n D seed history x y xs ys = if exactRevealCode D seed (xs, ys) = history ∧ ys ↑seed.coordinate = y then exactPriorQuestionWeight G n (xs, ys) else 0

theorem QuantumParallelRepetition.exactAliceQuestionMass_eq_sum_fiberMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) : exactAliceQuestionMass G n D seed history x = ∑ y : Y, exactFiberQuestionMass G n D seed history x y

theorem QuantumParallelRepetition.exactBobQuestionMass_eq_sum_fiberMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) : exactBobQuestionMass G n D seed history y = ∑ x : X, exactFiberQuestionMass G n D seed history x y

theorem QuantumParallelRepetition.exactCompatible_aliceMixed_coordinate_eq_or {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y y' : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y' ys') (j : Fin n) : xs j = xs' j ∨ ys j = ys' j

theorem QuantumParallelRepetition.exactQuestionWeight_aliceMixed_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y y' : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y' ys') : (G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys

theorem QuantumParallelRepetition.exactFiberQuestionWeight_aliceMixed_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y y' : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) : exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x y' xs' ys' = exactFiberQuestionWeight G n D seed history x y' xs ys' * exactFiberQuestionWeight G n D seed history x y xs' ys

theorem QuantumParallelRepetition.exactCompatible_bobMixed_coordinate_eq_or {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x x' : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x' xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') (j : Fin n) : xs j = xs' j ∨ ys j = ys' j

theorem QuantumParallelRepetition.exactQuestionWeight_bobMixed_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x x' : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x' xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') : (G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys

theorem QuantumParallelRepetition.exactFiberQuestionWeight_bobMixed_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x x' : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) : exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x' y xs' ys' = exactFiberQuestionWeight G n D seed history x y xs ys' * exactFiberQuestionWeight G n D seed history x' y xs' ys

theorem QuantumParallelRepetition.exactMixedRowMarginal_mul_total {ι : Type u_5} {κ : Type u_6} [Fintype ι] [Fintype κ] (left right : ι → κ → ℝ) (rectangle : ∀ (i i' : ι) (j j' : κ), left i j * right i' j' = right i j' * left i' j) (i : ι) : (∑ j : κ, left i j) * ∑ i' : ι, ∑ j' : κ, right i' j' = (∑ j' : κ, right i j') * ∑ i' : ι, ∑ j : κ, left i' j

theorem QuantumParallelRepetition.exactFiberQuestionWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : 0 ≤ exactFiberQuestionWeight G n D seed history x y xs ys

theorem QuantumParallelRepetition.exactFiberQuestionMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : 0 ≤ exactFiberQuestionMass G n D seed history x y

theorem QuantumParallelRepetition.exactAliceCoordinateFilter_eq_joint {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (y : Y) (a : A) (nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0) : exactAliceCoordinateFilter G n S D seed history answer x a = exactJointAliceCoordinateFilter G n S D seed history answer x y a

theorem QuantumParallelRepetition.exactBobCoordinateFilter_eq_joint {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) (y : Y) (b : B) (nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0) : exactBobCoordinateFilter G n S D seed history answer y b = exactJointBobCoordinateFilter G n S D seed history answer x y b

theorem QuantumParallelRepetition.exactSourceEquationTen {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (aliceAnswer : ↥D → A) (bobAnswer : ↥D → B) (x : X) (y : Y) (nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0) : ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D seed history aliceAnswer x)) (exactBobQuestionFilter G n S D seed history bobAnswer y) = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D aliceAnswer xs)) (conditionedBobEffect G n S D bobAnswer ys)