Quantum parallel repetition, part 02

@[instance_reducible]

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

The local matrix norm instance used while elaborating part two.

Equations

• QuantumParallelRepetition.matrixComplexContinuousENormPartTwo = SeminormedAddGroup.toContinuousENorm

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)

The quantum state representing e pr.

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

The unitary operator implementing permutation.

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

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

The unitary operator implementing coherent shared random controlled.

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

The positive operator-valued measurement implementing spectral partition.

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

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

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.localUnitaryPureResidual_targetLocalInverse_reset {n : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (x : EuclideanSpace ℂ (Fin n × Fin n)) : localUnitaryAction U⁻¹ V⁻¹ (localUnitaryAction U V x) = x

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

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

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] (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)

The DSV canonical failure prefix construction used in the quantum parallel-repetition argument.

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

The finite equivalence encoding DSV rank controlled target catalyst index.

Equations

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

theorem QuantumParallelRepetition.dSVMixedProjectorSuccessLoss_le_square {d : Type u_1} [Fintype d] [DecidableEq d] (P R : Matrix d d ℂ) (hcomplement : (1 - P).PosSemidef) (hR : R.PosSemidef) (hPP : P * P = P) (hRR : R * R = R) : P.trace.re - (P * R).trace.re ≤ ((P - R) * (P - R)).trace.re

theorem QuantumParallelRepetition.dSVWeightedMixedProjectorSuccessLoss_le_square {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq d] (w : κ → ℝ) (nonnegative : ∀ (k : κ), 0 ≤ w k) (P R : κ → Matrix d d ℂ) (hcomplement : ∀ (k : κ), (1 - P k).PosSemidef) (hR : ∀ (k : κ), (R k).PosSemidef) (hPP : ∀ (k : κ), P k * P k = P k) (hRR : ∀ (k : κ), R k * R k = R k) : ∑ k : κ, w k * (P k).trace.re - ∑ k : κ, w k * (P k * R k).trace.re ≤ ∑ k : κ, w k * ((P k - R k) * (P k - R k)).trace.re

def QuantumParallelRepetition.dSVGlobalProjectorBinaryPOVM {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (P : κ → Matrix d d ℂ) (positive : ∀ (k : κ), (P k).PosSemidef) (complement : ∀ (k : κ), (1 - P k).PosSemidef) : POVM Bool ((_ : κ) × d)

The positive operator-valued measurement implementing DSV global projector binary.

Equations

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

theorem QuantumParallelRepetition.dSVGlobalProjectorBinaryPOVM_projective {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (P : κ → Matrix d d ℂ) (positive : ∀ (k : κ), (P k).PosSemidef) (complement : ∀ (k : κ), (1 - P k).PosSemidef) (projective : ∀ (k : κ), P k * P k = P k) (b : Bool) : (dSVGlobalProjectorBinaryPOVM P positive complement).effect b * (dSVGlobalProjectorBinaryPOVM P positive complement).effect b = (dSVGlobalProjectorBinaryPOVM P positive complement).effect b

theorem QuantumParallelRepetition.dSVActualGlobalMixedBornSuccess_eq {κ : Type u_1} {d : Type u_2} [Fintype κ] [Fintype d] [DecidableEq κ] [DecidableEq d] (τ : κ → ℝ) (k₀ : κ) (i₀ : d) (nonzero : τ k₀ ≠ 0) (P R : κ → Matrix d d ℂ) (hP : ∀ (k : κ), (P k).PosSemidef) (hPc : ∀ (k : κ), (1 - P k).PosSemidef) (hR : ∀ (k : κ), (R k).PosSemidef) (hRc : ∀ (k : κ), (1 - R k).PosSemidef) (hPP : ∀ (k : κ), P k * P k = P k) (hRR : ∀ (k : κ), R k * R k = R k) : binaryJointSuccessProbability (pureDensityMatrix (sharedThresholdResource τ) ⋯) (dSVGlobalProjectorBinaryPOVM P hP hPc) (transposePOVM (dSVGlobalProjectorBinaryPOVM R hR hRc)) = (∑ k : κ, τ k ^ 2 * (P k * R k).trace.re) / (↑(Fintype.card d) * ∑ k : κ, τ k ^ 2)

noncomputable def QuantumParallelRepetition.dSVRationalSoftPass (t x : ℝ) : ℝ

The DSV rational soft pass construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.dSVRationalSoftPass t x = x / (x + t)

theorem QuantumParallelRepetition.dSVRationalSoftPass_mem_unit {t x : ℝ} (positive : 0 < t) (nonnegative : 0 ≤ x) : 0 ≤ dSVRationalSoftPass t x ∧ dSVRationalSoftPass t x ≤ 1

theorem QuantumParallelRepetition.dSVRationalSoftPass_sub {t a b : ℝ} (positive : 0 < t) (ha : 0 ≤ a) (hb : 0 ≤ b) : dSVRationalSoftPass t a - dSVRationalSoftPass t b = t * (a - b) / ((a + t) * (b + t))

theorem QuantumParallelRepetition.dSVRationalSoftPass_lipschitz {t a b : ℝ} (positive : 0 < t) (ha : 0 ≤ a) (hb : 0 ≤ b) : |dSVRationalSoftPass t a - dSVRationalSoftPass t b| ≤ |a - b| / t

theorem QuantumParallelRepetition.dSVAdaptiveSoft_sqrt_sub_sq_le_abs (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : (√a - √b) ^ 2 ≤ |a - b|

def QuantumParallelRepetition.dSVSoftBobLeftReducedDensity {d : ℕ} (ζ : BipartiteUnitVector d) : Matrix (Fin d) (Fin d) ℂ

The DSV soft bob left reduced density construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.dSVSoftBobLeftReducedDensity ζ = QuantumParallelRepetition.targetCoefficientMatrix✝ ζ * (QuantumParallelRepetition.targetCoefficientMatrix✝ ζ).conjTranspose

theorem QuantumParallelRepetition.dSVSoftBobLeftReducedDensity_posSemidef {d : ℕ} (ζ : BipartiteUnitVector d) : (dSVSoftBobLeftReducedDensity ζ).PosSemidef

theorem QuantumParallelRepetition.dSVSoftBobLeftReducedDensity_trace {d : ℕ} (ζ : BipartiteUnitVector d) : (dSVSoftBobLeftReducedDensity ζ).trace = 1

def QuantumParallelRepetition.dSVOriginalComputationalReindexedUnitary {ι : Type u_1} [Fintype ι] [DecidableEq ι] {D : ℕ} (e : ι ≃ Fin D) (U : ↥(Matrix.unitaryGroup ι ℂ)) : ↥(Matrix.unitaryGroup (Fin D) ℂ)

The unitary operator implementing DSV original computational reindexed.

Equations

• QuantumParallelRepetition.dSVOriginalComputationalReindexedUnitary e U = ⟨(Matrix.reindex e e) ↑U, ⋯⟩

def QuantumParallelRepetition.dSVHeterogeneousRealPrefix (continuation : ℕ → ℝ) (k : ℕ) : ℝ

The DSV heterogeneous real prefix construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.dSVHeterogeneousRealPrefix continuation k = ∏ i ∈ Finset.range k, continuation i

theorem QuantumParallelRepetition.dSVHeterogeneousRealPrefix_succ (continuation : ℕ → ℝ) (k : ℕ) : dSVHeterogeneousRealPrefix continuation (k + 1) = dSVHeterogeneousRealPrefix continuation k * continuation k

theorem QuantumParallelRepetition.dSVHeterogeneousRealStopping_escape_identity (continuation : ℕ → ℝ) (N : ℕ) : ∑ k ∈ Finset.range N, dSVHeterogeneousRealPrefix continuation k * (1 - continuation k) = 1 - dSVHeterogeneousRealPrefix continuation N

theorem QuantumParallelRepetition.dSVHeterogeneousRealPrefix_nonneg (continuation : ℕ → ℝ) (nonnegative : ∀ (k : ℕ), 0 ≤ continuation k) (k : ℕ) : 0 ≤ dSVHeterogeneousRealPrefix continuation k

theorem QuantumParallelRepetition.dSVHeterogeneousRealStopping_escape_budget (continuation escape : ℕ → ℝ) (continuation_nonnegative : ∀ (k : ℕ), 0 ≤ continuation k) (escape_bound : ∀ (k : ℕ), continuation k + escape k ≤ 1) (N : ℕ) : ∑ k ∈ Finset.range N, dSVHeterogeneousRealPrefix continuation k * escape k ≤ 1

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVUniformDensityThresholdLocalIndex (N d : ℕ) : Type

The type used to represent DSV uniform density threshold local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.DSVUniformDensityThresholdLocalIndex N d = ((_ : Fin N) × Fin d)

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdSharedState (N d : ℕ) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The quantum state representing DSV uniform density threshold shared.

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdSharedState N d = QuantumParallelRepetition.sharedThresholdResource fun (x : Fin N) => 1

theorem QuantumParallelRepetition.dSVUniformDensityThresholdRaw_norm_sq (N d : ℕ) : ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖ ^ 2 = ↑d * ↑N

theorem QuantumParallelRepetition.dSVUniformDensityThresholdSharedState_norm {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) : ‖dSVUniformDensityThresholdSharedState N d‖ = 1

theorem QuantumParallelRepetition.dSVUniformDensityThresholdSharedState_mismatchedFlag (N d : ℕ) (k l : Fin N) (i j : Fin d) (different : k ≠ l) : (dSVUniformDensityThresholdSharedState N d).ofLp (⟨k, i⟩, ⟨l, j⟩) = 0

theorem QuantumParallelRepetition.dSVUniformDensityThresholdSharedState_mismatchedWork (N d : ℕ) (k l : Fin N) (i j : Fin d) (different : i ≠ j) : (dSVUniformDensityThresholdSharedState N d).ofLp (⟨k, i⟩, ⟨l, j⟩) = 0

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdSharedDensity {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) : DensityMatrix (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The DSV uniform density threshold shared density construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityThresholdShared_mixedBorn_eq {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) (P R : Fin N → Matrix (Fin d) (Fin d) ℂ) (hP : ∀ (k : Fin N), (P k).PosSemidef) (hPc : ∀ (k : Fin N), (1 - P k).PosSemidef) (hR : ∀ (k : Fin N), (R k).PosSemidef) (hRc : ∀ (k : Fin N), (1 - R k).PosSemidef) (hPP : ∀ (k : Fin N), P k * P k = P k) (hRR : ∀ (k : Fin N), R k * R k = R k) : binaryJointSuccessProbability (dSVUniformDensityThresholdSharedDensity grid dimension) (dSVGlobalProjectorBinaryPOVM P hP hPc) (transposePOVM (dSVGlobalProjectorBinaryPOVM R hR hRc)) = (∑ k : Fin N, (P k * R k).trace.re) / (↑d * ↑N)

theorem QuantumParallelRepetition.dSVUniformDensityThresholdShared_diagonalBorn_eq {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) (P : Fin N → Matrix (Fin d) (Fin d) ℂ) (hP : ∀ (k : Fin N), (P k).PosSemidef) (hPc : ∀ (k : Fin N), (1 - P k).PosSemidef) (hPP : ∀ (k : Fin N), P k * P k = P k) : binaryJointSuccessProbability (dSVUniformDensityThresholdSharedDensity grid dimension) (dSVGlobalProjectorBinaryPOVM P hP hPc) (transposePOVM (dSVGlobalProjectorBinaryPOVM P hP hPc)) = (∑ k : Fin N, (P k).trace.re) / (↑d * ↑N)

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVUniformDensityIndependentHistoryLocalIndex (L N d : ℕ) : Type

The type used to represent DSV uniform density independent history local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.DSVUniformDensityIndependentHistoryLocalIndex L N d = (Fin L → QuantumParallelRepetition.DSVUniformDensityThresholdLocalIndex N d)

noncomputable def QuantumParallelRepetition.dSVUniformDensityIndependentSharedState (L N d : ℕ) : EuclideanSpace ℂ (DSVUniformDensityIndependentHistoryLocalIndex L N d × DSVUniformDensityIndependentHistoryLocalIndex L N d)

The quantum state representing DSV uniform density independent shared.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityIndependentSharedState_apply (L N d : ℕ) (alice bob : DSVUniformDensityIndependentHistoryLocalIndex L N d) : (dSVUniformDensityIndependentSharedState L N d).ofLp (alice, bob) = ∏ j : Fin L, (dSVUniformDensityThresholdSharedState N d).ofLp (alice j, bob j)

theorem QuantumParallelRepetition.dSVUniformDensityIndependentSharedState_norm (L : ℕ) {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) : ‖dSVUniformDensityIndependentSharedState L N d‖ = 1

theorem QuantumParallelRepetition.ClassicalSampling.swap_mem_iff_of_mem {α : Type u_1} [DecidableEq α] {marked : Finset α} {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) (a : α) : (Equiv.swap x y) a ∈ marked ↔ a ∈ marked

noncomputable def QuantumParallelRepetition.ClassicalSampling.uniformPermutationProbability {α : Type u_1} [Fintype α] [DecidableEq α] (event : Equiv.Perm α → Prop) : ℝ

The probability of uniform permutation.

Equations

• QuantumParallelRepetition.ClassicalSampling.uniformPermutationProbability event = ↑{permutation : Equiv.Perm α | event permutation}.card / ↑(Fintype.card (Equiv.Perm α))

def QuantumParallelRepetition.ClassicalSampling.rationalMarked {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) : Finset (β × Fin denominator)

The rational marked construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.ClassicalSampling.rationalMarked denominator numerator = {point : β × Fin denominator | ↑point.2 < numerator point.1}

theorem QuantumParallelRepetition.ClassicalSampling.rationalMarked_fiber_card {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (letter : β) : {point ∈ rationalMarked denominator numerator | point.1 = letter}.card = min denominator (numerator letter)

theorem QuantumParallelRepetition.ClassicalSampling.rationalNumerator_le_denominator {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (letter : β) : numerator letter ≤ denominator

theorem QuantumParallelRepetition.ClassicalSampling.rationalMarked_card {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) : (rationalMarked denominator numerator).card = denominator

theorem QuantumParallelRepetition.ClassicalSampling.rationalMarked_nonempty {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (positive : 0 < denominator) : (rationalMarked denominator numerator).Nonempty

theorem QuantumParallelRepetition.Pinsker.centered_log_lower_of_one_le {x : ℝ} (hx : 1 ≤ x) : 2 * (x - 1) / (x + 1) ≤ Real.log x

theorem QuantumParallelRepetition.Pinsker.centered_log_upper_of_le_one {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : Real.log x ≤ 2 * (x - 1) / (x + 1)

theorem QuantumParallelRepetition.Pinsker.pinsker_rational_coefficient_le {x : ℝ} (hx : 0 < x) : 3 * (x + 5) / (2 * (x + 2) ^ 2) ≤ 2 / (x + 1)

theorem QuantumParallelRepetition.Pinsker.pinskerScalarGap_derivative_nonneg {x : ℝ} (hx : 1 ≤ x) : 0 ≤ Real.log x - 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2)

theorem QuantumParallelRepetition.Pinsker.pinskerScalarGap_derivative_nonpos {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : Real.log x - 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2) ≤ 0

theorem QuantumParallelRepetition.Pinsker.quadratic_le_klFun {x : ℝ} (hx : 0 ≤ x) : 3 * (x - 1) ^ 2 / (2 * (x + 2)) ≤ InformationTheory.klFun x

noncomputable def QuantumParallelRepetition.Pinsker.finiteRelativeEntropy {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : ℝ

The entropy quantity for finite relative.

Equations

• QuantumParallelRepetition.Pinsker.finiteRelativeEntropy p q = ∑ i : ι, q i * InformationTheory.klFun (p i / q i)

noncomputable def QuantumParallelRepetition.Pinsker.finiteTotalVariation {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : ℝ

The finite total variation construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.Pinsker.finiteTotalVariation p q = (∑ i : ι, |p i - q i|) / 2

theorem QuantumParallelRepetition.Pinsker.quadratic_density_le_weighted_kl {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) : 3 * (p - q) ^ 2 / (2 * (p + 2 * q)) ≤ q * InformationTheory.klFun (p / q)

theorem QuantumParallelRepetition.Pinsker.finiteRelativeEntropy_eq_log_sum {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hq : ∀ (i : ι), 0 < q i) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteRelativeEntropy p q = ∑ i : ι, p i * Real.log (p i / q i)

theorem QuantumParallelRepetition.Pinsker.finite_pinsker {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 < q i) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : 2 * finiteTotalVariation p q ^ 2 ≤ finiteRelativeEntropy p q

theorem QuantumParallelRepetition.Pinsker.sum_over_positive_reference_support {ι : Type u_1} [Fintype ι] (q f : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (hzero : ∀ (i : ι), q i = 0 → f i = 0) : ∑ i : { i : ι // 0 < q i }, f ↑i = ∑ i : ι, f i

theorem QuantumParallelRepetition.Pinsker.finite_pinsker_of_absolute_continuity {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : 2 * finiteTotalVariation p q ^ 2 ≤ finiteRelativeEntropy p q

theorem QuantumParallelRepetition.Pinsker.finiteRelativeEntropy_eq_log_sum_of_absolute_continuity {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteRelativeEntropy p q = ∑ i : ι, p i * Real.log (p i / q i)

theorem QuantumParallelRepetition.Pinsker.finite_pinsker_sqrt_of_absolute_continuity {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteTotalVariation p q ≤ √(finiteRelativeEntropy p q / 2)

noncomputable def QuantumParallelRepetition.ClassicalInformation.distributionFloorNumerator {ι : Type u_1} (denominator : ℕ) (p : ι → ℝ) : ι → ℕ

The distribution floor numerator construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.ClassicalInformation.distributionFloorNumerator denominator p i = ⌊p i * ↑denominator⌋₊

noncomputable def QuantumParallelRepetition.ClassicalInformation.distributionFloorResidual {ι : Type u_1} [Fintype ι] (denominator : ℕ) (p : ι → ℝ) : ℕ

The distribution floor residual construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.ClassicalInformation.distributionRoundedNumerator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) : ι → ℕ

The distribution rounded numerator construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.ClassicalInformation.distributionRoundedProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) : ι → ℝ

The probability of distribution rounded.

Equations

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

theorem QuantumParallelRepetition.ClassicalInformation.distributionFloorNumerator_cast_le {ι : Type u_1} (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (i : ι) : ↑(distributionFloorNumerator denominator p i) ≤ p i * ↑denominator

theorem QuantumParallelRepetition.ClassicalInformation.distributionFloorNumerator_sum_le {ι : Type u_1} [Fintype ι] (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ∑ i : ι, distributionFloorNumerator denominator p i ≤ denominator

theorem QuantumParallelRepetition.ClassicalInformation.distributionRoundedNumerator_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ∑ i : ι, distributionRoundedNumerator base denominator p i = denominator

theorem QuantumParallelRepetition.ClassicalInformation.distributionRoundedProbability_totalVariation_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : Pinsker.finiteTotalVariation p (distributionRoundedProbability base denominator p) ≤ ↑(Fintype.card ι) / ↑denominator

theorem QuantumParallelRepetition.ClassicalInformation.finite_log_sum_inequality {ι : Type u_1} (indices : Finset ι) (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (positive_mass : 0 < ∑ i ∈ indices, q i) : (∑ i ∈ indices, q i) * InformationTheory.klFun ((∑ i ∈ indices, p i) / ∑ i ∈ indices, q i) ≤ ∑ i ∈ indices, q i * InformationTheory.klFun (p i / q i)

def QuantumParallelRepetition.ClassicalInformation.groupedMass {ι : Type u_1} [Fintype ι] {κ : Type u_2} [DecidableEq κ] (map : ι → κ) (p : ι → ℝ) (j : κ) : ℝ

The total probability mass of grouped.

Equations

• QuantumParallelRepetition.ClassicalInformation.groupedMass map p j = ∑ i : ι with map i = j, p i

theorem QuantumParallelRepetition.ClassicalInformation.groupedMass_eq_sum_ite {ι : Type u_1} [Fintype ι] {κ : Type u_2} [DecidableEq κ] (map : ι → κ) (p : ι → ℝ) (j : κ) : groupedMass map p j = ∑ i : ι, if map i = j then p i else 0

Express a grouped mass as an indicator-weighted sum over its source.

theorem QuantumParallelRepetition.ClassicalInformation.finite_relative_entropy_data_processing {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (map : ι → κ) (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) : Pinsker.finiteRelativeEntropy (groupedMass map p) (groupedMass map q) ≤ Pinsker.finiteRelativeEntropy p q

def QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) : ι → ℝ

The marginal distribution of joint first.

Equations

• QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal joint i = ∑ j : κ, joint (i, j)

noncomputable def QuantumParallelRepetition.ClassicalInformation.jointConditional {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (i : ι) : κ → ℝ

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

Equations

• QuantumParallelRepetition.ClassicalInformation.jointConditional joint i j = joint (i, j) / QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal joint i

theorem QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (nonnegative : ∀ (point : ι × κ), 0 ≤ joint point) (i : ι) : 0 ≤ jointFirstMarginal joint i

theorem QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal_sum {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) : ∑ i : ι, jointFirstMarginal joint i = ∑ point : ι × κ, joint point

theorem QuantumParallelRepetition.ClassicalInformation.jointFirstMarginal_absolute_continuity {ι : Type u_1} {κ : Type u_2} [Fintype κ] (p q : ι × κ → ℝ) (hq : ∀ (point : ι × κ), 0 ≤ q point) (absolute_continuity : ∀ (point : ι × κ), q point = 0 → p point = 0) (i : ι) : jointFirstMarginal q i = 0 → jointFirstMarginal p i = 0

theorem QuantumParallelRepetition.ClassicalInformation.jointConditional_sum {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (i : ι) (nonzero : jointFirstMarginal joint i ≠ 0) : ∑ j : κ, jointConditional joint i j = 1

theorem QuantumParallelRepetition.ClassicalInformation.finite_relative_entropy_joint_chain_rule {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (p q : ι × κ → ℝ) (hp : ∀ (point : ι × κ), 0 ≤ p point) (hq : ∀ (point : ι × κ), 0 ≤ q point) (absolute_continuity : ∀ (point : ι × κ), q point = 0 → p point = 0) (hp_normalized : ∑ point : ι × κ, p point = 1) (hq_normalized : ∑ point : ι × κ, q point = 1) : Pinsker.finiteRelativeEntropy p q = Pinsker.finiteRelativeEntropy (jointFirstMarginal p) (jointFirstMarginal q) + ∑ i : ι, jointFirstMarginal p i * Pinsker.finiteRelativeEntropy (jointConditional p i) (jointConditional q i)

noncomputable def QuantumParallelRepetition.ClassicalInformation.rationalPermutationOutput {ι : Type u_1} [Fintype ι] (denominator : ℕ) (numerator : ι → ℕ) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (permutation : Equiv.Perm (ι × Fin denominator)) : ι

The rational permutation output construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.ClassicalInformation.rationalPermutationOutput_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (numerator : ι → ℕ) (normalized : ∑ i : ι, numerator i = denominator) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (letter : ι) : (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ι × Fin denominator)) => rationalPermutationOutput denominator numerator nonempty permutation = letter) = ↑(numerator letter) / ↑denominator

theorem QuantumParallelRepetition.ClassicalInformation.rationalMarked_inter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (left right : ι → ℕ) : ClassicalSampling.rationalMarked denominator left ∩ ClassicalSampling.rationalMarked denominator right = ClassicalSampling.rationalMarked denominator fun (i : ι) => min (left i) (right i)

theorem QuantumParallelRepetition.ClassicalInformation.rationalMarked_inter_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) : (ClassicalSampling.rationalMarked denominator left ∩ ClassicalSampling.rationalMarked denominator right).card = ∑ i : ι, min (left i) (right i)

theorem QuantumParallelRepetition.ClassicalInformation.uniformPermutationProbability_mono {α : Type u_2} [Fintype α] [DecidableEq α] (small large : Equiv.Perm α → Prop) (hinclusion : ∀ (permutation : Equiv.Perm α), small permutation → large permutation) : ClassicalSampling.uniformPermutationProbability small ≤ ClassicalSampling.uniformPermutationProbability large

theorem QuantumParallelRepetition.ClassicalInformation.rationalPermutationOutput_disagreement_le_two_mul_finiteTotalVariation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (positive : 0 < denominator) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (hright : ∑ i : ι, right i = denominator) (nonempty_left : (ClassicalSampling.rationalMarked denominator left).Nonempty) (nonempty_right : (ClassicalSampling.rationalMarked denominator right).Nonempty) : (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ι × Fin denominator)) => rationalPermutationOutput denominator left nonempty_left permutation ≠ rationalPermutationOutput denominator right nonempty_right permutation) ≤ 2 * Pinsker.finiteTotalVariation (fun (i : ι) => ↑(left i) / ↑denominator) fun (i : ι) => ↑(right i) / ↑denominator

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

The DSV uniform left density schmidt coefficient construction used in the quantum parallel- repetition argument.

Equations

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

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

The DSV uniform left density spectral atom discrepancy construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformLeftDensitySpectralAtomDiscrepancy_le {d : ℕ} (ξ ζ : BipartiteUnitVector d) : dSVUniformLeftDensitySpectralAtomDiscrepancy ξ ζ ≤ 2 * √2 * ‖↑ξ - ↑ζ‖

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdGrid (N : ℕ) (k : Fin N) : ℝ

The DSV uniform density threshold grid construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdGrid N k = QuantumParallelRepetition.finiteUniformThresholdGrid✝ (1 / ↑N) (1 + 1 / ↑N) N k

theorem QuantumParallelRepetition.dSVUniformDensityThresholdGrid_apply {N : ℕ} (positive : 0 < N) (k : Fin N) : dSVUniformDensityThresholdGrid N k = (↑↑k + 1) / ↑N

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdWeight (N : ℕ) (_k : Fin N) : ℝ

The probability weight for DSV uniform density threshold.

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdWeight N _k = 1 / ↑N

theorem QuantumParallelRepetition.dSVUniformDensityThresholdWeight_nonneg (N : ℕ) (k : Fin N) : 0 ≤ dSVUniformDensityThresholdWeight N k

noncomputable def QuantumParallelRepetition.dSVUniformDensityGridPrefix (N : ℕ) (density : ℝ) : ℝ

The DSV uniform density grid prefix construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityGridPrefix_eq_count (N : ℕ) (density : ℝ) : dSVUniformDensityGridPrefix N density = ↑{k : Fin N | dSVUniformDensityThresholdGrid N k ≤ density}.card / ↑N

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdMismatch (N : ℕ) (alice bob : ℝ) : ℝ

The DSV uniform density threshold mismatch construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityThresholdMismatch_indicator_le_crossing {N : ℕ} (k : Fin N) (alice bob : ℝ) : (if dSVUniformDensityThresholdGrid N k ≤ alice ↔ dSVUniformDensityThresholdGrid N k ≤ bob then 0 else 1) ≤ if min alice bob ≤ dSVUniformDensityThresholdGrid N k ∧ dSVUniformDensityThresholdGrid N k ≤ max alice bob then 1 else 0

theorem QuantumParallelRepetition.dSVUniformDensityThresholdMismatch_le {N : ℕ} (positive : 0 < N) (alice bob : ℝ) : dSVUniformDensityThresholdMismatch N alice bob ≤ |alice - bob| + 1 / ↑N

theorem QuantumParallelRepetition.dSVUniformDensityThresholdGrid_count_eq_floor {N : ℕ} (positive : 0 < N) (density : ℝ) (nonnegative : 0 ≤ density) (bounded : density ≤ 1) : {k : Fin N | dSVUniformDensityThresholdGrid N k ≤ density}.card = ⌊density * ↑N⌋₊

theorem QuantumParallelRepetition.dSVUniformDensityBinarySpectral_false_eq_complement {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (bin : d → Bool) : (spectralPartitionPOVM F hF bin).effect false = 1 - (spectralPartitionPOVM F hF bin).effect true

theorem QuantumParallelRepetition.dSVUniformDensitySchmidtVector_sub {d : ℕ} (σ τ : Fin d → ℝ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : schmidtVector σ U V - schmidtVector τ U V = schmidtVector (fun (i : Fin d) => σ i - τ i) U V

theorem QuantumParallelRepetition.dSVUniformDensity_normalize_sub_self_norm {d : ℕ} (v : EuclideanSpace ℂ (Fin d × Fin d)) (nonzero : v ≠ 0) : ‖NormedSpace.normalize v - v‖ = |1 - ‖v‖|

noncomputable def QuantumParallelRepetition.normalizeOrDefault {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (fallback z : E) : E

The normalize or default construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.normalizeOrDefault fallback z = if z = 0 then fallback else NormedSpace.normalize z

theorem QuantumParallelRepetition.normalizeOrDefault_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (fallback z : E) (hfallback : ‖fallback‖ = 1) : ‖normalizeOrDefault fallback z‖ = 1

theorem QuantumParallelRepetition.normalizeOrDefault_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (fallback u v : E) (hfallback : ‖fallback‖ = 1) (hu : u ≠ 0) : ‖normalizeOrDefault fallback u - normalizeOrDefault fallback v‖ ≤ 2 * ‖u - v‖ / ‖u‖

noncomputable def QuantumParallelRepetition.dSVCanonicalFailureUnitRankFamily (d : ℕ) (positive : 0 < d) (rank : Fin (d + 1)) : BipartiteUnitVector d

The DSV canonical failure unit rank family construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_eq_zero_of_rank_zero {d : ℕ} (rank : Fin (d + 1)) (zero : ↑rank = 0) : dSVCanonicalFailurePrefix rank = 0

theorem QuantumParallelRepetition.dSVCanonicalFailurePrefix_norm_eq_sqrt {d : ℕ} (rank : Fin (d + 1)) : ‖dSVCanonicalFailurePrefix rank‖ = √↑↑rank

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdLeftBobBasis {d : ℕ} (ζ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (Fin d) ℂ)

The DSV uniform density threshold left bob basis construction used in the quantum parallel- repetition argument.

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdLeftBobBasis ζ = ⋯.eigenvectorUnitary

theorem QuantumParallelRepetition.exists_proofDSVUniformDensityPolarLeftCanonicalSchmidt {d : ℕ} (ξ : BipartiteUnitVector d) : ∃ (A : ↥(Matrix.unitaryGroup (Fin d) ℂ)), ↑ξ = schmidtVector (dSVUniformLeftDensitySchmidtCoefficient ξ) A (dSVUniformDensityThresholdLeftBobBasis ξ)

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

The unitary operator implementing controlled finite tensor local.

Equations

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

theorem QuantumParallelRepetition.controlledFiniteTensorLocalUnitary_apply {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} [Fintype Ω] [DecidableEq Ω] [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (U : Ω → ι → ↥(Matrix.unitaryGroup β ℂ)) (ω ν : Ω) (q r : ι → β) : ↑(controlledFiniteTensorLocalUnitary U) ⟨ω, q⟩ ⟨ν, r⟩ = if ω = ν then ∏ i : ι, ↑(U ω i) (q i) (r i) else 0

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryLocalIndex (N d L : ℕ) : Type

The type used to represent DSV uniform density threshold whole history local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryLocalIndex N d L = ((_ : Fin (L + 1)) × (Fin (L + 1) → QuantumParallelRepetition.DSVUniformDensityThresholdLocalIndex N d))

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryCatalystIndex (N d L : ℕ) : Type

The type used to represent DSV uniform density threshold whole history catalyst index in the exact sampling construction.

Equations

• QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryCatalystIndex N d L = (Fin N × Fin (L + 1) × (Fin L → QuantumParallelRepetition.DSVUniformDensityThresholdLocalIndex N d))

noncomputable def QuantumParallelRepetition.dSVUniformDensityThresholdWholeHistorySharedState (N d L : ℕ) : EuclideanSpace ℂ (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

The quantum state representing DSV uniform density threshold whole history shared.

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdWholeHistorySharedState N d L = QuantumParallelRepetition.sharedThresholdResource fun (flag : Fin (L + 1)) => if ↑flag = 0 then 1 else 0

theorem QuantumParallelRepetition.dSVUniformDensityThresholdWholeHistorySharedState_norm {N d : ℕ} (grid : 0 < N) (dimension : 0 < d) (L : ℕ) : ‖dSVUniformDensityThresholdWholeHistorySharedState N d L‖ = 1

def QuantumParallelRepetition.dSVUniformDensityThresholdWholeHistoryTargetSplitEquiv (N d L : ℕ) : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L ≃ Fin d × DSVUniformDensityThresholdWholeHistoryCatalystIndex N d L

The finite equivalence encoding DSV uniform density threshold whole history target split.

Equations

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

noncomputable def QuantumParallelRepetition.dSVUniformDensityAliceHistorySpectralCopy {N d : ℕ} (ξ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)

The DSV uniform density alice history spectral copy construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.dSVUniformDensityBobHistoryCopyBasis {N d : ℕ} (ζ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)

The DSV uniform density bob history copy basis construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityCompletePureHistory_raw_norm (N d L : ℕ) : ‖sharedThresholdResourceRaw fun (flag : Fin (L + 1)) => if ↑flag = 0 then 1 else 0‖ = ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖ ^ (L + 1)

theorem QuantumParallelRepetition.dSVUniformDensityCompletePureHistory_zeroFlag_apply (N d L : ℕ) (flag other : Fin (L + 1)) (alice bob : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d) : (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (⟨flag, alice⟩, ⟨other, bob⟩) = if ↑flag = 0 ∧ ↑other = 0 then (dSVUniformDensityIndependentSharedState (L + 1) N d).ofLp (alice, bob) else 0

noncomputable def QuantumParallelRepetition.commonPurificationSubspace {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) : Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioi 0)))

The common purification subspace construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.commonPurificationSubspace F M positive hM = Submodule.span ℂ (Set.range (QuantumParallelRepetition.commonPurificationGenerator✝ F M positive hM))

theorem QuantumParallelRepetition.commonPurificationSubspace_finiteDimensional {ι : Type u_1} {d : Type u_2} [Finite ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) : FiniteDimensional ℂ ↥(commonPurificationSubspace F M positive hM)

noncomputable def QuantumParallelRepetition.spectralPurificationFilterEntryLp {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i j : d) : ↥(MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioi 0)))

The spectral purification filter entry lp construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.spectralPurificationFilterEntryLp F hF i j = MeasureTheory.MemLp.toLp (fun (s : ℝ) => QuantumParallelRepetition.spectralPurificationFilter F hF s i j) ⋯

theorem QuantumParallelRepetition.spectralPurificationFilterEntryLp_coeFn {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i j : d) : ↑↑(spectralPurificationFilterEntryLp F hF i j) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => spectralPurificationFilter F hF s i j

theorem QuantumParallelRepetition.ensemble_spectralPurificationFilterEntryLp_mem_common {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) (i j : d) : spectralPurificationFilterEntryLp (F a) ⋯ i j ∈ commonPurificationSubspace F M positive hM

theorem QuantumParallelRepetition.mean_spectralPurificationFilterEntryLp_mem_common {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (i j : d) : spectralPurificationFilterEntryLp M hM i j ∈ commonPurificationSubspace F M positive hM

noncomputable def QuantumParallelRepetition.ensemblePurificationSubspaceEntry {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) (i j : d) : ↥(commonPurificationSubspace F M positive hM)

The ensemble purification subspace entry construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.ensemblePurificationSubspaceEntry F M positive hM a i j = ⟨QuantumParallelRepetition.spectralPurificationFilterEntryLp (F a) ⋯ i j, ⋯⟩

noncomputable def QuantumParallelRepetition.commonPurificationOrthonormalBasis {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) : OrthonormalBasis (Fin (Module.finrank ℂ ↥(commonPurificationSubspace F M positive hM))) ℂ ↥(commonPurificationSubspace F M positive hM)

The common purification orthonormal basis construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.commonPurificationOrthonormalBasis F M positive hM = stdOrthonormalBasis ℂ ↥(QuantumParallelRepetition.commonPurificationSubspace F M positive hM)

noncomputable def QuantumParallelRepetition.finitePurificationMatrix {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) : Matrix (d × Fin (Module.finrank ℂ ↥(commonPurificationSubspace F M positive hM))) d ℂ

The matrix representation of finite purification.

Equations

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

noncomputable def QuantumParallelRepetition.meanFinitePurificationMatrix {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) : Matrix (d × Fin (Module.finrank ℂ ↥(commonPurificationSubspace F M positive hM))) d ℂ

The matrix representation of mean finite purification.

Equations

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

theorem QuantumParallelRepetition.finitePurificationMatrix_gram_apply {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) (i j : d) : ((finitePurificationMatrix F M positive hM a).conjTranspose * finitePurificationMatrix F M positive hM a) i j = ∑ r : d, inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i) (ensemblePurificationSubspaceEntry F M positive hM a r j)

theorem QuantumParallelRepetition.ensemblePurificationSubspaceEntry_inner_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) (r i j : d) : inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i) (ensemblePurificationSubspaceEntry F M positive hM a r j) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s r i) * spectralPurificationFilter (F a) ⋯ s r j

theorem QuantumParallelRepetition.finitePurificationMatrix_gram_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) : (finitePurificationMatrix F M positive hM a).conjTranspose * finitePurificationMatrix F M positive hM a = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s) * spectralPurificationFilter (F a) ⋯ s

theorem QuantumParallelRepetition.finitePurificationMatrix_gram {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) : (finitePurificationMatrix F M positive hM a).conjTranspose * finitePurificationMatrix F M positive hM a = F a

theorem QuantumParallelRepetition.finitePurificationMatrix_difference_gram_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a : ι) : (finitePurificationMatrix F M positive hM a - meanFinitePurificationMatrix F M positive hM).conjTranspose * (finitePurificationMatrix F M positive hM a - meanFinitePurificationMatrix F M positive hM) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter M hM s) * (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter M hM s)

theorem QuantumParallelRepetition.weighted_finitePurificationMatrix_difference_gram {ι : 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) : ∑ a : ι, weight a • ((finitePurificationMatrix F M positive hM a - meanFinitePurificationMatrix F M positive hM).conjTranspose * (finitePurificationMatrix F M positive hM a - meanFinitePurificationMatrix F M positive hM)) = ∫ (s : ℝ) in Set.Ioi 0, weightedSpectralFilterVariance weight F M positive hM s

theorem QuantumParallelRepetition.finite_purification_log_entropy_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 - ∑ i : ι, weight i • ((finitePurificationMatrix F M positive hM i - meanFinitePurificationMatrix F M positive hM).conjTranspose * (finitePurificationMatrix F M positive hM i - meanFinitePurificationMatrix F M positive hM))).PosSemidef

noncomputable def QuantumParallelRepetition.strategyPurificationVector {X : Type u_1} {Y : Type 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) : EuclideanSpace ℂ ((S.Alice × S.Alice × S.Bob) × S.Bob)

The state vector representing strategy purification.

Equations

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

theorem QuantumParallelRepetition.strategyPurificationVector_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) : ‖strategyPurificationVector S‖ = 1

theorem QuantumParallelRepetition.reindexedMatrixQuadratic {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq e] (φ : e ≃ d) (M : Matrix d d ℂ) (v : d → ℂ) : quadraticExpectation (Matrix.toEuclideanCLM (M.submatrix ⇑φ ⇑φ)) (WithLp.toLp 2 (v ∘ ⇑φ)) = (star v ⬝ᵥ M.mulVec v).re

def QuantumParallelRepetition.purificationAlicePOVM {ι : Type u_1} {d : Type u_2} {k : Type u_3} [Fintype ι] [Fintype d] [Fintype k] [DecidableEq d] [DecidableEq k] (P : POVM ι d) : POVM ι (d × k)

The positive operator-valued measurement implementing purification alice.

Equations

• QuantumParallelRepetition.purificationAlicePOVM P = { effect := fun (a : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) 1, positive := ⋯, complete := ⋯ }

theorem QuantumParallelRepetition.strategyPurificationVector_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (EA : Matrix S.Alice S.Alice ℂ) (EB : Matrix S.Bob S.Bob ℂ) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA 1) EB)) (strategyPurificationVector S) = (S.state.matrix * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA EB).trace.re

noncomputable def QuantumParallelRepetition.purifiedStrategy {X : Type u_1} {Y : Type 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) : Strategy G

The strategy implementing purified.

Equations

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

theorem QuantumParallelRepetition.purifiedStrategy_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) : (purifiedStrategy S).outcomeProbability x y a b = S.outcomeProbability x y a b

theorem QuantumParallelRepetition.purifiedStrategy_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) : (purifiedStrategy S).winProbability = S.winProbability

def QuantumParallelRepetition.finiteLocalPurificationJointMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : Matrix ((eA × S.Alice × S.Bob) × eB) ((S.Alice × S.Alice × S.Bob) × S.Bob) ℂ

The matrix representation of finite local purification joint.

Equations

• QuantumParallelRepetition.finiteLocalPurificationJointMatrix S KA KB = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) KA 1) KB

noncomputable def QuantumParallelRepetition.finiteLocalPurificationVector {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : EuclideanSpace ℂ ((eA × S.Alice × S.Bob) × eB)

The state vector representing finite local purification.

Equations

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

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

theorem QuantumParallelRepetition.finiteLocalPurificationVector_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : ‖finiteLocalPurificationVector S KA KB‖ ^ 2 = (S.state.matrix * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (KA.conjTranspose * KA) (KB.conjTranspose * KB)).trace.re

theorem QuantumParallelRepetition.dSVUniformDensityMixedProtocolLocalAction_norm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U V : ↥(Matrix.unitaryGroup ι ℂ)) (z : EuclideanSpace ℂ (ι × ι)) : ‖WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).mulVec z.ofLp)‖ = ‖z‖

def QuantumParallelRepetition.dSVUniformDensityPhysicalAsyncSigmaContinuation {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (U V : ι → ↥(Matrix.unitaryGroup κ ℂ)) (z : EuclideanSpace ℂ (((_ : ι) × κ) × (_ : ι) × κ)) : EuclideanSpace ℂ (((_ : ι) × κ) × (_ : ι) × κ)

The DSV uniform density physical async sigma continuation construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalAsyncSigmaContinuation_norm {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (U V : ι → ↥(Matrix.unitaryGroup κ ℂ)) (z : EuclideanSpace ℂ (((_ : ι) × κ) × (_ : ι) × κ)) : ‖dSVUniformDensityPhysicalAsyncSigmaContinuation U V z‖ = ‖z‖

theorem QuantumParallelRepetition.dSVUniformDensityFirstAcceptFinitePrefix {L : ℕ} (s : Finset (Fin L)) (j : Fin L) : (if h : s.Nonempty then (s.min' h).succ else 0) = j.succ ↔ j ∈ s ∧ ∀ i < j, i ∉ s

theorem QuantumParallelRepetition.dSVUniformDensityFirstAcceptControlledTensor_inv_apply {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} [Fintype Ω] [DecidableEq Ω] [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (U : Ω → ι → ↥(Matrix.unitaryGroup β ℂ)) (ω ν : Ω) (q r : ι → β) : ↑(controlledFiniteTensorLocalUnitary U)⁻¹ ⟨ω, q⟩ ⟨ν, r⟩ = if ω = ν then ∏ i : ι, star (↑(U ω i) (r i) (q i)) else 0

theorem QuantumParallelRepetition.coherentSharedRandomControlledUnitary_inv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (U : ι → ↥(Matrix.unitaryGroup κ ℂ)) : (coherentSharedRandomControlledUnitary U)⁻¹ = coherentSharedRandomControlledUnitary fun (i : ι) => (U i)⁻¹

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalAsync_doubleProductSum {ι : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype β] [Fintype γ] (f : ι → β → γ → ℝ) : ∑ x : ι → β, ∑ y : ι → γ, ∏ i : ι, f i (x i) (y i) = ∏ i : ι, ∑ a : β, ∑ b : γ, f i a b

theorem QuantumParallelRepetition.spectralPartitionPOVM_effect_eq_spectralDiagonal {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (F : Matrix ι ι ℂ) (positive : F.PosSemidef) (bin : ι → κ) (outcome : κ) : (spectralPartitionPOVM F positive bin).effect outcome = (spectralConjugationCLM ⋯.eigenvectorUnitary) (Matrix.diagonal fun (i : ι) => if bin i = outcome then 1 else 0)

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalSpectralAliceCopy_inv {N d : ℕ} (ξ : BipartiteUnitVector d) : (dSVUniformDensityAliceHistorySpectralCopy ξ)⁻¹ = coherentSharedRandomControlledUnitary fun (x : Fin N) => dSVUniformDensityThresholdLeftBobBasis ξ

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalSpectralAliceCopy_transpose {N d : ℕ} (ξ : BipartiteUnitVector d) : (↑(dSVUniformDensityAliceHistorySpectralCopy ξ)).transpose = ↑(dSVUniformDensityBobHistoryCopyBasis ξ)

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalSpectralAliceCopy_inv_transpose {N d : ℕ} (ξ : BipartiteUnitVector d) : (↑(dSVUniformDensityAliceHistorySpectralCopy ξ)⁻¹).transpose = ↑(dSVUniformDensityBobHistoryCopyBasis ξ)⁻¹

theorem QuantumParallelRepetition.dSVUniformDensityPhysicalMatched_doubleTensorSourceFactor {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] (A B : ι → Matrix β β ℂ) (source : β × β → ℂ) (a b : ι → β) : ∑ x : ι → β, ∑ y : ι → β, ((∏ i : ι, A i (a i) (x i)) * ∏ i : ι, B i (b i) (y i)) * ∏ i : ι, source (x i, y i) = ∏ i : ι, ∑ x : β, ∑ y : β, A i (a i) x * B i (b i) y * source (x, y)

def QuantumParallelRepetition.dSVUniformDensityCorrectedMatchedSigmaWeightedResidual {H : Type u_1} {n : ℕ} (history : EuclideanSpace ℂ (H × H)) (work : H → H → EuclideanSpace ℂ (Fin n × Fin n)) : EuclideanSpace ℂ (((_ : H) × Fin n) × (_ : H) × Fin n)

The DSV uniform density corrected matched sigma weighted residual construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensityCorrectedMatchedSigmaWeightedResidual_distance_sq {H : Type u_1} [Fintype H] {n : ℕ} (history : EuclideanSpace ℂ (H × H)) (work target : H → H → EuclideanSpace ℂ (Fin n × Fin n)) : ‖dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history work - dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history target‖ ^ 2 = ∑ a : H, ∑ b : H, ‖history.ofLp (a, b)‖ ^ 2 * ‖work a b - target a b‖ ^ 2

theorem QuantumParallelRepetition.dSVUniformDensityCorrectedMatchedSigmaWeightedResidual_controlled {H : Type u_1} [Fintype H] [DecidableEq H] {n : ℕ} (history : EuclideanSpace ℂ (H × H)) (work : H → H → EuclideanSpace ℂ (Fin n × Fin n)) (U V : H → ↥(Matrix.unitaryGroup (Fin n) ℂ)) : dSVUniformDensityPhysicalAsyncSigmaContinuation U V (dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history work) = dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history fun (a b : H) => localUnitaryAction (U a) (V b) (work a b)

theorem QuantumParallelRepetition.dSVUniformDensityCorrectedMatchedSigmaControlledReset_distance_sq {H : Type u_1} [Fintype H] [DecidableEq H] {n : ℕ} (history : EuclideanSpace ℂ (H × H)) (work target : H → H → EuclideanSpace ℂ (Fin n × Fin n)) (U V : H → ↥(Matrix.unitaryGroup (Fin n) ℂ)) : ‖dSVUniformDensityPhysicalAsyncSigmaContinuation U V (dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history work) - dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history target‖ ^ 2 = ∑ a : H, ∑ b : H, ‖history.ofLp (a, b)‖ ^ 2 * ‖localUnitaryAction (U a) (V b) (work a b) - target a b‖ ^ 2

noncomputable def QuantumParallelRepetition.dSVDensityRationalProjectiveThresholdBin (w : ℝ) (N : ℕ) (k : Fin N) (a : ℝ) : Bool

The DSV density rational projective threshold bin construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalProjectiveThresholdPOVM {ι : Type u_1} [Fintype ι] [DecidableEq ι] (w : ℝ) (N : ℕ) (k : Fin N) (F : Matrix ι ι ℂ) (positive : F.PosSemidef) : POVM Bool ι

The positive operator-valued measurement implementing DSV density rational projective threshold.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalProjectiveThresholdPOVM_projective {ι : Type u_1} [Fintype ι] [DecidableEq ι] (w : ℝ) (N : ℕ) (k : Fin N) (F : Matrix ι ι ℂ) (positive : F.PosSemidef) (outcome : Bool) : (dSVDensityRationalProjectiveThresholdPOVM w N k F positive).effect outcome * (dSVDensityRationalProjectiveThresholdPOVM w N k F positive).effect outcome = (dSVDensityRationalProjectiveThresholdPOVM w N k F positive).effect outcome

noncomputable def QuantumParallelRepetition.dSVDensityRationalLeftProjectiveThresholdPOVM {d : ℕ} (w : ℝ) (N : ℕ) (k : Fin N) (ξ : BipartiteUnitVector d) : POVM Bool (Fin d)

The positive operator-valued measurement implementing DSV density rational left projective threshold.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalLeftProjectiveThresholdAtomMismatch {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : ℝ

The DSV density rational left projective threshold atom mismatch construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalLeftProjectiveThresholdAtomMismatch_le_discrepancy {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ ≤ dSVUniformLeftDensitySpectralAtomDiscrepancy ξ ζ / w + ↑d / ↑N

theorem QuantumParallelRepetition.dSVUniformDensityGridPrefix_le_density {N : ℕ} (positive : 0 < N) {a : ℝ} (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : dSVUniformDensityGridPrefix N a ≤ a

theorem QuantumParallelRepetition.dSVUniformDensityGridPrefix_density_sub_lt {N : ℕ} (positive : 0 < N) {a : ℝ} (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a - dSVUniformDensityGridPrefix N a < 1 / ↑N

theorem QuantumParallelRepetition.dSVUniformDensityGridPrefix_density_sub_le {N : ℕ} (positive : 0 < N) {a : ℝ} (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a - 1 / ↑N ≤ dSVUniformDensityGridPrefix N a

noncomputable def QuantumParallelRepetition.dSVDensityRationalLeftProjectiveDiagonalMass {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : ℝ

The total probability mass of DSV density rational left projective diagonal.

Equations

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

theorem QuantumParallelRepetition.dSVSoftBobLeftReducedDensity_eigenvalue_le_one {d : ℕ} (ξ : BipartiteUnitVector d) (i : Fin d) : ⋯.eigenvalues i ≤ 1

theorem QuantumParallelRepetition.dSVRationalSoftPass_ge_density_div_width_add_one {w a : ℝ} (width : 0 < w) (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a / (w + 1) ≤ dSVRationalSoftPass w a

theorem QuantumParallelRepetition.dSVDensityRationalLeftProjectiveDiagonalMass_lower {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) : 1 / (w + 1) - ↑d / ↑N ≤ dSVDensityRationalLeftProjectiveDiagonalMass w N ξ