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)

• questionWeight : X → Y → ℝ
• 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

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) : ℝ

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) : ℝ

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)

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

• matrix : Matrix d d ℂ
• 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)

• effect : ι → Matrix d d ℂ
• 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)

• Alice : Type
• Bob : Type
• alice_fintype : Fintype self.Alice
• bob_fintype : Fintype self.Bob
• alice_decidableEq : DecidableEq self.Alice
• bob_decidableEq : DecidableEq self.Bob
• state : DensityMatrix (self.Alice × self.Bob)
• aliceMeasurement : X → POVM A self.Alice
• bobMeasurement : Y → POVM B self.Bob

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

def QuantumParallelRepetition.Strategy.jointEffect {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) : Matrix (S.Alice × S.Bob) (S.Alice × S.Bob) ℂ

Equations

• S.jointEffect x y a b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((S.aliceMeasurement x).effect a) ((S.bobMeasurement y).effect b)

theorem QuantumParallelRepetition.Strategy.jointEffect_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} (S : Strategy G) (x : X) (y : Y) (a : A) (b : B) : (S.jointEffect x y a b).PosSemidef

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) : ℝ

Equations

• S.outcomeProbability x y a b = (S.state.matrix * S.jointEffect 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.jointEffect_complete {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.jointEffect x y a b = 1

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) : ℝ

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) : ℝ

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 : ℕ) : ℝ

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) : ℝ

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

theorem QuantumParallelRepetition.matrixEffectCLM_norm_le_one {d : Type u_1} [Fintype d] [DecidableEq d] (E : Matrix d d ℂ) (hE : E.PosSemidef) (h_complement : (1 - E).PosSemidef) : ‖Matrix.toEuclideanCLM E‖ ≤ 1

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) ℂ

Equations

• S.winningEffect x y = ∑ a : A, ∑ b : B, if G.predicate x y a b = true then S.jointEffect 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} [Fintype ι] [DecidableEq ι] {d : ι → Type u_6} [(j : ι) → Fintype (d j)] (M : (j : ι) → Matrix (d j) (d j) ℂ) (hM : ∀ (j : ι), (M j).PosSemidef) : (Matrix.blockDiagonal' M).PosSemidef

@[reducible, inline]

abbrev QuantumParallelRepetition.mixtureAlice {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : J → Strategy G) : Type

Equations

• QuantumParallelRepetition.mixtureAlice S = ((j : J) × (S j).Alice)

@[reducible, inline]

abbrev QuantumParallelRepetition.mixtureBob {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : J → Strategy G) : Type

Equations

• QuantumParallelRepetition.mixtureBob S = ((j : J) × (S j).Bob)

@[reducible, inline]

abbrev QuantumParallelRepetition.mixtureMatched {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : J → Strategy G) : Type

Equations

• QuantumParallelRepetition.mixtureMatched S = ((j : J) × (S j).Alice × (S j).Bob)

def QuantumParallelRepetition.mixtureMatchedIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : J → Strategy G) : mixtureMatched S → mixtureAlice S × mixtureBob S

Equations

• QuantumParallelRepetition.mixtureMatchedIndex S ⟨j, (a, b)⟩ = (⟨j, a⟩, ⟨j, b⟩)

theorem QuantumParallelRepetition.mixtureMatchedIndex_injective {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : J → Strategy G) : Function.Injective (mixtureMatchedIndex S)

def QuantumParallelRepetition.mixtureEmbedding {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) : Matrix (mixtureAlice S × mixtureBob S) (mixtureMatched S) ℂ

Equations

• QuantumParallelRepetition.mixtureEmbedding S q r = if q = QuantumParallelRepetition.mixtureMatchedIndex S r then 1 else 0

theorem QuantumParallelRepetition.mixtureEmbedding_isometry {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) : (mixtureEmbedding S).conjTranspose * mixtureEmbedding S = 1

theorem QuantumParallelRepetition.mixtureEmbedding_compress {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) (E : Matrix (mixtureAlice S × mixtureBob S) (mixtureAlice S × mixtureBob S) ℂ) : (mixtureEmbedding S).conjTranspose * E * mixtureEmbedding S = E.submatrix (mixtureMatchedIndex S) (mixtureMatchedIndex S)

noncomputable def QuantumParallelRepetition.mixtureBlockMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq J] {G : Game X Y A B} (p : J → ℝ) (S : J → Strategy G) : Matrix (mixtureMatched S) (mixtureMatched S) ℂ

Equations

• QuantumParallelRepetition.mixtureBlockMatrix p S = Matrix.blockDiagonal' fun (j : J) => p j • (S j).state.matrix

theorem QuantumParallelRepetition.mixtureBlockMatrix_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (p : J → ℝ) (hp : ∀ (j : J), 0 ≤ p j) (S : J → Strategy G) : (mixtureBlockMatrix p S).PosSemidef

theorem QuantumParallelRepetition.mixtureBlockMatrix_trace {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (p : J → ℝ) (S : J → Strategy G) : (mixtureBlockMatrix p S).trace = ↑(∑ j : J, p j)

noncomputable def QuantumParallelRepetition.mixtureDensityMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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) (S : J → Strategy G) : DensityMatrix (mixtureAlice S × mixtureBob S)

Equations

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

def QuantumParallelRepetition.mixtureAlicePOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) (x : X) : POVM A (mixtureAlice S)

Equations

• QuantumParallelRepetition.mixtureAlicePOVM S x = { effect := fun (a : A) => Matrix.blockDiagonal' fun (j : J) => ((S j).aliceMeasurement x).effect a, positive := ⋯, complete := ⋯ }

def QuantumParallelRepetition.mixtureBobPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) (y : Y) : POVM B (mixtureBob S)

Equations

• QuantumParallelRepetition.mixtureBobPOVM S y = { effect := fun (b : B) => Matrix.blockDiagonal' fun (j : J) => ((S j).bobMeasurement y).effect b, positive := ⋯, complete := ⋯ }

noncomputable def QuantumParallelRepetition.convexMixtureStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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) (S : J → Strategy G) : Strategy G

Equations

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

theorem QuantumParallelRepetition.mixtureJointEffect_compress {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) (x : X) (y : Y) (a : A) (b : B) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((mixtureAlicePOVM S x).effect a) ((mixtureBobPOVM S y).effect b)).submatrix (mixtureMatchedIndex S) (mixtureMatchedIndex S) = Matrix.blockDiagonal' fun (j : J) => (S j).jointEffect x y a b

theorem QuantumParallelRepetition.mixtureEmbedding_trace_mul {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (S : J → Strategy G) (R : Matrix (mixtureMatched S) (mixtureMatched S) ℂ) (E : Matrix (mixtureAlice S × mixtureBob S) (mixtureAlice S × mixtureBob S) ℂ) : (mixtureEmbedding S * R * (mixtureEmbedding S).conjTranspose * E).trace = (R * E.submatrix (mixtureMatchedIndex S) (mixtureMatchedIndex S)).trace

theorem QuantumParallelRepetition.mixtureBlockMatrix_trace_mul {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] [DecidableEq J] {G : Game X Y A B} (p : J → ℝ) (S : J → Strategy G) (E : (j : J) → Matrix ((S j).Alice × (S j).Bob) ((S j).Alice × (S j).Bob) ℂ) : (mixtureBlockMatrix p S * Matrix.blockDiagonal' E).trace = ∑ j : J, p j • ((S j).state.matrix * E j).trace

theorem QuantumParallelRepetition.convexMixtureStrategy_outcomeProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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) (S : J → Strategy G) (x : X) (y : Y) (a : A) (b : B) : (convexMixtureStrategy p hp h_normalized S).outcomeProbability x y a b = ∑ j : J, p j * (S j).outcomeProbability x y a b

theorem QuantumParallelRepetition.convexMixtureStrategy_winProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [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) (S : J → Strategy G) : (convexMixtureStrategy p hp h_normalized S).winProbability = ∑ j : J, p j * (S j).winProbability

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

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

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

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

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

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

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 Ω] [Fintype ι] (wins : ι → Ω → Bool) (D : Finset ι) : Finset Ω

Equations

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

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

theorem QuantumParallelRepetition.FiniteEventLaw.winEvent_antitone {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [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 Ω] [Fintype ι] [DecidableEq ι] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (D : Finset ι) (i : ι) : ℝ

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θ : 0 < θ) (_hη : 0 < η) (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θ : 0 < θ) (hη : 0 < η) (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)

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)

Equations

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

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

Equations

• QuantumParallelRepetition.strategyWinEvent G = {ω : QuantumParallelRepetition.StrategyOutcome X Y A B | G.predicate ω.1 ω.2.1 ω.2.2.1 ω.2.2.2 = true}

theorem QuantumParallelRepetition.strategyEventLaw_winEvent {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) : (strategyEventLaw G S).eventMass (strategyWinEvent G) = S.winProbability

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

Equations

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

theorem QuantumParallelRepetition.repeated_allWinEvent_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 : ℕ) : FiniteEventLaw.winEvent (repeatedCoordinateWin G n) Finset.univ = strategyWinEvent (G.repeat n)

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θ : 0 < θ) (hη : 0 < η) (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] [DecidableEq 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} [Fintype d] [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 ι] [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) : ∑ i : ι, weight i • (F i - M) = 0

theorem QuantumParallelRepetition.weighted_positive_matrix_mean {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (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.diagonalPurificationGram {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (s : ℝ) : Matrix d d ℂ

Equations

• QuantumParallelRepetition.diagonalPurificationGram eigenvalue s = Matrix.diagonal fun (i : d) => ↑((eigenvalue i / (eigenvalue i + s)) ^ 2)

theorem QuantumParallelRepetition.diagonalPurificationGram_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (h_nonneg : ∀ (i : d), 0 ≤ eigenvalue i) : MeasureTheory.IntegrableOn (diagonalPurificationGram eigenvalue) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.integral_diagonalPurificationGram {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (h_nonneg : ∀ (i : d), 0 ≤ eigenvalue i) : ∫ (s : ℝ) in Set.Ioi 0, diagonalPurificationGram eigenvalue s = Matrix.diagonal fun (i : d) => ↑(eigenvalue i)

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

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.spectralPurificationGram {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : ℝ) : Matrix d d ℂ

Equations

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

theorem QuantumParallelRepetition.spectralPurificationGram_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : MeasureTheory.IntegrableOn (spectralPurificationGram F hF) (Set.Ioi 0) MeasureTheory.volume

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

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

Equations

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

theorem QuantumParallelRepetition.spectralPurificationFilter_gram {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : ℝ) : star (spectralPurificationFilter F hF s) * spectralPurificationFilter F hF s = spectralPurificationGram F hF s

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 ℂ →ₗ[ℝ] ℝ

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) : ℝ

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) : ℝ

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

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

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 ℂ

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 ℂ

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 ℂ

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.spectralSupportInverse {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : Matrix d d ℂ

Equations

• QuantumParallelRepetition.spectralSupportInverse F hF = QuantumParallelRepetition.spectralSupportFunctional F hF fun (x : ℝ) => x⁻¹

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

Equations

• QuantumParallelRepetition.spectralSupportProjection F hF = QuantumParallelRepetition.spectralSupportFunctional F hF fun (x : ℝ) => if x = 0 then 0 else 1

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

Equations

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

theorem QuantumParallelRepetition.spectralSupportInverse_isHermitian {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : (spectralSupportInverse F hF).IsHermitian

theorem QuantumParallelRepetition.spectralSupportProjection_isHermitian {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : (spectralSupportProjection F hF).IsHermitian

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

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

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

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

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.mul_spectralSupportProjection {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : F * spectralSupportProjection F hF = F

theorem QuantumParallelRepetition.posSemidef_kernel_of_sub_posSemidef {d : Type u_1} [Fintype d] [DecidableEq 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.posSemidef_mul_spectralSupportProjection {d : Type u_1} [Fintype d] [DecidableEq d] {F A : Matrix d d ℂ} (hF : F.PosSemidef) (hA : A.PosSemidef) (hsub : (F - A).PosSemidef) : A * spectralSupportProjection F hF = A

theorem QuantumParallelRepetition.spectralSupportProjection_mul_posSemidef {d : Type u_1} [Fintype d] [DecidableEq d] {F A : Matrix d d ℂ} (hF : F.PosSemidef) (hA : A.PosSemidef) (hsub : (F - A).PosSemidef) : spectralSupportProjection F hF * A = A

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

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

Equations

• QuantumParallelRepetition.purificationRangeProjection F hF Γ = Γ * QuantumParallelRepetition.spectralSupportInverse F hF * Γ.conjTranspose

theorem QuantumParallelRepetition.purificationRangeProjection_isHermitian {d : Type u_1} {e : Type u_2} [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) : (purificationRangeProjection F hF Γ).IsHermitian

theorem QuantumParallelRepetition.purificationRangeProjection_idempotent {d : Type u_1} {e : Type u_2} [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) : purificationRangeProjection F hF Γ * purificationRangeProjection F hF Γ = purificationRangeProjection F hF Γ

theorem QuantumParallelRepetition.purificationRangeProjection_complement_posSemidef {d : Type u_1} {e : Type u_2} [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) : (1 - purificationRangeProjection F hF Γ).PosSemidef

noncomputable def QuantumParallelRepetition.purifiedRefinementCore {ι : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype ι] [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (effect : ι → Matrix d d ℂ) (a : ι) : Matrix e e ℂ

Equations

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

theorem QuantumParallelRepetition.purifiedRefinementCore_posSemidef {ι : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype ι] [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (effect : ι → Matrix d d ℂ) (hpositive : ∀ (a : ι), (effect a).PosSemidef) (a : ι) : (purifiedRefinementCore F hF Γ effect a).PosSemidef

theorem QuantumParallelRepetition.purifiedRefinementCore_sum {ι : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype ι] [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (effect : ι → Matrix d d ℂ) (hsum : ∑ a : ι, effect a = F) : ∑ a : ι, purifiedRefinementCore F hF Γ effect a = purificationRangeProjection F hF Γ

noncomputable def QuantumParallelRepetition.purifiedRefinedEffect {ι : 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 ℂ) (effect : ι → Matrix d d ℂ) (a₀ a : ι) : Matrix e e ℂ

Equations

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

theorem QuantumParallelRepetition.purifiedRefinedEffect_posSemidef {ι : 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) (a₀ a : ι) : (purifiedRefinedEffect F hF Γ effect a₀ a).PosSemidef

theorem QuantumParallelRepetition.purifiedRefinedEffect_complete {ι : 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 ℂ) (effect : ι → Matrix d d ℂ) (hsum : ∑ a : ι, effect a = F) (a₀ : ι) : ∑ a : ι, purifiedRefinedEffect F hF Γ effect a₀ a = 1

theorem QuantumParallelRepetition.purificationRangeProjection_compression {d : Type u_1} {e : Type u_2} [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) : Γ.conjTranspose * purificationRangeProjection F hF Γ * Γ = F

theorem QuantumParallelRepetition.purificationRangeProjection_complement_compression {d : Type u_1} {e : Type u_2} [Fintype d] [DecidableEq d] [Fintype e] [DecidableEq e] (F : Matrix d d ℂ) (hF : F.PosSemidef) (Γ : Matrix e d ℂ) (hΓ : Γ.conjTranspose * Γ = F) : Γ.conjTranspose * (1 - purificationRangeProjection F hF Γ) * Γ = 0

theorem QuantumParallelRepetition.purifiedRefinementCore_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 : ι) : Γ.conjTranspose * purifiedRefinementCore F hF Γ effect a * Γ = effect a

theorem QuantumParallelRepetition.purifiedRefinedEffect_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 * purifiedRefinedEffect F hF Γ effect a₀ a * Γ = effect a

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

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)

Equations

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

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

• aliceConditioned : ↥D → X
• bobConditioned : ↥D → Y
• aliceRevealed : ↥L → X
• bobRemaining : ↥(fullHistoryRemaining n D L) → Y

theorem QuantumParallelRepetition.FullSubsetHistory.ext {X : Type u_1} {Y : Type u_2} {inst✝ : Fintype X} {inst✝¹ : Fintype Y} {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} {inst✝ : Fintype X✝} {inst✝¹ : Fintype Y✝} {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} [Fintype X] [Fintype Y] {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥(fullHistoryRemaining n D L) → X) : Fin n → X

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} [Fintype X] [Fintype Y] {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (hidden : ↥L → Y) : Fin n → Y

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.fullHistoryQuestionEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) : FullSubsetHistory X Y n D L × (↥(fullHistoryRemaining n D L) → X) × (↥L → Y) ≃ (Fin n → X) × (Fin n → Y)

Equations

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

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) : ℝ

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) : ℝ

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) : ℝ

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 ℂ

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 ℂ

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) : ℝ

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

def QuantumParallelRepetition.fullQuestionWinIndicator {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)) (xs : Fin n → X) (ys : Fin n → Y) (α : ↥D → A) (β : ↥D → B) : ℝ

Equations

• QuantumParallelRepetition.fullQuestionWinIndicator G D xs ys α β = if ∀ (i : ↥D), G.predicate (xs ↑i) (ys ↑i) (α i) (β i) = true then 1 else 0

theorem QuantumParallelRepetition.fullHistoryWinIndicator_eq_question {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) (hx : ↥(fullHistoryRemaining n D L) → X) (hy : ↥L → Y) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G h α β = fullQuestionWinIndicator G D (fullHistoryAliceQuestion h hx) (fullHistoryBobQuestion h hy) α β

theorem QuantumParallelRepetition.conditionedEffects_postselection_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] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (xs : Fin n → X) (ys : Fin n → Y) : ∑ α : ↥D → A, ∑ β : ↥D → B, fullQuestionWinIndicator G D xs ys α β * ((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 : ↥D), G.predicate (xs ↑i) (ys ↑i) (aa ↑i) (bb ↑i) = true then S.outcomeProbability xs ys aa bb else 0

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.fullQuestionConditionedBornMass_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] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ∑ xs : Fin n → X, ∑ ys : Fin n → Y, ∑ α : ↥D → A, ∑ β : ↥D → B, (G.repeat n).questionWeight xs ys * fullQuestionWinIndicator G D xs ys α β * ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D α xs)) (conditionedBobEffect G n S D β ys) = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)

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] [DecidableEq A] [DecidableEq 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

noncomputable def QuantumParallelRepetition.matrixQuadraticCLM {d : Type u_1} [Fintype d] (x : d → ℂ) : Matrix d d ℂ →L[ℝ] ℂ

Equations

• QuantumParallelRepetition.matrixQuadraticCLM x = LinearMap.toContinuousLinearMap { toFun := fun (A : Matrix d d ℂ) => star x ⬝ᵥ A.mulVec x, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def QuantumParallelRepetition.matrixAdjointCLM {d : Type u_1} [Fintype d] : Matrix d d ℂ →L[ℝ] Matrix d d ℂ

Equations

• QuantumParallelRepetition.matrixAdjointCLM = LinearMap.toContinuousLinearMap { toFun := fun (A : Matrix d d ℂ) => star A, map_add' := ⋯, map_smul' := ⋯ }

theorem QuantumParallelRepetition.bochner_integral_posSemidef {α : Type u_1} {d : Type u_2} [MeasurableSpace α] [Fintype d] [DecidableEq 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.spectralEntropyKernel {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : ℝ) : Matrix d d ℂ

Equations

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

theorem QuantumParallelRepetition.spectralEntropyKernel_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : MeasureTheory.IntegrableOn (spectralEntropyKernel F hF) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.spectralEntropyKernel_eq_scalar_sub_filter {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (s : ℝ) : spectralEntropyKernel F hF s = (1 / (1 + s)) • F - spectralPurificationFilter F hF s

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 ℂ

Equations

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

noncomputable def QuantumParallelRepetition.weightedSpectralEntropyJensen {ι : 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 ℂ

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.weightedSpectralEntropyJensen_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 (weightedSpectralEntropyJensen weight F M positive hM) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.weightedSpectralEntropyJensen_eq_shifted_inverse {ι : 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) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) {s : ℝ} (hs : 0 < s) : weightedSpectralEntropyJensen weight F M positive hM s = s • (∑ i : ι, weight i • (F i + s • 1)⁻¹ - (M + s • 1)⁻¹)

theorem QuantumParallelRepetition.integrated_weighted_spectralPurificationFilter_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 := ⋯; ((∫ (s : ℝ) in Set.Ioi 0, weightedSpectralEntropyJensen weight F M positive hM s) - ∫ (s : ℝ) in Set.Ioi 0, weightedSpectralFilterVariance weight F M positive hM s).PosSemidef

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

noncomputable def QuantumParallelRepetition.diagonalEntropyKernel {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (s : ℝ) : Matrix d d ℂ

Equations

• QuantumParallelRepetition.diagonalEntropyKernel eigenvalue s = Matrix.diagonal fun (i : d) => ↑(eigenvalue i / (1 + s) - eigenvalue i / (eigenvalue i + s))

theorem QuantumParallelRepetition.diagonalEntropyKernel_integrable {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (nonnegative : ∀ (i : d), 0 ≤ eigenvalue i) : MeasureTheory.IntegrableOn (diagonalEntropyKernel eigenvalue) (Set.Ioi 0) MeasureTheory.volume

theorem QuantumParallelRepetition.integral_diagonalEntropyKernel {d : Type u_1} [Fintype d] [DecidableEq d] (eigenvalue : d → ℝ) (nonnegative : ∀ (i : d), 0 ≤ eigenvalue i) : ∫ (s : ℝ) in Set.Ioi 0, diagonalEntropyKernel eigenvalue s = Matrix.diagonal fun (i : d) => ↑(eigenvalue i * Real.log (eigenvalue i))

theorem QuantumParallelRepetition.integral_spectralEntropyKernel_eq_cfc {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) : ∫ (s : ℝ) in Set.Ioi 0, spectralEntropyKernel F hF s = cfc (fun (z : ℝ) => z * Real.log z) F

theorem QuantumParallelRepetition.integral_weightedSpectralEntropyJensen_eq_cfc {ι : 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 : ℝ) in Set.Ioi 0, weightedSpectralEntropyJensen weight F M positive hM s = ∑ i : ι, weight i • cfc (fun (z : ℝ) => z * Real.log z) (F i) - cfc (fun (z : ℝ) => z * Real.log z) M

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] [DecidableEq dB] (ρ : 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 dA] [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)) : ℝ

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 ℂ

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

noncomputable def QuantumParallelRepetition.leftSpectralBornWeight {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) (G : Matrix dB dB ℂ) (i : dA) : ℝ

Equations

• QuantumParallelRepetition.leftSpectralBornWeight ρ F hF G i = ((QuantumParallelRepetition.bornTracePairing ρ.matrix) (QuantumParallelRepetition.positiveMatrixSpectralAtom F hF i)) G

theorem QuantumParallelRepetition.leftSpectralBornWeight_nonneg {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) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (i : dA) : 0 ≤ leftSpectralBornWeight ρ F hF G i

theorem QuantumParallelRepetition.leftSpectralBornWeight_sum {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) (G : Matrix dB dB ℂ) : ∑ i : dA, leftSpectralBornWeight ρ F hF G i = ((bornTracePairing ρ.matrix) 1) G

theorem QuantumParallelRepetition.leftSpectralBornWeight_moment {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) (G : Matrix dB dB ℂ) : ∑ i : dA, leftSpectralBornWeight ρ F hF G i * ⋯.eigenvalues i = ((bornTracePairing ρ.matrix) F) G

theorem QuantumParallelRepetition.leftSpectralBornWeight_entropy {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) (G : Matrix dB dB ℂ) : ((bornTracePairing ρ.matrix) (cfc (fun (z : ℝ) => z * Real.log z) F)) G = ∑ i : dA, leftSpectralBornWeight ρ F hF G i * (⋯.eigenvalues i * Real.log (⋯.eigenvalues 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.leftSpectralBornWeight_negEntropy {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) (G : Matrix dB dB ℂ) : -((bornTracePairing ρ.matrix) (cfc (fun (z : ℝ) => z * Real.log z) F)) G = ∑ i : dA, leftSpectralBornWeight ρ F hF G i * (⋯.eigenvalues i).negMulLog

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)

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 : ℕ) : ℝ

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)

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

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) : ℝ

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)

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 ι] [Fintype d] (v : ι → EuclideanSpace ℂ d) : EuclideanSpace ℂ (ι → d)

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) : ℝ

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) : ℝ

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) : ℝ

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) : ℝ

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} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) : EuclideanSpace ℂ (((_ : κ) × d) × (_ : κ) × d)

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} [Fintype κ] [Fintype d] [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)

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

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} [Fintype κ] [Fintype d] [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} [Fintype κ] [Fintype d] [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] [DecidableEq 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] [DecidableEq 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

noncomputable def QuantumParallelRepetition.weightedComplexOverlapVector {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (σ : ι → ℝ) (μ : κ → ℝ) (L : ι → κ → ℂ) : EuclideanSpace ℂ (ι × κ)

Equations

• QuantumParallelRepetition.weightedComplexOverlapVector σ μ L = WithLp.toLp 2 fun (q : ι × κ) => ↑√(σ q.1 * μ q.2) * L q.1 q.2

theorem QuantumParallelRepetition.weightedComplexOverlapVector_norm_sq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (σ : ι → ℝ) (μ : κ → ℝ) (hσ : ∀ (i : ι), 0 ≤ σ i) (hμ : ∀ (j : κ), 0 ≤ μ j) (L : ι → κ → ℂ) : ‖weightedComplexOverlapVector σ μ L‖ ^ 2 = ∑ i : ι, ∑ j : κ, σ i * μ j * ‖L i j‖ ^ 2

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

theorem QuantumParallelRepetition.twoSidedSchmidtSpectralEnergy_le {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [Fintype ι] [Fintype κ] [Fintype ν] (ψ φ : EuclideanSpace ℂ ν) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) (σ : ι → ℝ) (μ : κ → ℝ) (hσ : ∀ (i : ι), 0 ≤ σ i) (hμ : ∀ (j : κ), 0 ≤ μ j) (hσunit : ∑ i : ι, σ i ^ 2 = 1) (hμunit : ∑ j : κ, μ j ^ 2 = 1) (L R : ι → κ → ℂ) (hLrow : ∀ (i : ι), ∑ j : κ, ‖L i j‖ ^ 2 = 1) (hLcol : ∀ (j : κ), ∑ i : ι, ‖L i j‖ ^ 2 = 1) (hRrow : ∀ (i : ι), ∑ j : κ, ‖R i j‖ ^ 2 = 1) (hRcol : ∀ (j : κ), ∑ i : ι, ‖R i j‖ ^ 2 = 1) (hinner : inner ℂ ψ φ = inner ℂ (weightedComplexOverlapVector σ μ L) (weightedComplexOverlapVector σ μ R)) : ∑ i : ι, ∑ j : κ, (σ i - μ j) ^ 2 * ‖L i j‖ ^ 2 ≤ 2 * ‖ψ - φ‖ ^ 2

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

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)

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 ℂ)

Equations

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

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

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)

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.weightedComplexOverlapVector_inner {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (σ : ι → ℝ) (μ : κ → ℝ) (hσ : ∀ (i : ι), 0 ≤ σ i) (hμ : ∀ (j : κ), 0 ≤ μ j) (L R : ι → κ → ℂ) : inner ℂ (weightedComplexOverlapVector σ μ fun (i : ι) (j : κ) => star (L i j)) (weightedComplexOverlapVector σ μ R) = ∑ i : ι, ∑ j : κ, ↑(σ i) * ↑(μ j) * L i j * R i j

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} [Fintype d] [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) ℂ)

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) ℂ)

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

theorem QuantumParallelRepetition.harmonicNumber_eq_harmonic (n : ℕ) : harmonicNumber n = ↑(harmonic n)

theorem QuantumParallelRepetition.harmonicNumber_log_lower (n : ℕ) : Real.log (↑n + 1) ≤ harmonicNumber n

theorem QuantumParallelRepetition.harmonicNumber_log_upper (n : ℕ) : harmonicNumber n ≤ 1 + Real.log ↑n

theorem QuantumParallelRepetition.harmonicNumber_pos {n : ℕ} (hn : 0 < n) : 0 < harmonicNumber n

theorem QuantumParallelRepetition.harmonicNumber_mul_le_add {d n : ℕ} (hd : 0 < d) (hn : 0 < n) : harmonicNumber (d * n) ≤ harmonicNumber n + (1 + Real.log ↑d)

theorem QuantumParallelRepetition.exists_proofHarmonicNumber_gt (bound : ℝ) : ∃ (n : ℕ), bound < harmonicNumber n

theorem QuantumParallelRepetition.exists_proofHarmonicNumber_ratio_ge (d : ℕ) (hd : 0 < d) {ε : ℝ} (hε : 0 < ε) (hεone : ε ≤ 1) : ∃ (n : ℕ), 0 < n ∧ 1 - ε ≤ harmonicNumber n / harmonicNumber (d * n)

noncomputable def QuantumParallelRepetition.ePRState (m : ℕ) : EuclideanSpace ℂ (Fin m × Fin m)

Equations

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

theorem QuantumParallelRepetition.ePRState_norm (m : ℕ) (hm : 0 < m) : ‖ePRState m‖ = 1

theorem QuantumParallelRepetition.permutationMatrix_mem_unitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : Equiv.Perm.permMatrix ℂ σ ∈ Matrix.unitaryGroup ι ℂ

def QuantumParallelRepetition.permutationUnitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : ↥(Matrix.unitaryGroup ι ℂ)

Equations

• QuantumParallelRepetition.permutationUnitary σ = ⟨Equiv.Perm.permMatrix ℂ σ, ⋯⟩

@[simp]

theorem QuantumParallelRepetition.permutationUnitary_val {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) : ↑(permutationUnitary σ) = Equiv.Perm.permMatrix ℂ σ

theorem QuantumParallelRepetition.localPermutationUnitaryAction_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (ψ : EuclideanSpace ℂ (Fin n × Fin n)) (i j : Fin n) : (localUnitaryAction (permutationUnitary σ) (permutationUnitary σ) ψ).ofLp (i, j) = ψ.ofLp (σ i, σ j)

theorem QuantumParallelRepetition.diagonalInner_real_eq_sum {N : ℕ} (z w : EuclideanSpace ℂ (Fin N × Fin N)) (hz : ∀ (i j : Fin N), i ≠ j → z.ofLp (i, j) = 0) : (inner ℂ z w).re = ∑ i : Fin N, (inner ℂ (z.ofLp (i, i)) (w.ofLp (i, i))).re

theorem QuantumParallelRepetition.harmonicSchmidtFiber_count_sq_le {n : ℕ} (a x : ℝ) (ha : 0 ≤ a) (hx : 0 ≤ x) : ↑{j : Fin n | x ≤ a * (√(↑↑j + 1))⁻¹}.card * x ^ 2 ≤ a ^ 2

noncomputable def QuantumParallelRepetition.harmonicTensorSchmidtAmplitude {d n : ℕ} (σ : Fin d → ℝ) (q : Fin (d * n)) : ℝ

Equations

• QuantumParallelRepetition.harmonicTensorSchmidtAmplitude σ q = σ (finProdFinEquiv.symm q).1 * (√(↑↑(finProdFinEquiv.symm q).2 + 1))⁻¹

noncomputable def QuantumParallelRepetition.descendingHarmonicSchmidtPermutation {d n : ℕ} (σ : Fin d → ℝ) : Equiv.Perm (Fin (d * n))

Equations

• QuantumParallelRepetition.descendingHarmonicSchmidtPermutation σ = Tuple.sort fun (q : Fin (d * n)) => -QuantumParallelRepetition.harmonicTensorSchmidtAmplitude σ q

theorem QuantumParallelRepetition.descendingHarmonicSchmidtPermutation_antitone {d n : ℕ} (σ : Fin d → ℝ) : Antitone fun (q : Fin (d * n)) => harmonicTensorSchmidtAmplitude σ ((descendingHarmonicSchmidtPermutation σ) q)

theorem QuantumParallelRepetition.harmonicSchmidtThreshold_card_eq {d n : ℕ} (σ : Fin d → ℝ) (x : ℝ) : ↑{q : Fin (d * n) | x ≤ harmonicTensorSchmidtAmplitude σ q}.card = ∑ i : Fin d, ↑{j : Fin n | x ≤ σ i * (√(↑↑j + 1))⁻¹}.card

theorem QuantumParallelRepetition.harmonicSchmidtThreshold_count_sq_le_one {d n : ℕ} (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (x : ℝ) (hx : 0 ≤ x) : ↑{q : Fin (d * n) | x ≤ harmonicTensorSchmidtAmplitude σ q}.card * x ^ 2 ≤ 1

theorem QuantumParallelRepetition.descendingHarmonicSchmidtAmplitude_rank_sq_le_one {d n : ℕ} (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (k : Fin (d * n)) : (↑↑k + 1) * harmonicTensorSchmidtAmplitude σ ((descendingHarmonicSchmidtPermutation σ) k) ^ 2 ≤ 1

theorem QuantumParallelRepetition.descendingHarmonicSchmidtAmplitude_le_harmonic {d n : ℕ} (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (k : Fin (d * n)) : harmonicTensorSchmidtAmplitude σ ((descendingHarmonicSchmidtPermutation σ) k) ≤ (√(↑↑k + 1))⁻¹

def QuantumParallelRepetition.diagonalSchmidtUnitVector {d : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) : BipartiteUnitVector d

Equations

• QuantumParallelRepetition.diagonalSchmidtUnitVector σ hunit = ⟨QuantumParallelRepetition.diagonalSchmidtState σ, ⋯⟩

theorem QuantumParallelRepetition.diagonalSchmidtTensorTarget_diagonal {d n : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (q : Fin (d * n)) : (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit)).ofLp (q, q) = ‖rawEmbezzlementState n‖⁻¹ • ↑(harmonicTensorSchmidtAmplitude σ q)

noncomputable def QuantumParallelRepetition.harmonicSchmidtPermutationUnitary {d n : ℕ} (σ : Fin d → ℝ) : ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)

Equations

• QuantumParallelRepetition.harmonicSchmidtPermutationUnitary σ = QuantumParallelRepetition.permutationUnitary (Equiv.symm (QuantumParallelRepetition.descendingHarmonicSchmidtPermutation σ))

theorem QuantumParallelRepetition.harmonicSchmidtPermutationAction_off_diagonal {d n : ℕ} (σ : Fin d → ℝ) (i j : Fin (d * n)) (hij : i ≠ j) : (localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n))).ofLp (i, j) = 0

theorem QuantumParallelRepetition.harmonicSchmidtPermutationAction_diagonal {d n : ℕ} (σ : Fin d → ℝ) (k : Fin (d * n)) : (localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n))).ofLp ((descendingHarmonicSchmidtPermutation σ) k, (descendingHarmonicSchmidtPermutation σ) k) = ‖rawEmbezzlementState (d * n)‖⁻¹ • ↑(√(↑↑k + 1))⁻¹

theorem QuantumParallelRepetition.harmonicTensorSchmidtAmplitude_sq_sum {d n : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) : ∑ q : Fin (d * n), harmonicTensorSchmidtAmplitude σ q ^ 2 = harmonicNumber n

theorem QuantumParallelRepetition.descendingHarmonicSchmidtAmplitude_sq_sum {d n : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) : ∑ k : Fin (d * n), harmonicTensorSchmidtAmplitude σ ((descendingHarmonicSchmidtPermutation σ) k) ^ 2 = harmonicNumber n

noncomputable def QuantumParallelRepetition.universalCatalystOverlapTerm {d n : ℕ} (σ : Fin d → ℝ) (k : Fin (d * n)) : ℝ

Equations

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

theorem QuantumParallelRepetition.universalCatalystOverlap_eq_sum {d n : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) : (inner ℂ (localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n))) (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit))).re = ∑ k : Fin (d * n), universalCatalystOverlapTerm σ k

theorem QuantumParallelRepetition.universalCatalystOverlapTerm_lower {d n : ℕ} (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (k : Fin (d * n)) : ‖rawEmbezzlementState (d * n)‖⁻¹ * ‖rawEmbezzlementState n‖⁻¹ * harmonicTensorSchmidtAmplitude σ ((descendingHarmonicSchmidtPermutation σ) k) ^ 2 ≤ universalCatalystOverlapTerm σ k

theorem QuantumParallelRepetition.universalDiagonalCatalystOverlap_lower {d n : ℕ} (hd : 0 < d) (hn : 0 < n) (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) : ‖rawEmbezzlementState n‖ / ‖rawEmbezzlementState (d * n)‖ ≤ (inner ℂ (localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n))) (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit))).re

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

Equations

• QuantumParallelRepetition.harmonicTargetLiftUnitary U = ⟨(Matrix.reindex finProdFinEquiv finProdFinEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑U) 1), ⋯⟩

@[simp]

theorem QuantumParallelRepetition.harmonicTargetLiftUnitary_apply {d n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (a b : Fin d) (i j : Fin n) : ↑(harmonicTargetLiftUnitary U) (finProdFinEquiv (a, i)) (finProdFinEquiv (b, j)) = if i = j then ↑U a b else 0

theorem QuantumParallelRepetition.localUnitaryAction_comp {m : ℕ} (U₁ V₁ U₂ V₂ : ↥(Matrix.unitaryGroup (Fin m) ℂ)) (ψ : EuclideanSpace ℂ (Fin m × Fin m)) : localUnitaryAction U₁ V₁ (localUnitaryAction U₂ V₂ ψ) = localUnitaryAction (U₁ * U₂) (V₁ * V₂) ψ

theorem QuantumParallelRepetition.targetCatalystDoubleSum_reindex {d n : ℕ} (F : Fin (d * n) → Fin (d * n) → ℂ) : ∑ i : Fin (d * n), ∑ j : Fin (d * n), F i j = ∑ p : Fin d × Fin n, ∑ q : Fin d × Fin n, F (finProdFinEquiv p) (finProdFinEquiv q)

theorem QuantumParallelRepetition.harmonicTargetLift_diagonal_action_apply {d n : ℕ} (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (a b : Fin d) (i j : Fin n) : (localUnitaryAction (harmonicTargetLiftUnitary U) (harmonicTargetLiftUnitary V) (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit))).ofLp (finProdFinEquiv (a, i), finProdFinEquiv (b, j)) = (schmidtVector σ U V).ofLp (a, b) * (embezzlementState n).ofLp (i, j)

theorem QuantumParallelRepetition.harmonicTargetLift_diagonal_action {d n : ℕ} (ξ : BipartiteUnitVector d) (σ : Fin d → ℝ) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (hξ : ↑ξ = schmidtVector σ U V) : localUnitaryAction (harmonicTargetLiftUnitary U) (harmonicTargetLiftUnitary V) (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit)) = tensorEmbezzlementTarget ξ

theorem QuantumParallelRepetition.localUnitaryAction_sub {m : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin m) ℂ)) (z w : EuclideanSpace ℂ (Fin m × Fin m)) : localUnitaryAction U V (z - w) = localUnitaryAction U V z - localUnitaryAction U V w

theorem QuantumParallelRepetition.universalDiagonalCatalystOverlap_of_harmonic_ratio {d n : ℕ} (hd : 0 < d) (hn : 0 < n) (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (δ : ℝ) (hδ : 0 ≤ δ) (hδone : δ ≤ 1) (hratio : 1 - δ ≤ harmonicNumber n / harmonicNumber (d * n)) : 1 - δ ≤ (inner ℂ (localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n))) (tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit))).re

theorem QuantumParallelRepetition.universalDiagonalCatalyst_distance {d n : ℕ} (hd : 0 < d) (hn : 0 < n) (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), 0 ≤ σ i) (hunit : ∑ i : Fin d, σ i ^ 2 = 1) (δ : ℝ) (hδ : 0 ≤ δ) (hδone : δ ≤ 1) (hratio : 1 - δ ≤ harmonicNumber n / harmonicNumber (d * n)) : ‖localUnitaryAction (harmonicSchmidtPermutationUnitary σ) (harmonicSchmidtPermutationUnitary σ) (embezzlementState (d * n)) - tensorEmbezzlementTarget (diagonalSchmidtUnitVector σ hunit)‖ ≤ √(2 * δ)

theorem QuantumParallelRepetition.exists_proofUniversalHarmonicCatalyst (d : ℕ) (hd : 0 < d) (ε : ℝ) (hε : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∀ (ξ : BipartiteUnitVector d), ∃ (U : ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)) (V : ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)), ‖localUnitaryAction U V (embezzlementState (d * n)) - tensorEmbezzlementTarget ξ‖ ≤ ε

def QuantumParallelRepetition.coherentSharedRandomControlledUnitary {Ω : Type u_1} {d : Type u_2} [Fintype Ω] [Fintype d] [DecidableEq Ω] [DecidableEq d] (U : Ω → ↥(Matrix.unitaryGroup d ℂ)) : ↥(Matrix.unitaryGroup ((_ : Ω) × d) ℂ)

Equations

• QuantumParallelRepetition.coherentSharedRandomControlledUnitary U = ⟨Matrix.blockDiagonal' fun (ω : Ω) => ↑(U ω), ⋯⟩

noncomputable def QuantumParallelRepetition.spectralPartitionPOVM {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (bin : d → κ) : POVM κ d

Equations

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

theorem QuantumParallelRepetition.spectralPartitionPOVM_projective {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (bin : d → κ) (k : κ) : (spectralPartitionPOVM F hF bin).effect k * (spectralPartitionPOVM F hF bin).effect k = (spectralPartitionPOVM F hF bin).effect k

def QuantumParallelRepetition.bilateralWorkPairEquiv {ι : Type u_1} {d : Type u_2} {e : Type u_3} : (ι → d) × (ι → e) ≃ (ι → d × e)

Equations

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

theorem QuantumParallelRepetition.spectralPartitionPOVM_trace_eq_atom_count {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (bin : d → κ) (k : κ) : ((spectralPartitionPOVM F hF bin).effect k).trace.re = ∑ i : d, if bin i = k then 1 else 0

theorem QuantumParallelRepetition.spectralPartitionPOVM_trace_mul_eq_atom_overlap {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (binF binG : d → κ) (k : κ) : ((spectralPartitionPOVM F hF binF).effect k * (spectralPartitionPOVM G hG binG).effect k).trace.re = ∑ i : d with binF i = k, ∑ j : d with binG j = k, spectralAtomOverlap F G hF hG i j

theorem QuantumParallelRepetition.spectralPartitionPOVM_weighted_trace_deficit_eq_mismatch {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (binF binG : d → κ) (τ : κ → ℝ) : ∑ k : κ, τ k ^ 2 * ((spectralPartitionPOVM G hG binG).effect k).trace.re - ∑ k : κ, τ k ^ 2 * ((spectralPartitionPOVM F hF binF).effect k * (spectralPartitionPOVM G hG binG).effect k).trace.re = ∑ i : d, ∑ j : d, if binF i = binG j then 0 else τ (binG j) ^ 2 * spectralAtomOverlap F G hF hG i j

noncomputable def QuantumParallelRepetition.finiteUniformThresholdGrid (lower upper : ℝ) (N : ℕ) (k : Fin N) : ℝ

Equations

• QuantumParallelRepetition.finiteUniformThresholdGrid lower upper N k = lower + ↑↑k * ((upper - lower) / ↑N)

noncomputable def QuantumParallelRepetition.finiteUniformThresholdCrossing (lower upper a b : ℝ) (N : ℕ) : ℝ

Equations

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

theorem QuantumParallelRepetition.finiteUniformGrid_interval_card_le (N : ℕ) (offset step lo hi : ℝ) (positive : 0 < step) (ordered : lo ≤ hi) : ↑{k : Fin N | lo ≤ offset + ↑↑k * step ∧ offset + ↑↑k * step ≤ hi}.card ≤ (hi - lo) / step + 1

theorem QuantumParallelRepetition.finiteUniformThresholdCrossing_le {lower upper : ℝ} (window : lower < upper) (a b : ℝ) (N : ℕ) (nonempty : 0 < N) : finiteUniformThresholdCrossing lower upper a b N ≤ |a - b| / (upper - lower) + 1 / ↑N

theorem QuantumParallelRepetition.localUnitaryPureResidual_targetLocalInverse_reset {n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (x : EuclideanSpace ℂ (Fin n × Fin n)) : localUnitaryAction U⁻¹ V⁻¹ (localUnitaryAction U V x) = x

def QuantumParallelRepetition.targetCoefficientMatrix {d : ℕ} (ξ : BipartiteUnitVector d) : Matrix (Fin d) (Fin d) ℂ

Equations

• QuantumParallelRepetition.targetCoefficientMatrix ξ b a = (↑ξ).ofLp (a, b)

theorem QuantumParallelRepetition.targetCoefficientMatrix_vec {d : ℕ} (ξ : BipartiteUnitVector d) : WithLp.toLp 2 (targetCoefficientMatrix ξ).vec = ↑ξ

def QuantumParallelRepetition.targetReducedDensity {d : ℕ} (ξ : BipartiteUnitVector d) : Matrix (Fin d) (Fin d) ℂ

Equations

• QuantumParallelRepetition.targetReducedDensity ξ = (QuantumParallelRepetition.targetCoefficientMatrix ξ).conjTranspose * QuantumParallelRepetition.targetCoefficientMatrix ξ

theorem QuantumParallelRepetition.targetReducedDensity_posSemidef {d : ℕ} (ξ : BipartiteUnitVector d) : (targetReducedDensity ξ).PosSemidef

theorem QuantumParallelRepetition.targetReducedDensity_trace {d : ℕ} (ξ : BipartiteUnitVector d) : (targetReducedDensity ξ).trace = 1

theorem QuantumParallelRepetition.targetSpectralAtom_apply {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i a b : d) : positiveMatrixSpectralAtom F hF i a b = ↑⋯.eigenvectorUnitary a i * star (↑⋯.eigenvectorUnitary b i)

theorem QuantumParallelRepetition.targetSpectralAtomOverlap_eq_basis_norm_sq {d : Type u_1} [Fintype d] [DecidableEq d] (F G : Matrix d d ℂ) (hF : F.PosSemidef) (hG : G.PosSemidef) (i j : d) : spectralAtomOverlap F G hF hG i j = ‖↑(unitaryBasisOverlap ⋯.eigenvectorUnitary ⋯.eigenvectorUnitary) i j‖ ^ 2

noncomputable def QuantumParallelRepetition.targetCanonicalSchmidtCoefficient {d : ℕ} (ξ : BipartiteUnitVector d) (i : Fin d) : ℝ

Equations

• QuantumParallelRepetition.targetCanonicalSchmidtCoefficient ξ i = √(⋯.eigenvalues i)

theorem QuantumParallelRepetition.targetCanonicalSchmidtCoefficient_nonneg {d : ℕ} (ξ : BipartiteUnitVector d) (i : Fin d) : 0 ≤ targetCanonicalSchmidtCoefficient ξ i

theorem QuantumParallelRepetition.targetCanonicalSchmidtCoefficient_sq_sum {d : ℕ} (ξ : BipartiteUnitVector d) : ∑ i : Fin d, targetCanonicalSchmidtCoefficient ξ i ^ 2 = 1

theorem QuantumParallelRepetition.exists_proofTargetCanonicalSpectralSchmidtDecomposition {d : ℕ} (ξ : BipartiteUnitVector d) : ∃ (V : ↥(Matrix.unitaryGroup (Fin d) ℂ)), ↑ξ = schmidtVector (targetCanonicalSchmidtCoefficient ξ) (conjugateUnitary ⋯.eigenvectorUnitary) V

theorem QuantumParallelRepetition.conjugateUnitaryBasisOverlap_norm_sq {d : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (i j : Fin d) : ‖↑(unitaryBasisOverlap (conjugateUnitary U) (conjugateUnitary V)) i j‖ ^ 2 = ‖↑(unitaryBasisOverlap U V) i j‖ ^ 2

noncomputable def QuantumParallelRepetition.targetCanonicalSpectralEnergy {d : ℕ} (ξ ζ : BipartiteUnitVector d) : ℝ

Equations

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

theorem QuantumParallelRepetition.targetCanonicalSpectralEnergy_le_of_canonicalSchmidt {d : ℕ} (ξ ζ : BipartiteUnitVector d) (V W : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (hξ : ↑ξ = schmidtVector (fun (i : Fin d) => √(⋯.eigenvalues i)) (conjugateUnitary ⋯.eigenvectorUnitary) V) (hζ : ↑ζ = schmidtVector (fun (j : Fin d) => √(⋯.eigenvalues j)) (conjugateUnitary ⋯.eigenvectorUnitary) W) : targetCanonicalSpectralEnergy ξ ζ ≤ 2 * ‖↑ξ - ↑ζ‖ ^ 2

theorem QuantumParallelRepetition.targetCanonicalSpectralEnergy_le {d : ℕ} (ξ ζ : BipartiteUnitVector d) : targetCanonicalSpectralEnergy ξ ζ ≤ 2 * ‖↑ξ - ↑ζ‖ ^ 2

theorem QuantumParallelRepetition.harmonicCoherentSharedResource_inverseAbsorption_distance {d n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)) (resource : BipartiteUnitVector d) : ‖localUnitaryAction U⁻¹ V⁻¹ (tensorEmbezzlementTarget resource) - embezzlementState (d * n)‖ = ‖localUnitaryAction U V (embezzlementState (d * n)) - tensorEmbezzlementTarget resource‖

theorem QuantumParallelRepetition.dSVProjectorSquaredDifference_trace {d : Type u_1} [Fintype d] [DecidableEq d] (P Q : Matrix d d ℂ) (hP : P * P = P) (hQ : Q * Q = Q) : ((P - Q) * (P - Q)).trace.re = P.trace.re + Q.trace.re - 2 * (P * Q).trace.re

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_card {d : ℕ} (r : Fin (d + 1)) : {i : Fin d | ↑i < ↑r}.card = ↑r

def QuantumParallelRepetition.dSVCanonicalFailurePrefix {d : ℕ} (r : Fin (d + 1)) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

• QuantumParallelRepetition.dSVCanonicalFailurePrefix r = WithLp.toLp 2 fun (q : Fin d × Fin d) => if q.1 = q.2 ∧ ↑q.1 < ↑r then 1 else 0

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_norm_sq {d : ℕ} (r : Fin (d + 1)) : ‖dSVCanonicalFailurePrefix r‖ ^ 2 = ↑↑r

theorem QuantumParallelRepetition.dSVProjectorComplement_posSemidef {d : Type u_1} [Fintype d] [DecidableEq d] (P : Matrix d d ℂ) (positive : P.PosSemidef) (projective : P * P = P) : (1 - P).PosSemidef

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_inner {d : ℕ} (r s : Fin (d + 1)) : inner ℂ (dSVCanonicalFailurePrefix r) (dSVCanonicalFailurePrefix s) = ↑(min ↑r ↑s)

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_sub_norm_sq {d : ℕ} (r s : Fin (d + 1)) : ‖dSVCanonicalFailurePrefix r - dSVCanonicalFailurePrefix s‖ ^ 2 = |↑↑r - ↑↑s|

noncomputable def QuantumParallelRepetition.dSVRankControlledTargetCatalystIndexEquiv {ι : Type u_1} [Fintype ι] (d n : ℕ) : (Fin d × ι) × Fin n ≃ Fin (d * (Fintype.card ι * n))

Equations

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