Quantum parallel repetition, part 01

@[instance_reducible]

noncomputable def QuantumParallelRepetition.matrixComplexContinuousENormPartOne {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : ContinuousENorm (Matrix m n ℂ)

The local matrix norm instance used while elaborating part one.

Equations

• QuantumParallelRepetition.matrixComplexContinuousENormPartOne = SeminormedAddGroup.toContinuousENorm

@[instance_reducible]

noncomputable def QuantumParallelRepetition.matrixComplexESeminormedAddCommMonoidPartOne {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : ESeminormedAddCommMonoid (Matrix m n ℂ)

The local matrix norm instance used while elaborating part one.

Equations

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

structure QuantumParallelRepetition.Game (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (max (max (max u_5 u_6) u_7) u_8)

A finite two-player nonlocal game with a question distribution and winning predicate.

• questionWeight : X → Y → ℝ

  The probability weight assigned to a pair of questions.

• weight_nonneg (x : X) (y : Y) : 0 ≤ self.questionWeight x y
• weight_normalized : ∑ x : X, ∑ y : Y, self.questionWeight x y = 1
• predicate : X → Y → A → B → Bool

  The Boolean predicate deciding whether a pair of answers wins.

def QuantumParallelRepetition.Game.marginalX {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) (x : X) : ℝ

The first-question marginal of a game.

Equations

• G.marginalX x = ∑ y : Y, G.questionWeight x y

def QuantumParallelRepetition.Game.marginalY {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) (y : Y) : ℝ

The second-question marginal of a game.

Equations

• G.marginalY y = ∑ x : X, G.questionWeight x y

theorem QuantumParallelRepetition.Game.marginalX_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) (x : X) : 0 ≤ G.marginalX x

theorem QuantumParallelRepetition.Game.marginalY_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) (y : Y) : 0 ≤ G.marginalY y

theorem QuantumParallelRepetition.Game.marginalX_normalized {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) : ∑ x : X, G.marginalX x = 1

theorem QuantumParallelRepetition.Game.marginalY_normalized {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) : ∑ y : Y, G.marginalY y = 1

def QuantumParallelRepetition.Game.repeat {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 : ℕ) : Game (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

The coordinatewise repeated game.

Equations

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

@[simp]

theorem QuantumParallelRepetition.Game.repeat_questionWeight {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 : ℕ) (xs : Fin n → X) (ys : Fin n → Y) : (G.repeat n).questionWeight xs ys = ∏ i : Fin n, G.questionWeight (xs i) (ys i)

@[simp]

theorem QuantumParallelRepetition.Game.repeat_predicate_eq_true {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 : ℕ) (xs : Fin n → X) (ys : Fin n → Y) (as : Fin n → A) (bs : Fin n → B) : (G.repeat n).predicate xs ys as bs = true ↔ ∀ (i : Fin n), G.predicate (xs i) (ys i) (as i) (bs i) = true

structure QuantumParallelRepetition.DensityMatrix (d : Type u_5) [Fintype d] : Type u_5

A finite-dimensional positive semidefinite matrix of trace one.

• matrix : Matrix d d ℂ

  The matrix underlying a density matrix.

• positive : self.matrix.PosSemidef
• trace_one : self.matrix.trace = 1

structure QuantumParallelRepetition.POVM (ι : Type u_5) (d : Type u_6) [Fintype ι] [Fintype d] [DecidableEq d] : Type (max u_5 u_6)

A finite-outcome positive operator-valued measurement.

• effect : ι → Matrix d d ℂ

  The positive operator associated with a measurement outcome.

• positive (i : ι) : (self.effect i).PosSemidef
• complete : ∑ i : ι, self.effect i = 1

structure QuantumParallelRepetition.Strategy {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) : Type (max (max (max (max 1 u_1) u_2) u_3) u_4)

A finite-dimensional entangled strategy for a nonlocal game.

• Alice : Type

  Alice's finite Hilbert-space basis type.

• Bob : Type

  Bob's finite Hilbert-space basis type.

• aliceFintype : Fintype self.Alice
• bobFintype : Fintype self.Bob
• aliceDecidableEq : DecidableEq self.Alice
• bobDecidableEq : DecidableEq self.Bob
• state : DensityMatrix (self.Alice × self.Bob)

  The shared bipartite state of the strategy.

• aliceMeasurement : X → POVM A self.Alice

  Alice's measurement for each question.

• bobMeasurement : Y → POVM B self.Bob

  Bob's measurement for each question.

theorem QuantumParallelRepetition.trace_mul_posSemidef_nonneg {d : Type u_5} [Fintype d] {R E : Matrix d d ℂ} (hR : R.PosSemidef) (hE : E.PosSemidef) : 0 ≤ (R * E).trace.re

def QuantumParallelRepetition.Strategy.outcomeProbability {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) (x : X) (y : Y) (a : A) (b : B) : ℝ

The Born probability of a question-and-answer outcome.

Equations

• S.outcomeProbability x y a b = (S.state.matrix * QuantumParallelRepetition.Strategy.jointEffect✝ S x y a b).trace.re

theorem QuantumParallelRepetition.Strategy.outcomeProbability_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} (S : Strategy G) (x : X) (y : Y) (a : A) (b : B) : 0 ≤ S.outcomeProbability x y a b

theorem QuantumParallelRepetition.Strategy.outcomeProbability_normalized {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) (x : X) (y : Y) : ∑ a : A, ∑ b : B, S.outcomeProbability x y a b = 1

def QuantumParallelRepetition.Strategy.winProbability {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) : ℝ

The winning probability of the strategy.

Equations

• S.winProbability = ∑ x : X, ∑ y : Y, G.questionWeight x y * ∑ a : A, ∑ b : B, if G.predicate x y a b = true then S.outcomeProbability x y a b else 0

theorem QuantumParallelRepetition.Strategy.winProbability_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} (S : Strategy G) : 0 ≤ S.winProbability

theorem QuantumParallelRepetition.Strategy.winProbability_le_one {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) : S.winProbability ≤ 1

noncomputable def QuantumParallelRepetition.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) : ℝ

The supremal winning probability over finite-dimensional entangled strategies.

Equations

• QuantumParallelRepetition.entangledValue G = sSup (Set.range QuantumParallelRepetition.Strategy.winProbability)

theorem QuantumParallelRepetition.winProbabilities_bddAbove {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) : BddAbove (Set.range Strategy.winProbability)

theorem QuantumParallelRepetition.entangledValue_le_one {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) : entangledValue G ≤ 1

theorem QuantumParallelRepetition.entangledValue_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) : 0 ≤ entangledValue G

noncomputable def QuantumParallelRepetition.repeatedEntangledValue {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 : ℕ) : ℝ

The entangled value of a coordinatewise repeated game.

Equations

• QuantumParallelRepetition.repeatedEntangledValue G n = QuantumParallelRepetition.entangledValue (G.repeat n)

noncomputable def QuantumParallelRepetition.quadraticExpectation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H →L[ℂ] H) (z : H) : ℝ

The quadratic expectation construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.quadraticExpectation W z = (inner ℂ z (W z)).re

theorem QuantumParallelRepetition.positive_quadraticExpectation_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H →L[ℂ] H) (hW : W.IsPositive) (z : H) : 0 ≤ quadraticExpectation W z

theorem QuantumParallelRepetition.positive_complement_quadraticExpectation_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H →L[ℂ] H) (h_complement : (1 - W).IsPositive) (z : H) : quadraticExpectation W z ≤ ‖z‖ ^ 2

theorem QuantumParallelRepetition.norm_le_of_operator_contraction {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H →L[ℂ] H) (hW : ‖W‖ ≤ 1) (z : H) : ‖W z‖ ≤ ‖z‖

theorem QuantumParallelRepetition.quadraticExpectation_sub_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (W : H →L[ℂ] H) (hW : ‖W‖ ≤ 1) (z w : H) : |quadraticExpectation W z - quadraticExpectation W w| ≤ (‖z‖ + ‖w‖) * ‖z - w‖

theorem QuantumParallelRepetition.weighted_real_cauchy {ι : Type u_2} [Fintype ι] (weight f g : ι → ℝ) (h_weight : ∀ (i : ι), 0 ≤ weight i) : ∑ i : ι, weight i * f i * g i ≤ √(∑ i : ι, weight i * f i ^ 2) * √(∑ i : ι, weight i * g i ^ 2)

theorem QuantumParallelRepetition.matrixEffectCLM_isPositive {d : Type u_1} [Fintype d] [DecidableEq d] (E : Matrix d d ℂ) (hE : E.PosSemidef) : (Matrix.toEuclideanCLM E).IsPositive

theorem QuantumParallelRepetition.matrixEffectCLM_complement_isPositive {d : Type u_1} [Fintype d] [DecidableEq d] (E : Matrix d d ℂ) (hE : (1 - E).PosSemidef) : (1 - Matrix.toEuclideanCLM E).IsPositive

def QuantumParallelRepetition.Strategy.winningEffect {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) (x : X) (y : Y) : Matrix (S.Alice × S.Bob) (S.Alice × S.Bob) ℂ

The measurement effect for winning.

Equations

• S.winningEffect x y = ∑ a : A, ∑ b : B, if G.predicate x y a b = true then QuantumParallelRepetition.Strategy.jointEffect✝ S x y a b else 0

theorem QuantumParallelRepetition.Strategy.winningEffect_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} (S : Strategy G) (x : X) (y : Y) : (S.state.matrix * S.winningEffect x y).trace.re = ∑ a : A, ∑ b : B, if G.predicate x y a b = true then S.outcomeProbability x y a b else 0

theorem QuantumParallelRepetition.Strategy.winProbability_eq_winningEffect_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} (S : Strategy G) : S.winProbability = ∑ x : X, ∑ y : Y, G.questionWeight x y * (S.state.matrix * S.winningEffect x y).trace.re

theorem QuantumParallelRepetition.posSemidef_blockDiagonal' {ι : Type u_5} [Finite ι] [DecidableEq ι] {d : ι → Type u_6} [∀ (j : ι), Finite (d j)] (M : (j : ι) → Matrix (d j) (d j) ℂ) (hM : ∀ (j : ι), (M j).PosSemidef) : (Matrix.blockDiagonal' M).PosSemidef

def QuantumParallelRepetition.pureDensityMatrix {d : Type u_1} [Fintype d] (z : EuclideanSpace ℂ d) (hz : ‖z‖ = 1) : DensityMatrix d

The matrix representation of pure density.

Equations

• QuantumParallelRepetition.pureDensityMatrix z hz = { matrix := Matrix.vecMulVec z.ofLp (star z.ofLp), positive := ⋯, trace_one := ⋯ }

theorem QuantumParallelRepetition.pureDensityMatrix_trace_mul {d : Type u_1} [Fintype d] [DecidableEq d] (z : EuclideanSpace ℂ d) (hz : ‖z‖ = 1) (E : Matrix d d ℂ) : ((pureDensityMatrix z hz).matrix * E).trace.re = quadraticExpectation (Matrix.toEuclideanCLM E) z

def QuantumParallelRepetition.pureVectorStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {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) : Strategy G

The strategy implementing pure vector.

Equations

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

theorem QuantumParallelRepetition.pureVectorStrategy_outcomeProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {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) (a : A) (b : B) : (pureVectorStrategy G z hz PA PB).outcomeProbability x y a b = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((PA x).effect a) ((PB y).effect b))) z

noncomputable def QuantumParallelRepetition.pureFlaggedStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {dA dB J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [Fintype J] [DecidableEq J] (G : Game X Y A B) (p : J → ℝ) (hp : ∀ (j : J), 0 ≤ p j) (h_normalized : ∑ j : J, p j = 1) (z : J → EuclideanSpace ℂ (dA × dB)) (hz : ∀ (j : J), ‖z j‖ = 1) (PA : J → X → POVM A dA) (PB : J → Y → POVM B dB) : Strategy G

The strategy implementing pure flagged.

Equations

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

theorem QuantumParallelRepetition.pureFlaggedStrategy_winProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {dA dB J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] [Fintype J] [DecidableEq J] (G : Game X Y A B) (p : J → ℝ) (hp : ∀ (j : J), 0 ≤ p j) (h_normalized : ∑ j : J, p j = 1) (z : J → EuclideanSpace ℂ (dA × dB)) (hz : ∀ (j : J), ‖z j‖ = 1) (PA : J → X → POVM A dA) (PB : J → Y → POVM B dB) : (pureFlaggedStrategy G p hp h_normalized z hz PA PB).winProbability = ∑ j : J, p j * (pureVectorStrategy G (z j) ⋯ (PA j) (PB j)).winProbability

structure QuantumParallelRepetition.FiniteEventLaw (Ω : Type u_1) [Fintype Ω] : Type u_1

A normalized nonnegative probability law on a finite sample space.

• weight : Ω → ℝ

  The probability weight of a sample point.

• weight_nonneg (ω : Ω) : 0 ≤ self.weight ω
• weight_sum : ∑ ω : Ω, self.weight ω = 1

def QuantumParallelRepetition.FiniteEventLaw.eventMass {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) : ℝ

The probability mass of a finite event.

Equations

• law.eventMass event = ∑ ω ∈ event, law.weight ω

theorem QuantumParallelRepetition.FiniteEventLaw.eventMass_univ {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) : law.eventMass Finset.univ = 1

theorem QuantumParallelRepetition.FiniteEventLaw.eventMass_mono {Ω : Type u_1} [Fintype Ω] (law : FiniteEventLaw Ω) {s t : Finset Ω} (h : s ⊆ t) : law.eventMass s ≤ law.eventMass t

def QuantumParallelRepetition.FiniteEventLaw.winEvent {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] (wins : ι → Ω → Bool) (D : Finset ι) : Finset Ω

The event on which every selected coordinate wins.

Equations

• QuantumParallelRepetition.FiniteEventLaw.winEvent wins D = {ω : Ω | ∀ i ∈ D, wins i ω = true}

theorem QuantumParallelRepetition.FiniteEventLaw.mem_winEvent_iff {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] (wins : ι → Ω → Bool) (D : Finset ι) (ω : Ω) : ω ∈ winEvent wins D ↔ ∀ i ∈ D, wins i ω = true

Membership in a finite-law win event is pointwise winning at every selected index.

theorem QuantumParallelRepetition.FiniteEventLaw.winEvent_empty {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] (wins : ι → Ω → Bool) : winEvent wins ∅ = Finset.univ

theorem QuantumParallelRepetition.FiniteEventLaw.winEvent_antitone {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] (wins : ι → Ω → Bool) {D E : Finset ι} (h : D ⊆ E) : winEvent wins E ⊆ winEvent wins D

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

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

The conditional mass of failure at a selected coordinate.

Equations

• law.failureMass wins D i = law.eventMass (QuantumParallelRepetition.FiniteEventLaw.winEvent wins D) - law.eventMass (QuantumParallelRepetition.FiniteEventLaw.winEvent wins (insert i D))

theorem QuantumParallelRepetition.FiniteEventLaw.exists_greedy_stopping {ι : Type u_2} [Fintype ι] [DecidableEq ι] (mass : Finset ι → ℝ) {θ η : ℝ} {T : ℕ} (hη_one : η ≤ 1) (hT : T ≤ Fintype.card ι) (hempty : mass ∅ = 1) (hfloor : ∀ (D : Finset ι), θ ≤ mass D) (h_terminal : (1 - η) ^ T < θ) : ∃ (D : Finset ι), D.card < T ∧ θ ≤ mass D ∧ ∑ i ∈ Finset.univ \ D, (mass D - mass (insert i D)) < ↑(Finset.univ \ D).card * (η * mass D)

theorem QuantumParallelRepetition.FiniteEventLaw.exists_conditioned_win_set {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] [DecidableEq ι] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) {θ η : ℝ} {T : ℕ} (hη_one : η ≤ 1) (hT : T ≤ Fintype.card ι) (hwin : θ ≤ law.eventMass (winEvent wins Finset.univ)) (h_terminal : (1 - η) ^ T < θ) : ∃ (D : Finset ι), D.card < T ∧ θ ≤ law.eventMass (winEvent wins D) ∧ ∑ i ∈ Finset.univ \ D, law.failureMass wins D i < ↑(Finset.univ \ D).card * (η * law.eventMass (winEvent wins D))

@[reducible, inline]

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

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

Equations

• QuantumParallelRepetition.StrategyOutcome X Y A B = (X × Y × A × B)

def QuantumParallelRepetition.strategyEventLaw {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) : FiniteEventLaw (StrategyOutcome X Y A B)

The finite probability law for strategy event.

Equations

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

def QuantumParallelRepetition.repeatedCoordinateWin {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 : ℕ) (i : Fin n) (ω : StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) : Bool

The repeated coordinate win construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.repeatedCoordinateWin G n i ω = G.predicate (ω.1 i) (ω.2.1 i) (ω.2.2.1 i) (ω.2.2.2 i)

theorem QuantumParallelRepetition.repeated_allWinMass_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)) : (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) Finset.univ) = S.winProbability

theorem QuantumParallelRepetition.repeatedStrategy_exists_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)) {θ η : ℝ} {T : ℕ} (hη_one : η ≤ 1) (hT : T ≤ n) (hwin : θ ≤ S.winProbability) (h_terminal : (1 - η) ^ T < θ) : ∃ (D : Finset (Fin n)), D.card < T ∧ θ ≤ (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.negMulLog_rescale {W p : ℝ} (hW : 0 < W) (hp : 0 < p) : W * (p / W).negMulLog = p * Real.log (W / p)

theorem QuantumParallelRepetition.finite_weighted_entropy_le {ι : Type u_1} (s : Finset ι) (w h : ι → ℝ) {W p : ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hh : ∀ i ∈ s, 0 ≤ h i) (hW : 0 < W) (hp : 0 < p) (hw_sum : ∑ i ∈ s, w i = W) (hp_sum : ∑ i ∈ s, w i * h i = p) : ∑ i ∈ s, w i * (h i).negMulLog ≤ p * Real.log (W / p)

theorem QuantumParallelRepetition.finite_weighted_entropy_le_of_weight_bound {ι : Type u_1} (s : Finset ι) (w h : ι → ℝ) {W N p : ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hh : ∀ i ∈ s, 0 ≤ h i) (hW : 0 < W) (hp : 0 < p) (hw_sum : ∑ i ∈ s, w i = W) (hp_sum : ∑ i ∈ s, w i * h i = p) (hWN : W ≤ N) : ∑ i ∈ s, w i * (h i).negMulLog ≤ p * Real.log (N / p)

theorem QuantumParallelRepetition.noncommutative_resolvent_identity {R : Type u_1} [Ring R] (F M S RF RM : R) (hF : RF * (F + S) = 1) (hM : (M + S) * RM = 1) : RF - RM = RF * (M - F) * RM

theorem QuantumParallelRepetition.noncommutative_filtered_resolvent_identity {R : Type u_1} [Ring R] (F M S RF RM : R) (hF_left : (F + S) * RF = 1) (hF_right : RF * (F + S) = 1) (hM_left : (M + S) * RM = 1) : F * RF - M * RM = S * (RF * (F - M) * RM)

theorem QuantumParallelRepetition.noncommutative_resolvent_second_order {R : Type u_1} [Ring R] (F M S RF RM : R) (hF_left : (F + S) * RF = 1) (hF_right : RF * (F + S) = 1) (hM_left : (M + S) * RM = 1) (hM_right : RM * (M + S) = 1) : RF = RM - RM * (F - M) * RM + RM * (F - M) * RF * (F - M) * RM

theorem QuantumParallelRepetition.noncommutative_weighted_resolvent_second_order {ι : Type u_1} {R : Type u_2} [Fintype ι] [Ring R] (weight F : ι → R) (M S : R) (RF : ι → R) (RM : R) (normalized : ∑ i : ι, weight i = 1) (centered : ∑ i : ι, weight i * (F i - M) = 0) (commute_mean : ∀ (i : ι), weight i * RM = RM * weight i) (hF_left : ∀ (i : ι), (F i + S) * RF i = 1) (hF_right : ∀ (i : ι), RF i * (F i + S) = 1) (hM_left : (M + S) * RM = 1) (hM_right : RM * (M + S) = 1) : ∑ i : ι, weight i * RF i - RM = (RM * ∑ i : ι, weight i * ((F i - M) * RF i * (F i - M))) * RM

theorem QuantumParallelRepetition.posSemidef_hermitian_sandwich {d : Type u_1} [Fintype d] {A D : Matrix d d ℂ} (hA : A.PosSemidef) (hD : D.IsHermitian) : (D * A * D).PosSemidef

theorem QuantumParallelRepetition.shifted_posSemidef_matrix_posDef {d : Type u_1} [DecidableEq d] {F : Matrix d d ℂ} (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : (F + s • 1).PosDef

theorem QuantumParallelRepetition.shifted_posSemidef_matrix_inverse_posSemidef {d : Type u_1} [Fintype d] [DecidableEq d] {F : Matrix d d ℂ} (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : (F + s • 1)⁻¹.PosSemidef

theorem QuantumParallelRepetition.matrix_weighted_centered {ι : Type u_1} {d : Type u_2} [Fintype ι] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) : ∑ i : ι, weight i • (F i - M) = 0

theorem QuantumParallelRepetition.weighted_positive_matrix_mean {ι : Type u_1} {d : Type u_2} [Fintype ι] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (positive : ∀ (i : ι), (F i).PosSemidef) : (∑ i : ι, weight i • F i).PosSemidef

theorem QuantumParallelRepetition.scalar_resolvent_purification_integrable_of_pos {z : ℝ} (hz : 0 < z) : MeasureTheory.IntegrableOn (fun (s : ℝ) => (z / (z + s)) ^ 2) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.scalar_resolvent_purification_integrable {z : ℝ} (hz : 0 ≤ z) : MeasureTheory.IntegrableOn (fun (s : ℝ) => (z / (z + s)) ^ 2) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.scalar_resolvent_purification_integral {z : ℝ} (hz : 0 ≤ z) : ∫ (s : ℝ) in Set.Ioi 0, (z / (z + s)) ^ 2 = z

noncomputable def QuantumParallelRepetition.spectralConjugationCLM {d : Type u_1} [Fintype d] [DecidableEq d] (U : ↥(Matrix.unitaryGroup d ℂ)) : Matrix d d ℂ →L[ℝ] Matrix d d ℂ

The continuous linear map implementing spectral conjugation.

Equations

• QuantumParallelRepetition.spectralConjugationCLM U = LinearMap.toContinuousLinearMap ↑↑((Unitary.conjStarAlgAut ℝ (Matrix d d ℂ)) U).toAlgEquiv

@[simp]

theorem QuantumParallelRepetition.spectralConjugationCLM_apply {d : Type u_1} [Fintype d] [DecidableEq d] (U : ↥(Matrix.unitaryGroup d ℂ)) (A : Matrix d d ℂ) : (spectralConjugationCLM U) A = ↑U * A * star ↑U

noncomputable def QuantumParallelRepetition.spectralPurificationFilter {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : ℝ) : Matrix d d ℂ

The spectral filter for spectral purification.

Equations

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

theorem QuantumParallelRepetition.integral_spectralPurificationFilter_gram {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter F hF s) * spectralPurificationFilter F hF s = F

theorem QuantumParallelRepetition.spectralPurificationFilter_gram_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : MeasureTheory.IntegrableOn (fun (s : ℝ) => star (spectralPurificationFilter F hF s) * spectralPurificationFilter F hF s) (Set.Ioi 0) MeasureTheory.volume

def QuantumParallelRepetition.bornTracePairing {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] (ρ : Matrix (dA × dB) (dA × dB) ℂ) : Matrix dA dA ℂ →ₗ[ℝ] Matrix dB dB ℂ →ₗ[ℝ] ℝ

The born trace pairing construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.Game.questionWeight_le_marginalX {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) (x : X) (y : Y) : G.questionWeight x y ≤ G.marginalX x

theorem QuantumParallelRepetition.Game.questionWeight_le_marginalY {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) (x : X) (y : Y) : G.questionWeight x y ≤ G.marginalY y

noncomputable def QuantumParallelRepetition.Game.conditionalYGivenX {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) (x : X) (y : Y) : ℝ

The conditional y given x construction used in the quantum parallel-repetition argument.

Equations

• G.conditionalYGivenX x y = G.questionWeight x y / G.marginalX x

noncomputable def QuantumParallelRepetition.Game.conditionalXGivenY {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) (y : Y) (x : X) : ℝ

The conditional x given y construction used in the quantum parallel-repetition argument.

Equations

• G.conditionalXGivenY y x = G.questionWeight x y / G.marginalY y

theorem QuantumParallelRepetition.Game.conditionalYGivenX_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) (x : X) (y : Y) : 0 ≤ G.conditionalYGivenX x y

theorem QuantumParallelRepetition.Game.conditionalXGivenY_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) (y : Y) (x : X) : 0 ≤ G.conditionalXGivenY y x

theorem QuantumParallelRepetition.Game.marginalX_mul_conditionalYGivenX {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) (x : X) (y : Y) : G.marginalX x * G.conditionalYGivenX x y = G.questionWeight x y

theorem QuantumParallelRepetition.Game.marginalY_mul_conditionalXGivenY {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) (x : X) (y : Y) : G.marginalY y * G.conditionalXGivenY y x = G.questionWeight x y

theorem QuantumParallelRepetition.Game.conditionalYGivenX_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) (x : X) (hx : 0 < G.marginalX x) : ∑ y : Y, G.conditionalYGivenX x y = 1

theorem QuantumParallelRepetition.Game.conditionalXGivenY_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) (y : Y) (hy : 0 < G.marginalY y) : ∑ x : X, G.conditionalXGivenY y x = 1

noncomputable def QuantumParallelRepetition.conditionalBobAverage {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {V : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [AddCommGroup V] [Module ℝ V] (G : Game X Y A B) (K : Y → V) (x : X) : V

The finite average of conditional bob.

Equations

• QuantumParallelRepetition.conditionalBobAverage G K x = ∑ y : Y, G.conditionalYGivenX x y • K y

noncomputable def QuantumParallelRepetition.conditionalAliceAverage {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {U : Type u_5} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [AddCommGroup U] [Module ℝ U] (G : Game X Y A B) (H : X → U) (y : Y) : U

The finite average of conditional alice.

Equations

• QuantumParallelRepetition.conditionalAliceAverage G H y = ∑ x : X, G.conditionalXGivenY y x • H x

theorem QuantumParallelRepetition.alice_mixed_history_pairing {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {U : Type u_5} {V : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (G : Game X Y A B) (pair : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H : X → U) (K : Y → V) : ∑ x : X, G.marginalX x * (pair (H x)) (conditionalBobAverage G K x) = ∑ x : X, ∑ y : Y, G.questionWeight x y * (pair (H x)) (K y)

theorem QuantumParallelRepetition.bob_mixed_history_pairing {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {U : Type u_5} {V : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (G : Game X Y A B) (pair : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H : X → U) (K : Y → V) : ∑ y : Y, G.marginalY y * (pair (conditionalAliceAverage G H y)) (K y) = ∑ x : X, ∑ y : Y, G.questionWeight x y * (pair (H x)) (K y)

theorem QuantumParallelRepetition.alice_reveal_increment {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {U : Type u_5} {V : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] (G : Game X Y A B) (pair : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (H : X → U) (M : Y → U) (K : Y → V) (f : U → U) : ∑ x : X, G.marginalX x * (pair (f (H x))) (conditionalBobAverage G K x) - ∑ y : Y, G.marginalY y * (pair (f (M y))) (K y) = ∑ y : Y, G.marginalY y * (pair (conditionalAliceAverage G (fun (x : X) => f (H x)) y - f (M y))) (K y)

noncomputable def QuantumParallelRepetition.conditionedAliceEffect {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) : Matrix S.Alice S.Alice ℂ

The measurement effect for conditioned alice.

Equations

• QuantumParallelRepetition.conditionedAliceEffect G n S D α xs = ∑ answers : Fin n → A, if ∀ (i : Fin n) (hi : i ∈ D), answers i = α ⟨i, hi⟩ then (S.aliceMeasurement xs).effect answers else 0

noncomputable def QuantumParallelRepetition.conditionedBobEffect {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) : Matrix S.Bob S.Bob ℂ

The measurement effect for conditioned bob.

Equations

• QuantumParallelRepetition.conditionedBobEffect G n S D β ys = ∑ answers : Fin n → B, if ∀ (i : Fin n) (hi : i ∈ D), answers i = β ⟨i, hi⟩ then (S.bobMeasurement ys).effect answers else 0

theorem QuantumParallelRepetition.conditionedAliceEffect_positive {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) : (conditionedAliceEffect G n S D α xs).PosSemidef

theorem QuantumParallelRepetition.conditionedBobEffect_positive {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) : (conditionedBobEffect G n S D β ys).PosSemidef

theorem QuantumParallelRepetition.conditionedAliceEffect_complement_positive {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) : (1 - conditionedAliceEffect G n S D α xs).PosSemidef

theorem QuantumParallelRepetition.conditionedBobEffect_complement_positive {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) : (1 - conditionedBobEffect G n S D β ys).PosSemidef

theorem QuantumParallelRepetition.history_forward_telescope (E : ℕ → ℝ) (m : ℕ) : ∑ k ∈ Finset.range m, (E (k + 1) - E k) = E m - E 0

noncomputable def QuantumParallelRepetition.spectralSupportFunctional {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (f : ℝ → ℝ) : Matrix d d ℂ

The spectral support functional construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.spectralSupportFunctional F hF f = ((Unitary.conjStarAlgAut ℂ (Matrix d d ℂ)) ⋯.eigenvectorUnitary) (Matrix.diagonal fun (i : d) => ↑(f (⋯.eigenvalues i)))

theorem QuantumParallelRepetition.spectralSupportFunctional_mul {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (f g : ℝ → ℝ) : spectralSupportFunctional F hF f * spectralSupportFunctional F hF g = spectralSupportFunctional F hF fun (x : ℝ) => f x * g x

theorem QuantumParallelRepetition.spectralSupportFunctional_id {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : (spectralSupportFunctional F hF fun (x : ℝ) => x) = F

theorem QuantumParallelRepetition.spectralSupportFunctional_congr {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {f g : ℝ → ℝ} (h : ∀ (i : d), f (⋯.eigenvalues i) = g (⋯.eigenvalues i)) : spectralSupportFunctional F hF f = spectralSupportFunctional F hF g

theorem QuantumParallelRepetition.spectralSupportFunctional_isHermitian {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (f : ℝ → ℝ) : (spectralSupportFunctional F hF f).IsHermitian

noncomputable def QuantumParallelRepetition.spectralSupportSqrt {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : Matrix d d ℂ

The positive square-root construction for spectral support.

Equations

• QuantumParallelRepetition.spectralSupportSqrt F hF = QuantumParallelRepetition.spectralSupportFunctional F hF Real.sqrt

theorem QuantumParallelRepetition.spectralSupportSqrt_sq {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : spectralSupportSqrt F hF * spectralSupportSqrt F hF = F

theorem QuantumParallelRepetition.posSemidef_kernel_of_sub_posSemidef {d : Type u_1} [Fintype d] {F A : Matrix d d ℂ} (hA : A.PosSemidef) (hsub : (F - A).PosSemidef) {x : d → ℂ} (hx : F.mulVec x = 0) : A.mulVec x = 0

theorem QuantumParallelRepetition.refinement_complement_posSemidef {ι : Type u_1} {d : Type u_2} [Fintype ι] (effect : ι → Matrix d d ℂ) (hpositive : ∀ (a : ι), (effect a).PosSemidef) (a : ι) : (∑ b : ι, effect b - effect a).PosSemidef

noncomputable def QuantumParallelRepetition.purifiedRefinedPOVM {ι : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) (effect : ι → Matrix d d ℂ) (hpositive : ∀ (a : ι), (effect a).PosSemidef) (hsum : ∑ a : ι, effect a = F) (a₀ : ι) : POVM ι e

The positive operator-valued measurement implementing purified refined.

Equations

• QuantumParallelRepetition.purifiedRefinedPOVM F hF Γ hΓ effect hpositive hsum a₀ = { effect := QuantumParallelRepetition.purifiedRefinedEffect✝ F hF Γ effect a₀, positive := ⋯, complete := ⋯ }

theorem QuantumParallelRepetition.purifiedRefinedPOVM_compression {ι : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) (effect : ι → Matrix d d ℂ) (hpositive : ∀ (a : ι), (effect a).PosSemidef) (hsum : ∑ a : ι, effect a = F) (a₀ a : ι) : Γ.conjTranspose * (purifiedRefinedPOVM F hF Γ hΓ effect hpositive hsum a₀).effect a * Γ = effect a

def QuantumParallelRepetition.fullHistoryRemaining (n : ℕ) (D L : Finset (Fin n)) : Finset (Fin n)

The set of coordinates remaining after full history.

Equations

• QuantumParallelRepetition.fullHistoryRemaining n D L = (Finset.univ \ D) \ L

structure QuantumParallelRepetition.FullSubsetHistory (X : Type u_1) (Y : Type u_2) (n : ℕ) (D L : Finset (Fin n)) : Type (max u_1 u_2)

A partial transcript split into conditioned, revealed, and remaining coordinates.

• aliceConditioned : ↥D → X

  Alice's questions on conditioned coordinates.

• bobConditioned : ↥D → Y

  Bob's questions on conditioned coordinates.

• aliceRevealed : ↥L → X

  Alice's questions on revealed coordinates.

• bobRemaining : ↥(fullHistoryRemaining n D L) → Y

  Bob's questions on the remaining coordinates.

theorem QuantumParallelRepetition.FullSubsetHistory.ext {X : Type u_1} {Y : Type u_2} {n : ℕ} {D L : Finset (Fin n)} {x y : FullSubsetHistory X Y n D L} (aliceConditioned : x.aliceConditioned = y.aliceConditioned) (bobConditioned : x.bobConditioned = y.bobConditioned) (aliceRevealed : x.aliceRevealed = y.aliceRevealed) (bobRemaining : x.bobRemaining = y.bobRemaining) : x = y

@[instance_reducible]

instance QuantumParallelRepetition.instFintypeFullSubsetHistory {X✝ : Type u_1} {Y✝ : Type u_2} {n✝ : ℕ} {D✝ L✝ : Finset (Fin n✝)} [Fintype X✝] [Fintype Y✝] : Fintype (FullSubsetHistory X✝ Y✝ n✝ D✝ L✝)

Equations

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

def QuantumParallelRepetition.fullHistoryAliceQuestion {X : Type u_1} {Y : Type u_2} {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥(fullHistoryRemaining n D L) → X) : Fin n → X

The full history alice question construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.fullHistoryAliceQuestion h hidden i = if hiD : i ∈ D then h.aliceConditioned ⟨i, hiD⟩ else if hiL : i ∈ L then h.aliceRevealed ⟨i, hiL⟩ else hidden ⟨i, ⋯⟩

def QuantumParallelRepetition.fullHistoryBobQuestion {X : Type u_1} {Y : Type u_2} {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥L → Y) : Fin n → Y

The full history bob question construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.fullHistoryBobQuestion h hidden i = if hiD : i ∈ D then h.bobConditioned ⟨i, hiD⟩ else if hiL : i ∈ L then hidden ⟨i, hiL⟩ else h.bobRemaining ⟨i, ⋯⟩

def QuantumParallelRepetition.fullHistoryWeight {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) : ℝ

The probability weight for full history.

Equations

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

noncomputable def QuantumParallelRepetition.fullHistoryHiddenAliceWeight {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥(fullHistoryRemaining n D L) → X) : ℝ

The probability weight for full history hidden alice.

Equations

• QuantumParallelRepetition.fullHistoryHiddenAliceWeight G h hidden = ∏ i : ↥(QuantumParallelRepetition.fullHistoryRemaining n D L), G.conditionalXGivenY (h.bobRemaining i) (hidden i)

noncomputable def QuantumParallelRepetition.fullHistoryHiddenBobWeight {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥L → Y) : ℝ

The probability weight for full history hidden bob.

Equations

• QuantumParallelRepetition.fullHistoryHiddenBobWeight G h hidden = ∏ i : ↥L, G.conditionalYGivenX (h.aliceRevealed i) (hidden i)

theorem QuantumParallelRepetition.fullHistoryWeight_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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) : 0 ≤ fullHistoryWeight G h

theorem QuantumParallelRepetition.fullHistoryHiddenAliceWeight_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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥(fullHistoryRemaining n D L) → X) : 0 ≤ fullHistoryHiddenAliceWeight G h hidden

theorem QuantumParallelRepetition.fullHistoryHiddenBobWeight_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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥L → Y) : 0 ≤ fullHistoryHiddenBobWeight G h hidden

theorem QuantumParallelRepetition.fullHistoryWeight_mul_hidden {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 L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (h : FullSubsetHistory X Y n D L) (hx : ↥(fullHistoryRemaining n D L) → X) (hy : ↥L → Y) : fullHistoryWeight G h * fullHistoryHiddenAliceWeight G h hx * fullHistoryHiddenBobWeight G h hy = (G.repeat n).questionWeight (fullHistoryAliceQuestion h hx) (fullHistoryBobQuestion h hy)

noncomputable def QuantumParallelRepetition.fullHistoryAliceFilter {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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (α : ↥D → A) : Matrix S.Alice S.Alice ℂ

The spectral filter for full history alice.

Equations

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

noncomputable def QuantumParallelRepetition.fullHistoryBobFilter {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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (β : ↥D → B) : Matrix S.Bob S.Bob ℂ

The spectral filter for full history bob.

Equations

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

theorem QuantumParallelRepetition.fullHistoryAliceFilter_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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (α : ↥D → A) : (fullHistoryAliceFilter G n S D L h α).PosSemidef

theorem QuantumParallelRepetition.fullHistoryBobFilter_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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (β : ↥D → B) : (fullHistoryBobFilter G n S D L h β).PosSemidef

def QuantumParallelRepetition.fullHistoryWinIndicator {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) : ℝ

The indicator function for full history win.

Equations

• QuantumParallelRepetition.fullHistoryWinIndicator G h α β = if ∀ (i : ↥D), G.predicate (h.aliceConditioned i) (h.bobConditioned i) (α i) (β i) = true then 1 else 0

theorem QuantumParallelRepetition.fullHistoryWinIndicator_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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) : 0 ≤ fullHistoryWinIndicator G h α β

theorem QuantumParallelRepetition.conditionedAnswerMatches_iff {T : Type u_5} {n : ℕ} (D : Finset (Fin n)) (answer : Fin n → T) (α : ↥D → T) : (∀ (i : Fin n) (hi : i ∈ D), answer i = α ⟨i, hi⟩) ↔ α = fun (i : ↥D) => answer ↑i

theorem QuantumParallelRepetition.conditionedEffects_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) : ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D α xs)) (conditionedBobEffect G n S D β ys) = ∑ aa : Fin n → A, ∑ bb : Fin n → B, if ∀ (i : Fin n) (hi : i ∈ D), aa i = α ⟨i, hi⟩ then if ∀ (i : Fin n) (hi : i ∈ D), bb i = β ⟨i, hi⟩ then S.outcomeProbability xs ys aa bb else 0 else 0

theorem QuantumParallelRepetition.finite_sum_four_swap {I : Type u_5} {J : Type u_6} {K : Type u_7} {T : Type u_8} [Fintype I] [Fintype J] [Fintype K] [Fintype T] (f : I → J → K → T → ℝ) : ∑ i : I, ∑ j : J, ∑ k : K, ∑ t : T, f i j k t = ∑ k : K, ∑ t : T, ∑ i : I, ∑ j : J, f i j k t

theorem QuantumParallelRepetition.repeated_partialWinMass_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] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, ∑ aa : Fin n → A, ∑ bb : Fin n → B, (G.repeat n).questionWeight xs ys * if ∀ (i : ↥D), G.predicate (xs ↑i) (ys ↑i) (aa ↑i) (bb ↑i) = true then S.outcomeProbability xs ys aa bb else 0

theorem QuantumParallelRepetition.fullHistoryFilters_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] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) : ((bornTracePairing S.state.matrix) (fullHistoryAliceFilter G n S D L h α)) (fullHistoryBobFilter G n S D L h β) = ∑ hx : ↥(fullHistoryRemaining n D L) → X, ∑ hy : ↥L → Y, fullHistoryHiddenAliceWeight G h hx * fullHistoryHiddenBobWeight G h hy * ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D α (fullHistoryAliceQuestion h hx))) (conditionedBobEffect G n S D β (fullHistoryBobQuestion h hy))

theorem QuantumParallelRepetition.fullSubsetHistory_mass_eq_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 L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) : ∑ h : FullSubsetHistory X Y n D L, ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * ((bornTracePairing S.state.matrix) (fullHistoryAliceFilter G n S D L h α)) (fullHistoryBobFilter G n S D L h β) = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)

theorem QuantumParallelRepetition.spectralPurificationFilter_mul_shift {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : spectralPurificationFilter F hF s * (F + s • 1) = F

theorem QuantumParallelRepetition.spectralPurificationFilter_eq_resolvent {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : spectralPurificationFilter F hF s = F * (F + s • 1)⁻¹

theorem QuantumParallelRepetition.spectralPurificationFilter_square_contraction {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : (spectralPurificationFilter F hF s - star (spectralPurificationFilter F hF s) * spectralPurificationFilter F hF s).PosSemidef

theorem QuantumParallelRepetition.bochner_integral_posSemidef {α : Type u_1} {d : Type u_2} [MeasurableSpace α] [Fintype d] {μ : MeasureTheory.Measure α} {f : α → Matrix d d ℂ} (hf : MeasureTheory.Integrable f μ) (hpos : ∀ᵐ (t : α) ∂μ, (f t).PosSemidef) : (∫ (t : α), f t ∂μ).PosSemidef

theorem QuantumParallelRepetition.spectralPurificationFilter_eq_one_sub_shifted_inverse {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : spectralPurificationFilter F hF s = 1 - s • (F + s • 1)⁻¹

theorem QuantumParallelRepetition.shifted_inverse_square_contraction {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) {s : ℝ} (hs : 0 < s) : (s • (F + s • 1)⁻¹ - s ^ 2 • ((F + s • 1)⁻¹ * (F + s • 1)⁻¹)).PosSemidef

theorem QuantumParallelRepetition.spectralPurificationFilter_sub_resolvent {d : Type u_1} [Fintype d] [DecidableEq d] (F M : Matrix d d ℂ) (hF : F.PosSemidef) (hM : M.PosSemidef) {s : ℝ} (hs : 0 < s) : spectralPurificationFilter F hF s - spectralPurificationFilter M hM s = s • ((F + s • 1)⁻¹ * (F - M) * (M + s • 1)⁻¹)

theorem QuantumParallelRepetition.spectralPurificationFilter_sub_gram {d : Type u_1} [Fintype d] [DecidableEq d] (F M : Matrix d d ℂ) (hF : F.PosSemidef) (hM : M.PosSemidef) {s : ℝ} (hs : 0 < s) : star (spectralPurificationFilter F hF s - spectralPurificationFilter M hM s) * (spectralPurificationFilter F hF s - spectralPurificationFilter M hM s) = s ^ 2 • ((M + s • 1)⁻¹ * (F - M) * ((F + s • 1)⁻¹ * (F + s • 1)⁻¹) * (F - M) * (M + s • 1)⁻¹)

theorem QuantumParallelRepetition.weighted_shifted_inverse_second_order {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) {s : ℝ} (hs : 0 < s) : ∑ i : ι, weight i • (F i + s • 1)⁻¹ - (M + s • 1)⁻¹ = ((M + s • 1)⁻¹ * ∑ i : ι, weight i • ((F i - M) * (F i + s • 1)⁻¹ * (F i - M))) * (M + s • 1)⁻¹

theorem QuantumParallelRepetition.weighted_spectralPurificationFilter_variance_le_inverse_jensen {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) (positive : ∀ (i : ι), (F i).PosSemidef) {s : ℝ} (hs : 0 < s) : have hM := ⋯; (s • (∑ i : ι, weight i • (F i + s • 1)⁻¹ - (M + s • 1)⁻¹) - ∑ i : ι, weight i • (star (spectralPurificationFilter (F i) ⋯ s - spectralPurificationFilter M hM s) * (spectralPurificationFilter (F i) ⋯ s - spectralPurificationFilter M hM s))).PosSemidef

theorem QuantumParallelRepetition.scalarResolventFilter_memLp_two {z : ℝ} (hz : 0 ≤ z) : MeasureTheory.MemLp (fun (s : ℝ) => z / (z + s)) 2 (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem QuantumParallelRepetition.spectralPurificationFilter_memLp_two {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : MeasureTheory.MemLp (spectralPurificationFilter F hF) 2 (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem QuantumParallelRepetition.matrix_memLp_two_mul_integrable {α : Type u_1} {d : Type u_2} [MeasurableSpace α] [Fintype d] {μ : MeasureTheory.Measure α} {f g : α → Matrix d d ℂ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : MeasureTheory.Integrable (fun (t : α) => f t * g t) μ

theorem QuantumParallelRepetition.spectralPurificationFilter_difference_gram_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (F M : Matrix d d ℂ) (hF : F.PosSemidef) (hM : M.PosSemidef) : MeasureTheory.IntegrableOn (fun (s : ℝ) => star (spectralPurificationFilter F hF s - spectralPurificationFilter M hM s) * (spectralPurificationFilter F hF s - spectralPurificationFilter M hM s)) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.scalar_entropy_resolvent_integrable {z : ℝ} (hz : 0 ≤ z) : MeasureTheory.IntegrableOn (fun (s : ℝ) => z / (1 + s) - z / (z + s)) (Set.Ioi 0) MeasureTheory.volume

noncomputable def QuantumParallelRepetition.weightedSpectralFilterVariance {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (s : ℝ) : Matrix d d ℂ

The weighted spectral filter variance construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.weightedSpectralFilterVariance_integrable {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) : MeasureTheory.IntegrableOn (weightedSpectralFilterVariance weight F M positive hM) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.scalar_entropy_resolvent_integral {z : ℝ} (hz : 0 ≤ z) : ∫ (s : ℝ) in Set.Ioi 0, z / (1 + s) - z / (z + s) = z * Real.log z

theorem QuantumParallelRepetition.exact_matrix_log_entropy_filter_jensen {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) (positive : ∀ (i : ι), (F i).PosSemidef) : have hM := ⋯; (∑ i : ι, weight i • cfc (fun (z : ℝ) => z * Real.log z) (F i) - cfc (fun (z : ℝ) => z * Real.log z) M - ∫ (s : ℝ) in Set.Ioi 0, weightedSpectralFilterVariance weight F M positive hM s).PosSemidef

theorem QuantumParallelRepetition.Game.conditionalYGivenX_sum_le_one {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) (x : X) : ∑ y : Y, G.conditionalYGivenX x y ≤ 1

theorem QuantumParallelRepetition.Game.conditionalXGivenY_sum_le_one {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) (y : Y) : ∑ x : X, G.conditionalXGivenY y x ≤ 1

theorem QuantumParallelRepetition.fullHistoryHiddenAliceWeight_sum_le_one {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) : ∑ hidden : ↥(fullHistoryRemaining n D L) → X, fullHistoryHiddenAliceWeight G h hidden ≤ 1

theorem QuantumParallelRepetition.fullHistoryHiddenBobWeight_sum_le_one {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 L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) : ∑ hidden : ↥L → Y, fullHistoryHiddenBobWeight G h hidden ≤ 1

theorem QuantumParallelRepetition.fullHistoryAliceFilter_complement_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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (α : ↥D → A) : (1 - fullHistoryAliceFilter G n S D L h α).PosSemidef

theorem QuantumParallelRepetition.fullHistoryBobFilter_complement_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 L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (β : ↥D → B) : (1 - fullHistoryBobFilter G n S D L h β).PosSemidef

theorem QuantumParallelRepetition.matrixLogEntropy_nonpos_of_contraction {d : Type u_5} [Fintype d] [DecidableEq d] {F : Matrix d d ℂ} (hF : F.PosSemidef) (hcomplement : (1 - F).PosSemidef) : (-cfc (fun (z : ℝ) => z * Real.log z) F).PosSemidef

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

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

noncomputable def QuantumParallelRepetition.fullHistoryAliceEntropyPotential {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 L : Finset (Fin n)) : ℝ

The potential function controlling full history alice entropy.

Equations

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

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_nonpos {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 L : Finset (Fin n)) : fullHistoryAliceEntropyPotential G n S D L ≤ 0

noncomputable def QuantumParallelRepetition.positiveMatrixSpectralAtom {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i : d) : Matrix d d ℂ

The finite atom representing positive matrix spectral.

Equations

• QuantumParallelRepetition.positiveMatrixSpectralAtom F hF i = (QuantumParallelRepetition.spectralConjugationCLM ⋯.eigenvectorUnitary) (Matrix.diagonal (Pi.single i 1))

theorem QuantumParallelRepetition.positiveMatrixSpectralAtom_posSemidef {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i : d) : (positiveMatrixSpectralAtom F hF i).PosSemidef

theorem QuantumParallelRepetition.positiveMatrixSpectralAtom_sum {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : ∑ i : d, positiveMatrixSpectralAtom F hF i = 1

theorem QuantumParallelRepetition.positiveMatrix_cfc_spectral_sum {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (f : ℝ → ℝ) : cfc f F = ∑ i : d, f (⋯.eigenvalues i) • positiveMatrixSpectralAtom F hF i

theorem QuantumParallelRepetition.bornTracePairing_one_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) : ((bornTracePairing ρ.matrix) 1) 1 = 1

theorem QuantumParallelRepetition.bornTracePairing_one_le_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (G : Matrix dB dB ℂ) (hGcomplement : (1 - G).PosSemidef) : ((bornTracePairing ρ.matrix) 1) G ≤ 1

theorem QuantumParallelRepetition.positiveContraction_eigenvalue_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (hcomplement : (1 - F).PosSemidef) (i : d) : ⋯.eigenvalues i ≤ 1

theorem QuantumParallelRepetition.matrixLogEntropy_born_lower_bound_left {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

noncomputable def QuantumParallelRepetition.rawEmbezzlementState (n : ℕ) : EuclideanSpace ℂ (Fin n × Fin n)

The quantum state representing raw embezzlement.

Equations

• QuantumParallelRepetition.rawEmbezzlementState n = WithLp.toLp 2 fun (q : Fin n × Fin n) => if q.1 = q.2 then ↑(√(↑↑q.1 + 1))⁻¹ else 0

theorem QuantumParallelRepetition.rawEmbezzlementState_ne_zero (n : ℕ) (hn : 0 < n) : rawEmbezzlementState n ≠ 0

noncomputable def QuantumParallelRepetition.harmonicNumber (n : ℕ) : ℝ

The harmonic number construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.harmonicNumber n = ∑ j : Fin n, (↑↑j + 1)⁻¹

theorem QuantumParallelRepetition.rawEmbezzlementState_norm_sq (n : ℕ) : ‖rawEmbezzlementState n‖ ^ 2 = harmonicNumber n

noncomputable def QuantumParallelRepetition.embezzlementState (n : ℕ) : EuclideanSpace ℂ (Fin n × Fin n)

The quantum state representing embezzlement.

Equations

• QuantumParallelRepetition.embezzlementState n = ‖QuantumParallelRepetition.rawEmbezzlementState n‖⁻¹ • QuantumParallelRepetition.rawEmbezzlementState n

theorem QuantumParallelRepetition.embezzlementState_norm (n : ℕ) (hn : 0 < n) : ‖embezzlementState n‖ = 1

theorem QuantumParallelRepetition.embezzlementState_apply (n : ℕ) (i j : Fin n) : (embezzlementState n).ofLp (i, j) = ‖rawEmbezzlementState n‖⁻¹ • if i = j then ↑(√(↑↑i + 1))⁻¹ else 0

@[reducible, inline]

abbrev QuantumParallelRepetition.BipartiteUnitVector (d : ℕ) : Type

The type used to represent bipartite unit vector in the exact sampling construction.

Equations

• QuantumParallelRepetition.BipartiteUnitVector d = { ξ : EuclideanSpace ℂ (Fin d × Fin d) // ‖ξ‖ = 1 }

noncomputable def QuantumParallelRepetition.spectralAtomOverlap {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (i j : d) : ℝ

The overlap quantity for spectral atom.

Equations

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

theorem QuantumParallelRepetition.spectralAtomOverlap_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (i j : d) : 0 ≤ spectralAtomOverlap F G hF hG i j

theorem QuantumParallelRepetition.spectralAtom_trace {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i : d) : (positiveMatrixSpectralAtom F hF i).trace = 1

theorem QuantumParallelRepetition.spectralAtom_mul {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i j : d) : positiveMatrixSpectralAtom F hF i * positiveMatrixSpectralAtom F hF j = if i = j then positiveMatrixSpectralAtom F hF i else 0

theorem QuantumParallelRepetition.spectralAtomSum_mul_self {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : Finset d) : (∑ i ∈ s, positiveMatrixSpectralAtom F hF i) * ∑ i ∈ s, positiveMatrixSpectralAtom F hF i = ∑ i ∈ s, positiveMatrixSpectralAtom F hF i

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

def QuantumParallelRepetition.coherentBinaryJointOutcome {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM Bool d) (Q : POVM Bool e) (z : EuclideanSpace ℂ (d × e)) (a b : Bool) : EuclideanSpace ℂ (d × e)

The finite outcome encoding for coherent binary joint.

Equations

• QuantumParallelRepetition.coherentBinaryJointOutcome P Q z a b = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) (Q.effect b)).mulVec z.ofLp)

theorem QuantumParallelRepetition.coherentBinaryJointOutcome_norm_sq {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM Bool d) (Q : POVM Bool e) (hP : ∀ (c : Bool), P.effect c * P.effect c = P.effect c) (hQ : ∀ (c : Bool), Q.effect c * Q.effect c = Q.effect c) (z : EuclideanSpace ℂ (d × e)) (hz : ‖z‖ = 1) (a b : Bool) : ‖coherentBinaryJointOutcome P Q z a b‖ ^ 2 = ((pureDensityMatrix z hz).matrix * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) (Q.effect b)).trace.re

def QuantumParallelRepetition.finiteTensorVector {ι : Type u_1} {d : Type u_2} [Fintype ι] (v : ι → EuclideanSpace ℂ d) : EuclideanSpace ℂ (ι → d)

The state vector representing finite tensor.

Equations

• QuantumParallelRepetition.finiteTensorVector v = WithLp.toLp 2 fun (q : ι → d) => ∏ i : ι, (v i).ofLp (q i)

theorem QuantumParallelRepetition.finiteTensorVector_norm_sq {ι : Type u_1} {d : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype d] (v : ι → EuclideanSpace ℂ d) : ‖finiteTensorVector v‖ ^ 2 = ∏ i : ι, ‖v i‖ ^ 2

theorem QuantumParallelRepetition.finiteTensorVector_norm {ι : Type u_1} {d : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype d] (v : ι → EuclideanSpace ℂ d) (hv : ∀ (i : ι), ‖v i‖ = 1) : ‖finiteTensorVector v‖ = 1

theorem QuantumParallelRepetition.spectralAtomOverlap_sum_right {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (i : d) : ∑ j : d, spectralAtomOverlap F G hF hG i j = 1

theorem QuantumParallelRepetition.spectralAtomOverlap_sum_left {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (j : d) : ∑ i : d, spectralAtomOverlap F G hF hG i j = 1

theorem QuantumParallelRepetition.positiveDensity_eigenvalues_sum {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (htrace : F.trace = 1) : ∑ i : d, ⋯.eigenvalues i = 1

theorem QuantumParallelRepetition.spectralAtomOverlap_schmidtMass_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (hFtrace : F.trace = 1) (hGtrace : G.trace = 1) : ∑ i : d, ∑ j : d, √(⋯.eigenvalues i) * √(⋯.eigenvalues j) * spectralAtomOverlap F G hF hG i j ≤ 1

def QuantumParallelRepetition.binaryBornProbability {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) (a b : Bool) : ℝ

The probability of binary born.

Equations

• QuantumParallelRepetition.binaryBornProbability ρ P Q a b = (ρ.matrix * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) (Q.effect b)).trace.re

theorem QuantumParallelRepetition.binaryBornProbability_normalized {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) : ∑ a : Bool, ∑ b : Bool, binaryBornProbability ρ P Q a b = 1

def QuantumParallelRepetition.binaryContinueProbability {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) : ℝ

The probability of binary continue.

Equations

• QuantumParallelRepetition.binaryContinueProbability ρ P Q = QuantumParallelRepetition.binaryBornProbability ρ P Q false false

def QuantumParallelRepetition.binaryJointSuccessProbability {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) : ℝ

The probability of binary joint success.

Equations

• QuantumParallelRepetition.binaryJointSuccessProbability ρ P Q = QuantumParallelRepetition.binaryBornProbability ρ P Q true true

def QuantumParallelRepetition.binaryMismatchProbability {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) : ℝ

The probability of binary mismatch.

Equations

• QuantumParallelRepetition.binaryMismatchProbability ρ P Q = QuantumParallelRepetition.binaryBornProbability ρ P Q true false + QuantumParallelRepetition.binaryBornProbability ρ P Q false true

theorem QuantumParallelRepetition.binaryStoppingPartition {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (ρ : DensityMatrix (d × e)) (P : POVM Bool d) (Q : POVM Bool e) : binaryContinueProbability ρ P Q + binaryJointSuccessProbability ρ P Q + binaryMismatchProbability ρ P Q = 1

theorem QuantumParallelRepetition.unitVector_distance_of_real_overlap {ι : Type u_1} [Fintype ι] (z w : EuclideanSpace ℂ ι) (hz : ‖z‖ = 1) (hw : ‖w‖ = 1) (ε : ℝ) (hε : 0 ≤ ε) (hoverlap : 1 - ε ≤ (inner ℂ z w).re) : ‖z - w‖ ≤ √(2 * ε)

def QuantumParallelRepetition.sharedThresholdResourceRaw {κ : Type u_1} {d : Type u_2} [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : EuclideanSpace ℂ (((_ : κ) × d) × (_ : κ) × d)

The shared threshold resource raw construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.sharedThresholdResourceRaw τ = WithLp.toLp 2 fun (q : ((_ : κ) × d) × (_ : κ) × d) => if q.1.fst = q.2.fst ∧ q.1.snd = q.2.snd then ↑(τ q.1.fst) else 0

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_norm_sq {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : ‖sharedThresholdResourceRaw τ‖ ^ 2 = ↑(Fintype.card d) * ∑ k : κ, τ k ^ 2

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_ne_zero {κ : Type u_1} {d : Type u_2} [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (k : κ) (i : d) (hk : τ k ≠ 0) : sharedThresholdResourceRaw τ ≠ 0

noncomputable def QuantumParallelRepetition.sharedThresholdResource {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : EuclideanSpace ℂ (((_ : κ) × d) × (_ : κ) × d)

The auxiliary resource for shared threshold.

Equations

• QuantumParallelRepetition.sharedThresholdResource τ = ‖QuantumParallelRepetition.sharedThresholdResourceRaw τ‖⁻¹ • QuantumParallelRepetition.sharedThresholdResourceRaw τ

theorem QuantumParallelRepetition.sharedThresholdResource_norm {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (k : κ) (i : d) (hk : τ k ≠ 0) : ‖sharedThresholdResource τ‖ = 1

def QuantumParallelRepetition.transposePOVM {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (P : POVM ι d) : POVM ι d

The positive operator-valued measurement implementing transpose.

Equations

• QuantumParallelRepetition.transposePOVM P = { effect := fun (b : ι) => (P.effect b).transpose, positive := ⋯, complete := ⋯ }

theorem QuantumParallelRepetition.transposePOVM_projective {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (P : POVM ι d) (hP : ∀ (b : ι), P.effect b * P.effect b = P.effect b) (b : ι) : (transposePOVM P).effect b * (transposePOVM P).effect b = (transposePOVM P).effect b

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_eq_vec {κ : Type u_1} {d : Type u_2} [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : sharedThresholdResourceRaw τ = WithLp.toLp 2 (Matrix.diagonal fun (q : (_ : κ) × d) => ↑(τ q.fst)).vec

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_local_action {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (A B : Matrix ((_ : κ) × d) ((_ : κ) × d) ℂ) : WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B.transpose).mulVec (sharedThresholdResourceRaw τ).ofLp) = WithLp.toLp 2 ((B.transpose * Matrix.diagonal fun (q : (_ : κ) × d) => ↑(τ q.fst)) * A.transpose).vec

theorem QuantumParallelRepetition.matrixVectorization_norm_sq {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] (K : Matrix d e ℂ) : ‖WithLp.toLp 2 K.vec‖ ^ 2 = (K.conjTranspose * K).trace.re

theorem QuantumParallelRepetition.sharedThresholdDiagonal_eq_block {κ : Type u_1} {d : Type u_2} [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : (Matrix.diagonal fun (q : (_ : κ) × d) => ↑(τ q.fst)) = Matrix.blockDiagonal' fun (k : κ) => ↑(τ k) • 1

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_block_action {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (A B : κ → Matrix d d ℂ) : WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.blockDiagonal' A) (Matrix.blockDiagonal' B).transpose).mulVec (sharedThresholdResourceRaw τ).ofLp) = WithLp.toLp 2 (Matrix.blockDiagonal' fun (k : κ) => ↑(τ k) • (A k * B k)).transpose.vec

theorem QuantumParallelRepetition.projectorProduct_hilbertSchmidt_trace {d : Type u_1} [Fintype d] (A B : Matrix d d ℂ) (hA : A.PosSemidef) (hB : B.PosSemidef) (hAA : A * A = A) (hBB : B * B = B) : ((A * B).conjTranspose * (A * B)).trace = (A * B).trace

theorem QuantumParallelRepetition.weightedProjectorProduct_hilbertSchmidt_trace {d : Type u_1} [Fintype d] (t : ℝ) (A B : Matrix d d ℂ) (hA : A.PosSemidef) (hB : B.PosSemidef) (hAA : A * A = A) (hBB : B * B = B) : ((↑t • (A * B)).conjTranspose * ↑t • (A * B)).trace.re = t ^ 2 * (A * B).trace.re

theorem QuantumParallelRepetition.sharedThresholdResourceRaw_block_action_norm_sq {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (A B : κ → Matrix d d ℂ) (hA : ∀ (k : κ), (A k).PosSemidef) (hB : ∀ (k : κ), (B k).PosSemidef) (hAA : ∀ (k : κ), A k * A k = A k) (hBB : ∀ (k : κ), B k * B k = B k) : ‖WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.blockDiagonal' A) (Matrix.blockDiagonal' B).transpose).mulVec (sharedThresholdResourceRaw τ).ofLp)‖ ^ 2 = ∑ k : κ, τ k ^ 2 * (A k * B k).trace.re

theorem QuantumParallelRepetition.sharedThresholdResource_block_action_norm_sq {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (A B : κ → Matrix d d ℂ) (hA : ∀ (k : κ), (A k).PosSemidef) (hB : ∀ (k : κ), (B k).PosSemidef) (hAA : ∀ (k : κ), A k * A k = A k) (hBB : ∀ (k : κ), B k * B k = B k) : ‖WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.blockDiagonal' A) (Matrix.blockDiagonal' B).transpose).mulVec (sharedThresholdResource τ).ofLp)‖ ^ 2 = (∑ k : κ, τ k ^ 2 * (A k * B k).trace.re) / (↑(Fintype.card d) * ∑ k : κ, τ k ^ 2)

theorem QuantumParallelRepetition.doublyStochasticSchmidtMass_le_one {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (σ : ι → ℝ) (μ : κ → ℝ) (w : ι → κ → ℝ) (hσunit : ∑ i : ι, σ i ^ 2 = 1) (hμunit : ∑ j : κ, μ j ^ 2 = 1) (hw : ∀ (i : ι) (j : κ), 0 ≤ w i j) (hrow : ∀ (i : ι), ∑ j : κ, w i j = 1) (hcol : ∀ (j : κ), ∑ i : ι, w i j = 1) : ∑ i : ι, ∑ j : κ, σ i * μ j * w i j ≤ 1

theorem QuantumParallelRepetition.doublyStochasticSchmidtEnergy_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (σ : ι → ℝ) (μ : κ → ℝ) (w : ι → κ → ℝ) (hσunit : ∑ i : ι, σ i ^ 2 = 1) (hμunit : ∑ j : κ, μ j ^ 2 = 1) (hrow : ∀ (i : ι), ∑ j : κ, w i j = 1) (hcol : ∀ (j : κ), ∑ i : ι, w i j = 1) : ∑ i : ι, ∑ j : κ, (σ i - μ j) ^ 2 * w i j = 2 - 2 * ∑ i : ι, ∑ j : κ, σ i * μ j * w i j

theorem QuantumParallelRepetition.complexInner_norm_sq_le {ι : Type u_1} [Fintype ι] (z w : EuclideanSpace ℂ ι) : ‖inner ℂ z w‖ ^ 2 ≤ ‖z‖ ^ 2 * ‖w‖ ^ 2

noncomputable def QuantumParallelRepetition.tensorEmbezzlementTarget {d n : ℕ} (ξ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin (d * n) × Fin (d * n))

The target object for tensor embezzlement.

Equations

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

theorem QuantumParallelRepetition.tensorEmbezzlementTarget_norm {d n : ℕ} (hn : 0 < n) (ξ : BipartiteUnitVector d) : ‖tensorEmbezzlementTarget ξ‖ = 1

def QuantumParallelRepetition.localUnitaryAction {n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (ψ : EuclideanSpace ℂ (Fin n × Fin n)) : EuclideanSpace ℂ (Fin n × Fin n)

The operator action for local unitary.

Equations

• QuantumParallelRepetition.localUnitaryAction U V ψ = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).mulVec ψ.ofLp)

theorem QuantumParallelRepetition.localUnitaryAction_matrix_mem_unitary {n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin n) ℂ)) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V ∈ Matrix.unitaryGroup (Fin n × Fin n) ℂ

theorem QuantumParallelRepetition.localUnitaryAction_norm {n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (ψ : EuclideanSpace ℂ (Fin n × Fin n)) : ‖localUnitaryAction U V ψ‖ = ‖ψ‖

theorem QuantumParallelRepetition.unitary_row_norm_sq_sum {d : Type u_1} [Fintype d] [DecidableEq d] (U : ↥(Matrix.unitaryGroup d ℂ)) (i : d) : ∑ j : d, ‖↑U i j‖ ^ 2 = 1

theorem QuantumParallelRepetition.unitary_col_norm_sq_sum {d : Type u_1} [Fintype d] [DecidableEq d] (U : ↥(Matrix.unitaryGroup d ℂ)) (j : d) : ∑ i : d, ‖↑U i j‖ ^ 2 = 1

def QuantumParallelRepetition.unitaryBasisOverlap {d : Type u_1} [Fintype d] [DecidableEq d] (U V : ↥(Matrix.unitaryGroup d ℂ)) : ↥(Matrix.unitaryGroup d ℂ)

The overlap quantity for unitary basis.

Equations

• QuantumParallelRepetition.unitaryBasisOverlap U V = U⁻¹ * V

def QuantumParallelRepetition.diagonalSchmidtState {d : Type u_1} [DecidableEq d] (σ : d → ℝ) : EuclideanSpace ℂ (d × d)

The quantum state representing diagonal schmidt.

Equations

• QuantumParallelRepetition.diagonalSchmidtState σ = WithLp.toLp 2 fun (q : d × d) => if q.1 = q.2 then ↑(σ q.1) else 0

theorem QuantumParallelRepetition.diagonalSchmidtState_norm_sq {d : Type u_1} [Fintype d] [DecidableEq d] (σ : d → ℝ) : ‖diagonalSchmidtState σ‖ ^ 2 = ∑ i : d, σ i ^ 2

def QuantumParallelRepetition.schmidtVector {d : ℕ} (σ : Fin d → ℝ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : EuclideanSpace ℂ (Fin d × Fin d)

The state vector representing schmidt.

Equations

• QuantumParallelRepetition.schmidtVector σ U V = QuantumParallelRepetition.localUnitaryAction U V (QuantumParallelRepetition.diagonalSchmidtState σ)

theorem QuantumParallelRepetition.schmidtVector_norm_sq {d : ℕ} (σ : Fin d → ℝ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : ‖schmidtVector σ U V‖ ^ 2 = ∑ i : Fin d, σ i ^ 2

theorem QuantumParallelRepetition.schmidtVector_apply {d : ℕ} (σ : Fin d → ℝ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (a b : Fin d) : (schmidtVector σ U V).ofLp (a, b) = ∑ i : Fin d, ↑(σ i) * ↑U a i * ↑V b i

theorem QuantumParallelRepetition.matrixVectorization_inner {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] (X Y : Matrix d e ℂ) : inner ℂ (WithLp.toLp 2 X.vec) (WithLp.toLp 2 Y.vec) = (X.conjTranspose * Y).trace

theorem QuantumParallelRepetition.diagonalSchmidtState_eq_vec {d : Type u_1} [DecidableEq d] (σ : d → ℝ) : diagonalSchmidtState σ = WithLp.toLp 2 (Matrix.diagonal fun (i : d) => ↑(σ i)).vec

theorem QuantumParallelRepetition.schmidtVector_eq_vec {d : ℕ} (σ : Fin d → ℝ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : schmidtVector σ U V = WithLp.toLp 2 ((↑V * Matrix.diagonal fun (i : Fin d) => ↑(σ i)) * (↑U).transpose).vec

theorem QuantumParallelRepetition.weightedSchmidtMatrixTrace {d : Type u_1} [Fintype d] [DecidableEq d] (σ μ : d → ℝ) (L R : Matrix d d ℂ) : ((L.transpose * Matrix.diagonal fun (i : d) => ↑(σ i)) * R * Matrix.diagonal fun (j : d) => ↑(μ j)).trace = ∑ i : d, ∑ j : d, ↑(σ i) * ↑(μ j) * L i j * R i j

theorem QuantumParallelRepetition.schmidtVector_inner {d : ℕ} (σ μ : Fin d → ℝ) (U V X Y : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : inner ℂ (schmidtVector σ U V) (schmidtVector μ X Y) = ∑ i : Fin d, ∑ j : Fin d, ↑(σ i) * ↑(μ j) * ((↑U).conjTranspose * ↑X) i j * ((↑V).conjTranspose * ↑Y) i j

@[simp]

theorem QuantumParallelRepetition.unitaryBasisOverlap_apply {d : Type u_1} [Fintype d] [DecidableEq d] (U V : ↥(Matrix.unitaryGroup d ℂ)) (i j : d) : ↑(unitaryBasisOverlap U V) i j = ((↑U).conjTranspose * ↑V) i j

theorem QuantumParallelRepetition.schmidtVector_spectralEnergy_le {d : ℕ} (σ μ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hμ : ∀ (j : Fin d), 0 ≤ μ j) (hσunit : ∑ i : Fin d, σ i ^ 2 = 1) (hμunit : ∑ j : Fin d, μ j ^ 2 = 1) (U V X Y : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : ∑ i : Fin d, ∑ j : Fin d, (σ i - μ j) ^ 2 * ‖↑(unitaryBasisOverlap U X) i j‖ ^ 2 ≤ 2 * ‖schmidtVector σ U V - schmidtVector μ X Y‖ ^ 2

theorem QuantumParallelRepetition.linearMap_exists_singularBases {d : ℕ} (T : EuclideanSpace ℂ (Fin d) →ₗ[ℂ] EuclideanSpace ℂ (Fin d)) : ∃ (σ : Fin d → ℝ) (u : OrthonormalBasis (Fin d) ℂ (EuclideanSpace ℂ (Fin d))) (v : OrthonormalBasis (Fin d) ℂ (EuclideanSpace ℂ (Fin d))), (∀ (i : Fin d), 0 ≤ σ i) ∧ ∀ (i : Fin d), T (v i) = ↑(σ i) • u i

noncomputable def QuantumParallelRepetition.orthonormalBasisUnitary {d : ℕ} (b : OrthonormalBasis (Fin d) ℂ (EuclideanSpace ℂ (Fin d))) : ↥(Matrix.unitaryGroup (Fin d) ℂ)

The unitary operator implementing orthonormal basis.

Equations

• QuantumParallelRepetition.orthonormalBasisUnitary b = ⟨(EuclideanSpace.basisFun (Fin d) ℂ).toBasis.toMatrix ⇑b.toBasis, ⋯⟩

@[simp]

theorem QuantumParallelRepetition.orthonormalBasisUnitary_apply {d : ℕ} (b : OrthonormalBasis (Fin d) ℂ (EuclideanSpace ℂ (Fin d))) (i j : Fin d) : ↑(orthonormalBasisUnitary b) i j = (b j).ofLp i

def QuantumParallelRepetition.conjugateUnitary {d : ℕ} (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : ↥(Matrix.unitaryGroup (Fin d) ℂ)

The unitary operator implementing conjugate.

Equations

• QuantumParallelRepetition.conjugateUnitary U = ⟨(↑U).conjTranspose.transpose, ⋯⟩

@[simp]

theorem QuantumParallelRepetition.conjugateUnitary_apply {d : ℕ} (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (i j : Fin d) : ↑(conjugateUnitary U) i j = star (↑U i j)

theorem QuantumParallelRepetition.exists_proofSchmidtDecomposition {d : ℕ} (ξ : EuclideanSpace ℂ (Fin d × Fin d)) : ∃ (σ : Fin d → ℝ) (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (V : ↥(Matrix.unitaryGroup (Fin d) ℂ)), (∀ (i : Fin d), 0 ≤ σ i) ∧ ξ = schmidtVector σ U V

theorem QuantumParallelRepetition.exists_proofUnitSchmidtDecomposition {d : ℕ} (ξ : BipartiteUnitVector d) : ∃ (σ : Fin d → ℝ) (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (V : ↥(Matrix.unitaryGroup (Fin d) ℂ)), (∀ (i : Fin d), 0 ≤ σ i) ∧ ∑ i : Fin d, σ i ^ 2 = 1 ∧ ↑ξ = schmidtVector σ U V