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)

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

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

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

Equations

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

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

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

Equations

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

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

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)

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

Equations

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

noncomputable def QuantumParallelRepetition.dSVUniformDensityIndependentHistoryPairReindex (L N d : ℕ) : EuclideanSpace ℂ (Fin L → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (DSVUniformDensityIndependentHistoryLocalIndex L N d × DSVUniformDensityIndependentHistoryLocalIndex L N d)

Equations

• QuantumParallelRepetition.dSVUniformDensityIndependentHistoryPairReindex L N d = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ QuantumParallelRepetition.bilateralWorkPairEquiv.symm

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

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

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

Equations

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

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

Equations

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

theorem QuantumParallelRepetition.dSVUniformDensitySchmidtSumMass_le_four {d : ℕ} (ξ ζ : BipartiteUnitVector d) : dSVUniformDensitySchmidtSumMass ξ ζ ≤ 4

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

def QuantumParallelRepetition.ClassicalSampling.markedFirst {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : α

Equations

• QuantumParallelRepetition.ClassicalSampling.markedFirst rank marked nonempty permutation = (Equiv.symm permutation) (rank.symm ((Finset.image (fun (a : α) => rank (permutation a)) marked).min' ⋯))

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_mem {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank marked nonempty permutation ∈ marked

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_rank {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : rank (permutation (markedFirst rank marked nonempty permutation)) = (Finset.image (fun (a : α) => rank (permutation a)) marked).min' ⋯

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_rank_le {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) {a : α} (ha : a ∈ marked) : rank (permutation (markedFirst rank marked nonempty permutation)) ≤ rank (permutation a)

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_eq_of_mem_of_rank_le {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) {a : α} (ha : a ∈ marked) (hle : ∀ b ∈ marked, rank (permutation a) ≤ rank (permutation b)) : markedFirst rank marked nonempty permutation = a

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_subset_eq_of_mem {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) {small large : Finset α} (hsmall : small.Nonempty) (hlarge : large.Nonempty) (permutation : Equiv.Perm α) (hsub : small ⊆ large) (hmem : markedFirst rank large hlarge permutation ∈ small) : markedFirst rank small hsmall permutation = markedFirst rank large hlarge permutation

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_eq_iff_union_first_mem_inter {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank left hleft permutation = markedFirst rank right hright permutation ↔ markedFirst rank (left ∪ right) ⋯ permutation ∈ left ∩ right

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_ne_iff_union_first_mem_symmDiff {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation ↔ markedFirst rank (left ∪ right) ⋯ permutation ∈ left \ right ∪ right \ left

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

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_swap_trans {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) (permutation : Equiv.Perm α) : markedFirst rank marked nonempty (Equiv.trans (Equiv.swap x y) permutation) = (Equiv.swap x y) (markedFirst rank marked nonempty permutation)

def QuantumParallelRepetition.ClassicalSampling.firstFiber {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (a : α) : Finset (Equiv.Perm α)

Equations

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

theorem QuantumParallelRepetition.ClassicalSampling.firstFiber_card_eq {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) : (firstFiber rank marked nonempty x).card = (firstFiber rank marked nonempty y).card

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_event_card_mul {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (event : Finset α) (hevent : event ⊆ marked) : {permutation : Equiv.Perm α | markedFirst rank marked nonempty permutation ∈ event}.card * marked.card = event.card * Fintype.card (Equiv.Perm α)

theorem QuantumParallelRepetition.ClassicalSampling.sharedPermutation_disagreement_card_mul {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : {permutation : Equiv.Perm α | markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation}.card * (left ∪ right).card = (left \ right ∪ right \ left).card * Fintype.card (Equiv.Perm α)

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

Equations

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

theorem QuantumParallelRepetition.ClassicalSampling.markedFirst_event_probability {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (event : Finset α) (hevent : event ⊆ marked) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank marked nonempty permutation ∈ event) = ↑event.card / ↑marked.card

theorem QuantumParallelRepetition.ClassicalSampling.sharedPermutation_disagreement_probability {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) = ↑(left \ right ∪ right \ left).card / ↑(left ∪ right).card

theorem QuantumParallelRepetition.ClassicalSampling.sharedPermutation_disagreement_probability_le {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) ≤ ↑(left \ right ∪ right \ left).card / ↑left.card

noncomputable def QuantumParallelRepetition.ClassicalSampling.markedTotalVariation {α : Type u_1} [DecidableEq α] (left right : Finset α) : ℝ

Equations

• QuantumParallelRepetition.ClassicalSampling.markedTotalVariation left right = ↑(left \ right ∪ right \ left).card / (2 * ↑left.card)

theorem QuantumParallelRepetition.ClassicalSampling.sharedPermutation_disagreement_probability_le_two_mul_tv {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (_equal_card : left.card = right.card) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) ≤ 2 * markedTotalVariation left right

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

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 β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) : (rationalMarked denominator numerator).card = denominator

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

theorem QuantumParallelRepetition.ClassicalSampling.rationalMarked_letter_probability {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (nonempty : (rationalMarked denominator numerator).Nonempty) (rank : β × Fin denominator ≃ Fin (Fintype.card (β × Fin denominator))) (letter : β) : (uniformPermutationProbability fun (permutation : Equiv.Perm (β × Fin denominator)) => (markedFirst rank (rationalMarked denominator numerator) nonempty permutation).1 = letter) = ↑(numerator letter) / ↑denominator

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)

noncomputable def QuantumParallelRepetition.Pinsker.pinskerScalarGap (x : ℝ) : ℝ

Equations

• QuantumParallelRepetition.Pinsker.pinskerScalarGap x = InformationTheory.klFun x - 3 * (x - 1) ^ 2 / (2 * (x + 2))

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

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.pinskerScalarGap_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ pinskerScalarGap x

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

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

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

Equations

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

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

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

Equations

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

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

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

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.distributionFloorProbability_le {ι : Type u_1} (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (i : ι) : distributionFloorProbability denominator p i ≤ p i

theorem QuantumParallelRepetition.ClassicalInformation.distributionFloorProbability_error_lt {ι : Type u_1} (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (i : ι) : p i - distributionFloorProbability denominator p i < 1 / ↑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.distributionFloorResidual_probability_eq_sum {ι : Type u_1} [Fintype ι] (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ↑(distributionFloorResidual denominator p) / ↑denominator = ∑ i : ι, (p i - distributionFloorProbability denominator p i)

theorem QuantumParallelRepetition.ClassicalInformation.distributionRoundedProbability_eq_floor_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) (i : ι) : distributionRoundedProbability base denominator p i = distributionFloorProbability denominator p i + if i = base then ↑(distributionFloorResidual denominator p) / ↑denominator else 0

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

Equations

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

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 : ι × κ → ℝ) : ι → ℝ

Equations

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

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

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

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) (_hright : ∑ i : ι, right i = denominator) : (ClassicalSampling.rationalMarked denominator left ∩ ClassicalSampling.rationalMarked denominator right).card = ∑ i : ι, min (left i) (right i)

theorem QuantumParallelRepetition.ClassicalInformation.rationalMarked_markedTotalVariation_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (positive : 0 < denominator) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (hright : ∑ i : ι, right i = denominator) : ClassicalSampling.markedTotalVariation (ClassicalSampling.rationalMarked denominator left) (ClassicalSampling.rationalMarked denominator right) = Pinsker.finiteTotalVariation (fun (i : ι) => ↑(left i) / ↑denominator) fun (i : ι) => ↑(right i) / ↑denominator

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_tv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (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 * ClassicalSampling.markedTotalVariation (ClassicalSampling.rationalMarked denominator left) (ClassicalSampling.rationalMarked denominator right)

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

def QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwapVector {d : ℕ} (z : EuclideanSpace ℂ (Fin d × Fin d)) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

• QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwapVector z = WithLp.toLp 2 fun (ij : Fin d × Fin d) => star (z.ofLp (ij.2, ij.1))

theorem QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwapVector_norm {d : ℕ} (z : EuclideanSpace ℂ (Fin d × Fin d)) : ‖dSVUniformLeftDensityConjugateSwapVector z‖ = ‖z‖

theorem QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwapVector_distance {d : ℕ} (z w : EuclideanSpace ℂ (Fin d × Fin d)) : ‖dSVUniformLeftDensityConjugateSwapVector z - dSVUniformLeftDensityConjugateSwapVector w‖ = ‖z - w‖

def QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwap {d : ℕ} (ξ : BipartiteUnitVector d) : BipartiteUnitVector d

Equations

• QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwap ξ = ⟨QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwapVector ↑ξ, ⋯⟩

theorem QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwap_coefficient {d : ℕ} (ξ : BipartiteUnitVector d) : targetCoefficientMatrix (dSVUniformLeftDensityConjugateSwap ξ) = (targetCoefficientMatrix ξ).conjTranspose

theorem QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwap_density {d : ℕ} (ξ : BipartiteUnitVector d) : targetReducedDensity (dSVUniformLeftDensityConjugateSwap ξ) = dSVSoftBobLeftReducedDensity ξ

theorem QuantumParallelRepetition.dSVUniformLeftDensityConjugateSwap_distance {d : ℕ} (ξ ζ : BipartiteUnitVector d) : ‖↑(dSVUniformLeftDensityConjugateSwap ξ) - ↑(dSVUniformLeftDensityConjugateSwap ζ)‖ = ‖↑ξ - ↑ζ‖

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

Equations

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

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

Equations

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

theorem QuantumParallelRepetition.dSVUniformLeftDensitySpectralAtomDiscrepancy_eq_swap {d : ℕ} (ξ ζ : BipartiteUnitVector d) : dSVUniformLeftDensitySpectralAtomDiscrepancy ξ ζ = dSVUniformDensitySpectralAtomDiscrepancy (dSVUniformLeftDensityConjugateSwap ξ) (dSVUniformLeftDensityConjugateSwap ζ)

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

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

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

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

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

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

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

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

Equations

• QuantumParallelRepetition.dSVUniformDensityThresholdLeftBobBasis ζ = ⋯.eigenvectorUnitary

def QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap {d : ℕ} (v : EuclideanSpace ℂ (Fin d × Fin d)) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

• QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap v = WithLp.toLp 2 fun (q : Fin d × Fin d) => star (v.ofLp (q.2, q.1))

theorem QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap_norm {d : ℕ} (v : EuclideanSpace ℂ (Fin d × Fin d)) : ‖dSVUniformDensityPolarConjugateSwap v‖ = ‖v‖

def QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwapTarget {d : ℕ} (ξ : BipartiteUnitVector d) : BipartiteUnitVector d

Equations

• QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwapTarget ξ = ⟨QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap ↑ξ, ⋯⟩

theorem QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap_coefficient {d : ℕ} (ξ : BipartiteUnitVector d) : targetCoefficientMatrix (dSVUniformDensityPolarConjugateSwapTarget ξ) = (targetCoefficientMatrix ξ).conjTranspose

theorem QuantumParallelRepetition.dSVUniformDensityPolarConjugateSwap_reducedDensity {d : ℕ} (ξ : BipartiteUnitVector d) : targetReducedDensity (dSVUniformDensityPolarConjugateSwapTarget ξ) = dSVSoftBobLeftReducedDensity ξ

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

Equations

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

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

def QuantumParallelRepetition.finiteTensorLocalUnitaryMatrix {ι : Type u_1} {β : Type u_2} [Fintype ι] [Fintype β] [DecidableEq β] (U : ι → ↥(Matrix.unitaryGroup β ℂ)) : Matrix (ι → β) (ι → β) ℂ

Equations

• QuantumParallelRepetition.finiteTensorLocalUnitaryMatrix U q r = ∏ i : ι, ↑(U i) (q i) (r i)

theorem QuantumParallelRepetition.finiteTensorLocalUnitaryMatrix_gram {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (U : ι → ↥(Matrix.unitaryGroup β ℂ)) : (finiteTensorLocalUnitaryMatrix U).conjTranspose * finiteTensorLocalUnitaryMatrix U = 1

def QuantumParallelRepetition.finiteTensorLocalUnitary {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] (U : ι → ↥(Matrix.unitaryGroup β ℂ)) : ↥(Matrix.unitaryGroup (ι → β) ℂ)

Equations

• QuantumParallelRepetition.finiteTensorLocalUnitary U = ⟨QuantumParallelRepetition.finiteTensorLocalUnitaryMatrix U, ⋯⟩

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

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

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

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)

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

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

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

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.scalarPurificationLp (z : ℝ) (hz : 0 ≤ z) : ↥(MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioi 0)))

Equations

• QuantumParallelRepetition.scalarPurificationLp z hz = MeasureTheory.MemLp.toLp (fun (s : ℝ) => ↑(z / (z + s))) ⋯

theorem QuantumParallelRepetition.scalarPurificationLp_coeFn (z : ℝ) (hz : 0 ≤ z) : ↑↑(scalarPurificationLp z hz) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => ↑(z / (z + s))

noncomputable def QuantumParallelRepetition.commonPurificationGenerator {ι : 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) : ι × d ⊕ d → ↥(MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioi 0)))

Equations

• QuantumParallelRepetition.commonPurificationGenerator F M positive hM (Sum.inl (i, k)) = QuantumParallelRepetition.scalarPurificationLp (⋯.eigenvalues k) ⋯
• QuantumParallelRepetition.commonPurificationGenerator F M positive hM (Sum.inr k) = QuantumParallelRepetition.scalarPurificationLp (⋯.eigenvalues k) ⋯

noncomputable def QuantumParallelRepetition.commonPurificationSubspace {ι : 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) : Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioi 0)))

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

theorem QuantumParallelRepetition.ensemble_scalarPurificationLp_mem_common {ι : 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) (i : ι) (k : d) : scalarPurificationLp (⋯.eigenvalues k) ⋯ ∈ commonPurificationSubspace F M positive hM

theorem QuantumParallelRepetition.mean_scalarPurificationLp_mem_common {ι : 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) (k : d) : scalarPurificationLp (⋯.eigenvalues k) ⋯ ∈ 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)))

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.spectralPurificationFilterEntryLp_eq_eigen_sum {d : Type u_1} [Fintype d] [DecidableEq d] (F : Matrix d d ℂ) (hF : F.PosSemidef) (i j : d) : spectralPurificationFilterEntryLp F hF i j = ∑ k : d, (↑⋯.eigenvectorUnitary i k * star (↑⋯.eigenvectorUnitary) k j) • scalarPurificationLp (⋯.eigenvalues k) ⋯

theorem QuantumParallelRepetition.ensemble_spectralPurificationFilterEntryLp_mem_common {ι : 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) : spectralPurificationFilterEntryLp (F a) ⋯ i j ∈ commonPurificationSubspace F M positive hM

theorem QuantumParallelRepetition.mean_spectralPurificationFilterEntryLp_mem_common {ι : 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) (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 ι] [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)

Equations

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

noncomputable def QuantumParallelRepetition.meanPurificationSubspaceEntry {ι : 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) (i j : d) : ↥(commonPurificationSubspace F M positive hM)

Equations

• QuantumParallelRepetition.meanPurificationSubspaceEntry F M positive hM i j = ⟨QuantumParallelRepetition.spectralPurificationFilterEntryLp M hM 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)

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 ℂ

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 ℂ

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 ι] [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_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 - meanFinitePurificationMatrix F M positive hM).conjTranspose * (finitePurificationMatrix F M positive hM a - meanFinitePurificationMatrix F M positive hM)) i j = ∑ r : d, inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - meanPurificationSubspaceEntry F M positive hM r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - meanPurificationSubspaceEntry F M positive hM r j)

theorem QuantumParallelRepetition.purificationSubspaceEntry_difference_inner_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 : ι) (r i j : d) : inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - meanPurificationSubspaceEntry F M positive hM r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - meanPurificationSubspaceEntry F M positive hM r j) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s r i - spectralPurificationFilter M hM s r i) * (spectralPurificationFilter (F a) ⋯ s r j - spectralPurificationFilter M hM s r j)

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

def QuantumParallelRepetition.matrixPurificationVector {d : Type u_1} [Fintype d] (K : Matrix d d ℂ) : EuclideanSpace ℂ (d × d)

Equations

• QuantumParallelRepetition.matrixPurificationVector K = WithLp.toLp 2 K.vec

theorem QuantumParallelRepetition.matrixPurificationVector_norm_sq {d : Type u_1} [Fintype d] (K : Matrix d d ℂ) : ‖matrixPurificationVector K‖ ^ 2 = (K.conjTranspose * K).trace.re

def QuantumParallelRepetition.strategyPurificationShuffle (dA dB : Type) : (dA × dA × dB) × dB ≃ (dA × dB) × dA × dB

Equations

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

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)

Equations

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

theorem QuantumParallelRepetition.strategyPurificationVector_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) : ‖strategyPurificationVector S‖ ^ 2 = ‖matrixPurificationVector (spectralSupportSqrt S.state.matrix ⋯)‖ ^ 2

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

Equations

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

theorem QuantumParallelRepetition.purificationJointEffect_submatrix {dA dB : Type} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (A : Matrix dA dA ℂ) (B : Matrix dB dB ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1) B = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)).submatrix ⇑(strategyPurificationShuffle dA dB) ⇑(strategyPurificationShuffle dA dB)

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

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

theorem QuantumParallelRepetition.rectangular_matrix_mulVec_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.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] [Fintype eA] [Fintype eB] {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) ℂ

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] [Fintype eA] [Fintype eB] {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)

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 ℂ (((_ : ι) × κ) × (_ : ι) × κ)

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 β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (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 β] [DecidableEq β] (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} [Fintype H] {n : ℕ} (history : EuclideanSpace ℂ (H × H)) (work : H → H → EuclideanSpace ℂ (Fin n × Fin n)) : EuclideanSpace ℂ (((_ : H) × Fin n) × (_ : H) × Fin n)

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

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 ι

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)

Equations

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

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

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

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 ξ

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalProjector {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (k : Fin N) : Matrix (Fin d) (Fin d) ℂ

Equations

• QuantumParallelRepetition.dSVDensityRationalPhysicalProjector w ξ k = (QuantumParallelRepetition.dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect true

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjector_pos {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (k : Fin N) : (dSVDensityRationalPhysicalProjector w ξ k).PosSemidef

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjector_projective {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (k : Fin N) : dSVDensityRationalPhysicalProjector w ξ k * dSVDensityRationalPhysicalProjector w ξ k = dSVDensityRationalPhysicalProjector w ξ k

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjector_complement_pos {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (k : Fin N) : (1 - dSVDensityRationalPhysicalProjector w ξ k).PosSemidef

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalGlobalPOVM {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) : POVM Bool (DSVUniformDensityThresholdLocalIndex N d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjectorSquare_eq_atomMismatch {d N : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) (k : Fin N) : ((dSVDensityRationalPhysicalProjector w ξ k - dSVDensityRationalPhysicalProjector w ζ k) * (dSVDensityRationalPhysicalProjector w ξ k - dSVDensityRationalPhysicalProjector w ζ k)).trace.re = ∑ i : Fin d, ∑ j : Fin d, if dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues j) then 0 else spectralAtomOverlap (dSVSoftBobLeftReducedDensity ξ) (dSVSoftBobLeftReducedDensity ζ) ⋯ ⋯ i j

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjectorSquare_grid_eq {d N : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) : (∑ k : Fin N, ((dSVDensityRationalPhysicalProjector w ξ k - dSVDensityRationalPhysicalProjector w ζ k) * (dSVDensityRationalPhysicalProjector w ξ k - dSVDensityRationalPhysicalProjector w ζ k)).trace.re) / ↑N = dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjector_weighted_rank_eq {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) : ∑ k : Fin N, dSVUniformDensityThresholdWeight N k * (dSVDensityRationalPhysicalProjector w ξ k).trace.re = dSVDensityRationalLeftProjectiveDiagonalMass w N ξ

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalDiagonalBornSuccess {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ : BipartiteUnitVector d) : ℝ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalDiagonalBornSuccess_eq {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ : BipartiteUnitVector d) : dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ = dSVDensityRationalLeftProjectiveDiagonalMass w N ξ / ↑d

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalProjectorCrossHazard_eq {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ = dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / ↑d

noncomputable def QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdProjector {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (k : Fin N) : Matrix (Fin d) (Fin d) ℂ

Equations

• QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdProjector w N ξ k = (QuantumParallelRepetition.dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect true

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdProjector_pos {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (k : Fin N) : (dSVDensityRationalCompleteProjectiveThresholdProjector w N ξ k).PosSemidef

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdEffect_projective {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (k : Fin N) (a : Bool) : (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a * (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a = (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdEffect_false {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (k : Fin N) : (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect false = 1 - dSVDensityRationalCompleteProjectiveThresholdProjector w N ξ k

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveThresholdProjector_complement_pos {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (k : Fin N) : (1 - dSVDensityRationalCompleteProjectiveThresholdProjector w N ξ k).PosSemidef

noncomputable def QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveBinaryPOVM {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : POVM Bool (DSVUniformDensityThresholdLocalIndex N d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveBinaryPOVM_effect {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (a : Bool) : (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect a = Matrix.blockDiagonal' fun (k : Fin N) => (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveBinaryPOVM_projective {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (a : Bool) : (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect a * (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect a = (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect a

noncomputable def QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome_eq_block_action {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) : dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ a b = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.blockDiagonal' fun (k : Fin N) => (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a) (Matrix.blockDiagonal' fun (k : Fin N) => (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ζ).effect b).transpose).mulVec (dSVUniformDensityThresholdSharedState N d).ofLp)

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome_eq_blockVector {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) : dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ a b = ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ • WithLp.toLp 2 (Matrix.blockDiagonal' fun (k : Fin N) => (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a * (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ζ).effect b).transpose.vec

theorem QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome_norm_sq_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) : ‖dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ a b‖ ^ 2 = (∑ k : Fin N, ((dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a * (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ζ).effect b).trace.re) / (↑d * ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalGridPrefix_nonneg (N : ℕ) (a : ℝ) : 0 ≤ dSVUniformDensityGridPrefix N a

theorem QuantumParallelRepetition.dSVDensityRationalSoftPass_rescaled_le_density {w a : ℝ} (width : 0 < w) (nonnegative : 0 ≤ a) : w * dSVRationalSoftPass w a ≤ a

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

theorem QuantumParallelRepetition.dSVDensityRationalGrid_rescaled_le_density {N : ℕ} {w a : ℝ} (width : 0 < w) (grid : 0 < N) (nonnegative : 0 ≤ a) : w * dSVUniformDensityGridPrefix N (dSVRationalSoftPass w a) ≤ a

theorem QuantumParallelRepetition.dSVDensityRationalGrid_density_defect_le {N : ℕ} {w a : ℝ} (width : 0 < w) (grid : 0 < N) (nonnegative : 0 ≤ a) (bounded : a ≤ 1) : a - w * dSVUniformDensityGridPrefix N (dSVRationalSoftPass w a) ≤ a / w + w / ↑N

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedCoefficient_nonneg {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (i : Fin d) : 0 ≤ dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedCoefficient_sq {d : ℕ} {w : ℝ} (width : 0 < w) (N : ℕ) (ξ : BipartiteUnitVector d) (i : Fin d) : dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i ^ 2 = w * dSVUniformDensityGridPrefix N (dSVRationalSoftPass w (⋯.eigenvalues i))

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

Equations

• QuantumParallelRepetition.dSVDensityRationalCanonicalAliceBasis ξ = Classical.choose ⋯

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAliceBasis_target {d : ℕ} (ξ : BipartiteUnitVector d) : ↑ξ = schmidtVector (dSVUniformDensityPolarLeftSchmidtCoefficient ξ) (dSVDensityRationalCanonicalAliceBasis ξ) (dSVUniformDensityThresholdLeftBobBasis ξ)

noncomputable def QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget_norm_sq {d : ℕ} {w : ℝ} (width : 0 < w) (N : ℕ) (ξ : BipartiteUnitVector d) : ‖dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 = w * dSVDensityRationalLeftProjectiveDiagonalMass w N ξ

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget_distance_sq_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : ‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 = ∑ i : Fin d, (dSVUniformDensityPolarLeftSchmidtCoefficient ξ i - dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i) ^ 2

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedCoefficient_error_sq_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) (i : Fin d) : (dSVUniformDensityPolarLeftSchmidtCoefficient ξ i - dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i) ^ 2 ≤ ⋯.eigenvalues i / w + w / ↑N

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget_distance_sq_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) : ‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 ≤ 1 / w + ↑d * w / ↑N

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget_distance_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) : ‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ≤ √(1 / w + ↑d * w / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget_ne_zero {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : dSVDensityRationalCanonicalAcceptedTarget w N ξ ≠ 0

noncomputable def QuantumParallelRepetition.dSVDensityRationalCanonicalNormalizedTarget {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

• QuantumParallelRepetition.dSVDensityRationalCanonicalNormalizedTarget w N ξ = NormedSpace.normalize (QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedTarget w N ξ)

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalNormalizedTarget_norm {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : ‖dSVDensityRationalCanonicalNormalizedTarget w N ξ‖ = 1

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalNormalizedTarget_distance_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : ‖↑ξ - dSVDensityRationalCanonicalNormalizedTarget w N ξ‖ ≤ 2 * √(1 / w + ↑d * w / ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedUnitTarget {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : BipartiteUnitVector d

Equations

• QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine ξ = ⟨QuantumParallelRepetition.dSVDensityRationalCanonicalNormalizedTarget w N ξ, ⋯⟩

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalAcceptedUnitTarget_distance_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : ‖↑ξ - ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine ξ)‖ ≤ 2 * √(1 / w + ↑d * w / ↑N)

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

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

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidthRelativeMismatch_le_discrepancy {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N ≤ 1 / (2 * (w + 1))) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / dSVDensityRationalLeftProjectiveDiagonalMass w N ξ ≤ 2 * (w + 1) * (dSVUniformLeftDensitySpectralAtomDiscrepancy ξ ζ / w + ↑d / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidthRelativeMismatch_le_targetDistance {d N : ℕ} {w : ℝ} (large : 1 ≤ w) (grid : 0 < N) (fine : ↑d / ↑N ≤ 1 / (2 * (w + 1))) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / dSVDensityRationalLeftProjectiveDiagonalMass w N ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (w + 1) * (↑d / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidth_exists_fine_grid (d : ℕ) (dimension : 0 < d) (w : ℝ) (width : 0 < w) (ε : ℝ) (precision : 0 < ε) : ∃ (N : ℕ), 0 < N ∧ 2 * (w + 1) * (↑d / ↑N) ≤ ε

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidth_exists_sourceUniformParameters (d : ℕ) (dimension : 0 < d) (ε : ℝ) (precision : 0 < ε) (small : ε ≤ 1) : ∃ (w : ℝ) (N : ℕ), 1 ≤ w ∧ 0 < N ∧ 2 * (w + 1) * (↑d / ↑N) ≤ ε ∧ 1 / w + w * (↑d / ↑N) ≤ 3 * ε / 2 ∧ (∀ (ξ : BipartiteUnitVector d), 0 < dSVDensityRationalLeftProjectiveDiagonalMass w N ξ) ∧ ∀ (ξ ζ : BipartiteUnitVector d), dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / dSVDensityRationalLeftProjectiveDiagonalMass w N ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + ε

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidthPhysicalDiagonalBornSuccess_pos {d N : ℕ} (dimension : 0 < d) {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N ≤ 1 / (2 * (w + 1))) (ξ : BipartiteUnitVector d) : 0 < dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidthPhysicalRelativeHazard_eq {d N : ℕ} (dimension : 0 < d) {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N ≤ 1 / (2 * (w + 1))) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ = dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / dSVDensityRationalLeftProjectiveDiagonalMass w N ξ

theorem QuantumParallelRepetition.dSVDensityRationalLargeWidthPhysicalRelativeHazard_le {d N : ℕ} (dimension : 0 < d) {w : ℝ} (large : 1 ≤ w) (grid : 0 < N) (fine : ↑d / ↑N ≤ 1 / (2 * (w + 1))) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (w + 1) * (↑d / ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalMixedBornSuccess {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : ℝ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalMixedBornSuccess_eq {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalMixedBornSuccess grid dimension w ξ ζ = (∑ k : Fin N, (dSVDensityRationalPhysicalProjector w ξ k * dSVDensityRationalPhysicalProjector w ζ k).trace.re) / (↑d * ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalMixedBornSuccess_loss_le {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ - dSVDensityRationalPhysicalMixedBornSuccess grid dimension w ξ ζ ≤ dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ

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

Equations

• QuantumParallelRepetition.dSVDensityRationalActualMixedSuccessMass w N ξ ζ = ‖QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ true true‖ ^ 2

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

Equations

• QuantumParallelRepetition.dSVDensityRationalActualMixedContinueMass w N ξ ζ = ‖QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ false false‖ ^ 2

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalActualMixedSuccessMass_eq {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalActualMixedSuccessMass w N ξ ζ = dSVDensityRationalPhysicalMixedBornSuccess grid dimension w ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalActualMixedOutcome_norm_sq_eq_born {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) : ‖dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ a b‖ ^ 2 = binaryBornProbability (dSVUniformDensityThresholdSharedDensity grid dimension) (dSVDensityRationalPhysicalGlobalPOVM w ξ) (transposePOVM (dSVDensityRationalPhysicalGlobalPOVM w ζ)) a b

theorem QuantumParallelRepetition.dSVDensityRationalActualMixedContinueMass_eq_born {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalActualMixedContinueMass w N ξ ζ = binaryContinueProbability (dSVUniformDensityThresholdSharedDensity grid dimension) (dSVDensityRationalPhysicalGlobalPOVM w ξ) (transposePOVM (dSVDensityRationalPhysicalGlobalPOVM w ζ))

theorem QuantumParallelRepetition.dSVDensityRationalActualMixedAsynchronousMass_eq_born {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalActualMixedAsynchronousMass w N ξ ζ = binaryMismatchProbability (dSVUniformDensityThresholdSharedDensity grid dimension) (dSVDensityRationalPhysicalGlobalPOVM w ξ) (transposePOVM (dSVDensityRationalPhysicalGlobalPOVM w ζ))

theorem QuantumParallelRepetition.dSVDensityRationalActualMixed_mass_partition {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalActualMixedContinueMass w N ξ ζ + dSVDensityRationalActualMixedSuccessMass w N ξ ζ + dSVDensityRationalActualMixedAsynchronousMass w N ξ ζ = 1

def QuantumParallelRepetition.dSVDensityRationalCompletePhysicalStoppingCopyAccepted {N d : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (q : DSVUniformDensityThresholdLocalIndex N d) : Prop

Equations

• QuantumParallelRepetition.dSVDensityRationalCompletePhysicalStoppingCopyAccepted w ξ q = (QuantumParallelRepetition.dSVDensityRationalProjectiveThresholdBin w N q.fst (⋯.eigenvalues q.snd) = true)

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedOutcome {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

Equations

• QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedOutcome w N ξ ζ = QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ true true

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedRank {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (i : Fin d) : Fin (N + 1)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedRank_gridPrefix {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (i : Fin d) : dSVUniformDensityGridPrefix N (dSVRationalSoftPass w (⋯.eigenvalues i)) = ↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) / ↑N

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedRank_targetCoefficient_sq {d : ℕ} {w : ℝ} (width : 0 < w) (N : ℕ) (ξ : BipartiteUnitVector d) (i : Fin d) : dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i ^ 2 = w * ↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) / ↑N

theorem QuantumParallelRepetition.dSVUniformDensityGridPrefix_mono (N : ℕ) {a b : ℝ} (ordered : a ≤ b) : dSVUniformDensityGridPrefix N a ≤ dSVUniformDensityGridPrefix N b

theorem QuantumParallelRepetition.dSVUniformDensityThresholdMismatch_eq_sub_of_le (N : ℕ) {a b : ℝ} (ordered : a ≤ b) : dSVUniformDensityThresholdMismatch N a b = dSVUniformDensityGridPrefix N b - dSVUniformDensityGridPrefix N a

theorem QuantumParallelRepetition.dSVUniformDensityThresholdMismatch_eq_abs_gridPrefix (N : ℕ) (a b : ℝ) : dSVUniformDensityThresholdMismatch N a b = |dSVUniformDensityGridPrefix N a - dSVUniformDensityGridPrefix N b|

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedRankMismatch_eq_thresholdMismatch {d N : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : |↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) - ↑↑(dSVDensityRationalPhysicalAcceptedRank w N ζ j)| / ↑N = dSVUniformDensityThresholdMismatch N (dSVRationalSoftPass w (⋯.eigenvalues i)) (dSVRationalSoftPass w (⋯.eigenvalues j))

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPrefixRankMismatch_eq_atomMismatch {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPrefixRankMismatch w N ξ ζ = dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalPrefixRankMismatch_physicalHazard {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPrefixRankMismatch w N ξ ζ / ↑d = dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedRank_eq_floor {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) (i : Fin d) : ↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) = ⌊dSVRationalSoftPass w (⋯.eigenvalues i) * ↑N⌋₊

theorem QuantumParallelRepetition.dSVDensityRationalProjectiveThresholdBin_eq_true_iff_prefix {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ : BipartiteUnitVector d) (i : Fin d) (k : Fin N) : dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = true ↔ ↑k < ↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i)

noncomputable def QuantumParallelRepetition.dSVDensityRationalMixedSpectralAtomBlock {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) (k : Fin N) : Matrix (Fin d) (Fin d) ℂ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalMixedSpectralAtomBlock_eq_projectorProduct {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) (k : Fin N) : dSVDensityRationalMixedSpectralAtomBlock w N ξ ζ a b k = (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ξ).effect a * (dSVDensityRationalLeftProjectiveThresholdPOVM w N k ζ).effect b

theorem QuantumParallelRepetition.dSVDensityRationalMixedSpectralAtomBlock_trace_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (a b : Bool) (k : Fin N) : (dSVDensityRationalMixedSpectralAtomBlock w N ξ ζ a b k).trace.re = ∑ i : Fin d, ∑ j : Fin d, if dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = a ∧ dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues j) = b then spectralAtomOverlap (dSVSoftBobLeftReducedDensity ξ) (dSVSoftBobLeftReducedDensity ζ) ⋯ ⋯ i j else 0

theorem QuantumParallelRepetition.dSVDensityRationalActualMixedAsynchronousMass_eq_crossHazard {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalActualMixedAsynchronousMass w N ξ ζ = dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalActualMixed_escape_ge_diagonal {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ ≤ dSVDensityRationalActualMixedSuccessMass w N ξ ζ + dSVDensityRationalActualMixedAsynchronousMass w N ξ ζ

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalMixedAcceptedIntersectionRank {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : Fin (N + 1)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalMixedAcceptedThreshold_iff {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) (k : Fin N) : dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = true ∧ dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues j) = true ↔ ↑k < ↑(dSVDensityRationalPhysicalMixedAcceptedIntersectionRank w N ξ ζ i j)

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalMixedAcceptedThreshold_count {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : {k : Fin N | dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = true ∧ dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues j) = true}.card = ↑(dSVDensityRationalPhysicalMixedAcceptedIntersectionRank w N ξ ζ i j)

theorem QuantumParallelRepetition.dSVDensityRationalMixedAcceptedPrefix_norm_sq {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) : ‖dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ true true‖ ^ 2 = (∑ i : Fin d, ∑ j : Fin d, spectralAtomOverlap (dSVSoftBobLeftReducedDensity ξ) (dSVSoftBobLeftReducedDensity ζ) ⋯ ⋯ i j * ↑↑(dSVDensityRationalPhysicalMixedAcceptedIntersectionRank w N ξ ζ i j)) / (↑d * ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalPhysicalMixedAcceptedPrefixWork {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : EuclideanSpace ℂ (Fin N × Fin N)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalMixedAcceptedPrefixWork_norm_sq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : ‖dSVDensityRationalPhysicalMixedAcceptedPrefixWork w N ξ ζ i j‖ ^ 2 = ↑↑(dSVDensityRationalPhysicalMixedAcceptedIntersectionRank w N ξ ζ i j)

noncomputable def QuantumParallelRepetition.dSVDensityRationalCanonicalPrefixMask {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : Matrix (DSVUniformDensityThresholdLocalIndex N d) (DSVUniformDensityThresholdLocalIndex N d) ℂ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalPrefixMask_transpose {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : (dSVDensityRationalCanonicalPrefixMask w N ξ).transpose = dSVDensityRationalCanonicalPrefixMask w N ξ

theorem QuantumParallelRepetition.dSVDensityRationalPhysicalAcceptedProjector_eq_spectralMask {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : Matrix.blockDiagonal' (dSVDensityRationalPhysicalProjector w ξ) = ↑(dSVUniformDensityAliceHistorySpectralCopy ξ)⁻¹ * dSVDensityRationalCanonicalPrefixMask w N ξ * ↑(dSVUniformDensityAliceHistorySpectralCopy ξ)

noncomputable def QuantumParallelRepetition.dSVDensityRationalCanonicalPrefixSpectralOutcome {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalEffect {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : Option Bool → Matrix (DSVUniformDensityThresholdLocalIndex N d) (DSVUniformDensityThresholdLocalIndex N d) ℂ

Equations

• QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalEffect w N ξ none = 1
• QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalEffect w N ξ (some outcome) = (QuantumParallelRepetition.dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect outcome

noncomputable def QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalOutcome {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (alice bob : Option Bool) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalOutcome_some_some {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (alice bob : Bool) : dSVDensityRationalCompleteStoppedOptionalOutcome w N ξ ζ (some alice) (some bob) = dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ alice bob

theorem QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalOutcome_none_none {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalCompleteStoppedOptionalOutcome w N ξ ζ none none = dSVUniformDensityThresholdSharedState N d

def QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalSchedule (L : ℕ) (hit copy : Fin (L + 1)) : Option Bool

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalSchedule_zero (L : ℕ) (copy : Fin (L + 1)) : dSVDensityRationalCompleteStoppedOptionalLocalSchedule L 0 copy = if ↑copy < L then some false else none

theorem QuantumParallelRepetition.dSVDensityRationalCompleteStoppedOptionalLocalSchedule_hit {L : ℕ} (j : Fin L) : dSVDensityRationalCompleteStoppedOptionalLocalSchedule L j.succ j.castSucc = some true

noncomputable def QuantumParallelRepetition.dSVDensityRationalFirstAcceptLocalSpectralMask {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (outcome : Bool) : Matrix (DSVUniformDensityThresholdLocalIndex N d) (DSVUniformDensityThresholdLocalIndex N d) ℂ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalFirstAcceptPhysicalEffect_eq_spectralMask {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (outcome : Bool) : (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ξ).effect outcome = ↑(dSVUniformDensityAliceHistorySpectralCopy ξ)⁻¹ * dSVDensityRationalFirstAcceptLocalSpectralMask w N ξ outcome * ↑(dSVUniformDensityAliceHistorySpectralCopy ξ)

theorem QuantumParallelRepetition.dSVDensityRationalFirstAcceptLocalSpectralMask_transpose {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) (outcome : Bool) : (dSVDensityRationalFirstAcceptLocalSpectralMask w N ξ outcome).transpose = dSVDensityRationalFirstAcceptLocalSpectralMask w N ξ outcome

theorem QuantumParallelRepetition.dSVDensityRationalFirstAcceptPhysicalBobEffect_eq_spectralMask {d : ℕ} (w : ℝ) (N : ℕ) (ζ : BipartiteUnitVector d) (outcome : Bool) : (transposePOVM (dSVDensityRationalCompleteProjectiveBinaryPOVM w N ζ)).effect outcome = ↑(dSVUniformDensityBobHistoryCopyBasis ζ) * dSVDensityRationalFirstAcceptLocalSpectralMask w N ζ outcome * ↑(dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹

def QuantumParallelRepetition.dSVDensityRationalFirstAcceptActualTensorBasis {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (U : ↥(Matrix.unitaryGroup β ℂ)) : ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × (Fin (L + 1) → β)) ℂ)

Equations

• QuantumParallelRepetition.dSVDensityRationalFirstAcceptActualTensorBasis U = QuantumParallelRepetition.controlledFiniteTensorLocalUnitary fun (_stop _copy : Fin (L + 1)) => U

theorem QuantumParallelRepetition.tensorEmbezzlementTarget_sub_norm {d n : ℕ} (positive : 0 < n) (ξ ζ : BipartiteUnitVector d) : ‖tensorEmbezzlementTarget ξ - tensorEmbezzlementTarget ζ‖ = ‖↑ξ - ↑ζ‖

theorem QuantumParallelRepetition.dSVBobTargetLocalHarmonicCleanup_stable {d n : ℕ} (hn : 0 < n) (U V : ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)) (ξ ζ : BipartiteUnitVector d) (ε : ℝ) (clean : ‖localUnitaryAction U V (tensorEmbezzlementTarget ζ) - embezzlementState (d * n)‖ ≤ ε) : ‖localUnitaryAction U V (tensorEmbezzlementTarget ξ) - embezzlementState (d * n)‖ ≤ ‖↑ξ - ↑ζ‖ + ε

theorem QuantumParallelRepetition.dSVBobTargetLocalUniformHarmonicWorkCleanup {T : Type u_1} (d : ℕ) (dimension : 0 < d) (work : T → BipartiteUnitVector d) (ε : ℝ) (precision : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∃ (A : T → ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)) (B : T → ↥(Matrix.unitaryGroup (Fin (d * n)) ℂ)), (∀ (ζ : T), ‖localUnitaryAction (A ζ) (B ζ) (tensorEmbezzlementTarget (work ζ)) - embezzlementState (d * n)‖ ≤ ε) ∧ ∀ (ξ ζ : T), ‖localUnitaryAction (A ζ) (B ζ) (tensorEmbezzlementTarget (work ξ)) - embezzlementState (d * n)‖ ≤ ‖↑(work ξ) - ↑(work ζ)‖ + ε

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalUnitPrefix_relative_distance_sq {N : ℕ} (grid : 0 < N) (r s : Fin (N + 1)) : ‖↑(dSVCanonicalFailureUnitRankFamily N grid r) - ↑(dSVCanonicalFailureUnitRankFamily N grid s)‖ ^ 2 ≤ 4 * |↑↑r - ↑↑s| / ↑(max 1 (min ↑r ↑s))

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketLocalHarmonicCleanup_sq {Ω : Type u_1} {I : Type u_2} [DecidableEq I] {N D : ℕ} (dimension : 0 < N) (work : Fin D → BipartiteUnitVector N) (bucket : Ω → Fin D → I) (representative : Ω → I → Fin D) (ε : ℝ) (precision : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ (phase : Ω) (r s : Fin D), ‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s)) (tensorEmbezzlementTarget (work r)) - embezzlementState (N * n)‖ ^ 2 ≤ 2 * ε ^ 2 + 2 * ‖↑(work r) - ↑(work (representative phase (bucket phase r)))‖ ^ 2 + 4 * if bucket phase r = bucket phase s then 0 else 1

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCanonicalPrefixCleanup_sq {Ω : Type u_1} {I : Type u_2} [DecidableEq I] {N : ℕ} (grid : 0 < N) (bucket : Ω → Fin (N + 1) → I) (representative : Ω → I → Fin (N + 1)) (ε : ℝ) (precision : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ (phase : Ω) (r s : Fin (N + 1)), ‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s)) (tensorEmbezzlementTarget (dSVCanonicalFailureUnitRankFamily N grid r)) - embezzlementState (N * n)‖ ^ 2 ≤ 2 * ε ^ 2 + 8 * |↑↑r - ↑↑(representative phase (bucket phase r))| / ↑(max 1 (min ↑r ↑(representative phase (bucket phase r)))) + 4 * if bucket phase r = bucket phase s then 0 else 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory {H : Type u_1} [Fintype H] (B : ℕ) (history : EuclideanSpace ℂ (H × H)) : EuclideanSpace ℂ ((Fin B × H) × Fin B × H)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory_apply {H : Type u_1} [Fintype H] (B : ℕ) (history : EuclideanSpace ℂ (H × H)) (φ ψ : Fin B) (a b : H) : (dSVDensityRationalPublicBucketCoherentPhaseHistory B history).ofLp ((φ, a), ψ, b) = (ePRState B).ofLp (φ, ψ) * history.ofLp (a, b)

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory_apply_norm_sq {H : Type u_1} [Fintype H] {B : ℕ} (positive : 0 < B) (history : EuclideanSpace ℂ (H × H)) (φ ψ : Fin B) (a b : H) : ‖(dSVDensityRationalPublicBucketCoherentPhaseHistory B history).ofLp ((φ, a), ψ, b)‖ ^ 2 = (if φ = ψ then (↑B)⁻¹ else 0) * ‖history.ofLp (a, b)‖ ^ 2

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseSigmaState {H : Type u_1} [Fintype H] {m : ℕ} (B : ℕ) (history : EuclideanSpace ℂ (H × H)) (work : Fin B → H → H → EuclideanSpace ℂ (Fin m × Fin m)) : EuclideanSpace ℂ (((_ : Fin B × H) × Fin m) × (_ : Fin B × H) × Fin m)

Equations

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

def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseLocalUnitary {H : Type u_1} {I : Type u_2} [Fintype H] [DecidableEq H] [DecidableEq I] {B D m : ℕ} (rank : H → Fin D) (bucket : Fin B → Fin D → I) (A : Fin B → I → ↥(Matrix.unitaryGroup (Fin m) ℂ)) : ↥(Matrix.unitaryGroup ((_ : Fin B × H) × Fin m) ℂ)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseSigmaReset_distance_sq {H : Type u_1} {I : Type u_2} [Fintype H] [DecidableEq H] [DecidableEq I] {B D m : ℕ} (phase_positive : 0 < B) (history : EuclideanSpace ℂ (H × H)) (rankA rankB : H → Fin D) (bucket : Fin B → Fin D → I) (A C : Fin B → I → ↥(Matrix.unitaryGroup (Fin m) ℂ)) (work target : Fin B → H → H → EuclideanSpace ℂ (Fin m × Fin m)) : ‖dSVUniformDensityPhysicalAsyncSigmaContinuation (fun (q : Fin B × H) => A q.1 (bucket q.1 (rankA q.2))) (fun (q : Fin B × H) => C q.1 (bucket q.1 (rankB q.2))) (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history work) - dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history target‖ ^ 2 = (∑ φ : Fin B, ∑ a : H, ∑ b : H, ‖history.ofLp (a, b)‖ ^ 2 * ‖localUnitaryAction (A φ (bucket φ (rankA a))) (C φ (bucket φ (rankB b))) (work φ a b) - target φ a b‖ ^ 2) / ↑B

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_real_log_bound {r s : ℝ} (positive_r : 0 < r) (positive_s : 0 < s) : min r s * |Real.log r - Real.log s| ≤ |r - s|

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_zeroSafe_nat_bound (r s : ℕ) : min ↑r ↑s * |Real.log ↑(max 1 r) - Real.log ↑(max 1 s)| ≤ |↑r - ↑s|

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_zeroSafe_fin_bound {N : ℕ} (r s : Fin (N + 1)) : min ↑↑r ↑↑s * |Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑s)| ≤ |↑↑r - ↑↑s|

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) : ℕ

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel Q r = ⌊↑Q * Real.log ↑(max 1 ↑r)⌋₊

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight (B : ℕ) : Fin B → ℝ

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight B x✝ = 1 / ↑B

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight_sum {B : ℕ} (positive : 0 < B) : ∑ phase : Fin B, dSVDensityRationalPublicLogRankPhaseWeight B phase = 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) : Option ℕ

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket Q phase r = if ↑r = 0 then none else some ((QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel Q r + ↑phase) / B)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket_fineLabel_sub_lt {N B : ℕ} (Q : ℕ) (phase : Fin B) (r s : Fin (N + 1)) (nonzero_r : ↑r ≠ 0) (nonzero_s : ↑s ≠ 0) (same : dSVDensityRationalPublicLogRankBucket Q phase r = dSVDensityRationalPublicLogRankBucket Q phase s) : |↑(dSVDensityRationalPublicLogRankFineLabel Q r) - ↑(dSVDensityRationalPublicLogRankFineLabel Q s)| < ↑B

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_logCoordinate_nonneg {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) : 0 ≤ ↑Q * Real.log ↑(max 1 ↑r)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel_bounds {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) : ↑(dSVDensityRationalPublicLogRankFineLabel Q r) ≤ ↑Q * Real.log ↑(max 1 ↑r) ∧ ↑Q * Real.log ↑(max 1 ↑r) < ↑(dSVDensityRationalPublicLogRankFineLabel Q r) + 1

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket_log_sub_lt {N B Q : ℕ} (positive_Q : 0 < Q) (phase : Fin B) (r s : Fin (N + 1)) (nonzero_r : ↑r ≠ 0) (nonzero_s : ↑s ≠ 0) (same : dSVDensityRationalPublicLogRankBucket Q phase r = dSVDensityRationalPublicLogRankBucket Q phase s) : |Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑s)| < (↑B + 1) / ↑Q

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketFiber {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) : Finset (Fin (N + 1))

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketFiber Q phase label = {r : Fin (N + 1) | ↑r ≠ 0 ∧ QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket Q phase r = label}

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketFiber_mem {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) (r : Fin (N + 1)) : r ∈ dSVDensityRationalPublicLogRankBucketFiber Q phase label ↔ ↑r ≠ 0 ∧ dSVDensityRationalPublicLogRankBucket Q phase r = label

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) : Fin (N + 1)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_mem {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) (present : (dSVDensityRationalPublicLogRankBucketFiber Q phase label).Nonempty) : dSVDensityRationalPublicLogRankBucketRepresentative Q phase label ∈ dSVDensityRationalPublicLogRankBucketFiber Q phase label

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_same {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) : ↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) ≠ 0 ∧ dSVDensityRationalPublicLogRankBucket Q phase (dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) = dSVDensityRationalPublicLogRankBucket Q phase r

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_le {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) : dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r) ≤ r

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_log_sub_lt {N B Q : ℕ} (positive_Q : 0 < Q) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) : |Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)))| < (↑B + 1) / ↑Q

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase (S B : ℕ) : Type

Equations

• QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase S B = (Fin S → Fin B)

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseIndex (S B : ℕ) : Type

Equations

• QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseIndex S B = Fin (Fintype.card (QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase S B))

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhase_card (S B : ℕ) : Fintype.card (DSVDensityRationalPublicMultiscalePhase S B) = B ^ S

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhase_card_pos {S B : ℕ} (positive : 0 < B) : 0 < Fintype.card (DSVDensityRationalPublicMultiscalePhase S B)

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPrefixHarmonicSpectralOverlap_nonneg {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : 0 ≤ dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j

noncomputable def QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : ℂ

Equations

• QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j = ↑(QuantumParallelRepetition.unitaryBasisOverlap ⋯.eigenvectorUnitary ⋯.eigenvectorUnitary) i j

theorem QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap_norm_sq {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : ‖dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j‖ ^ 2 = dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j

noncomputable def QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairHistory {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin d × Fin d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairHistory_apply_norm_sq {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : ‖(dSVDensityRationalLocalSpectralPairHistory N ξ ζ).ofLp (i, j)‖ ^ 2 = dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j / (↑d * ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalMixedCanonicalCrossMatrix {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) : Matrix (DSVUniformDensityThresholdLocalIndex N d) (DSVUniformDensityThresholdLocalIndex N d) ℂ

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalCrossGauge_eq {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) : ↑(dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ * ↑(dSVUniformDensityBobHistoryCopyBasis ξ) = dSVDensityRationalMixedCanonicalCrossMatrix N ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalCanonicalPrefixMask_eq_diagonal {d : ℕ} (w : ℝ) (N : ℕ) (ξ : BipartiteUnitVector d) : dSVDensityRationalCanonicalPrefixMask w N ξ = Matrix.diagonal fun (q : DSVUniformDensityThresholdLocalIndex N d) => if dSVDensityRationalProjectiveThresholdBin w N q.fst (⋯.eigenvalues q.snd) = true then 1 else 0

noncomputable def QuantumParallelRepetition.dSVDensityRationalMixedCanonicalRawSource {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalRawSource_apply {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (k l : Fin N) (i j : Fin d) : (dSVDensityRationalMixedCanonicalRawSource w N ξ ζ).ofLp (⟨k, i⟩, ⟨l, j⟩) = if k = l ∧ dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = true ∧ dSVDensityRationalProjectiveThresholdBin w N l (⋯.eigenvalues j) = true then dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j else 0

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalProjectorMatrix_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : ↑(dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ * ((Matrix.blockDiagonal' fun (k : Fin N) => dSVDensityRationalPhysicalProjector w ξ k) * Matrix.blockDiagonal' fun (k : Fin N) => dSVDensityRationalPhysicalProjector w ζ k).transpose * (↑(dSVUniformDensityAliceHistorySpectralCopy ξ)).transpose = dSVDensityRationalCanonicalPrefixMask w N ζ * dSVDensityRationalMixedCanonicalCrossMatrix N ξ ζ * dSVDensityRationalCanonicalPrefixMask w N ξ

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalSpectralOutcome_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalCanonicalPrefixSpectralOutcome w N ξ ζ = ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ • dSVDensityRationalMixedCanonicalRawSource w N ξ ζ

def QuantumParallelRepetition.dSVDensityRationalPublicLogBilateralPureTensor {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (v : EuclideanSpace ℂ (ι × ι)) (u : EuclideanSpace ℂ (κ × κ)) : EuclideanSpace ℂ ((ι × κ) × ι × κ)

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogBilateralPureTensor v u = WithLp.toLp 2 fun (q : (ι × κ) × ι × κ) => v.ofLp (q.1.1, q.2.1) * u.ofLp (q.1.2, q.2.2)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogBilateralPureTensor_norm_sq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (v : EuclideanSpace ℂ (ι × ι)) (u : EuclideanSpace ℂ (κ × κ)) : ‖dSVDensityRationalPublicLogBilateralPureTensor v u‖ ^ 2 = ‖v‖ ^ 2 * ‖u‖ ^ 2

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseHistoryLocalIndex (B N d L : ℕ) : Type

Equations

• QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L = (Fin B × QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePureSource (B N d L : ℕ) : EuclideanSpace ℂ (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePureSource_apply (B N d L : ℕ) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) : (dSVDensityRationalPublicLogPhasePureSource B N d L).ofLp ((φ, a), ψ, b) = (if φ = ψ then ↑(√↑B)⁻¹ else 0) * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (a, b)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePureSource_norm {B N d L : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) : ‖dSVDensityRationalPublicLogPhasePureSource B N d L‖ = 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseHarmonicPureSource (B N d L m : ℕ) : EuclideanSpace ℂ ((DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m) × DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseHarmonicPureSource_apply (B N d L m : ℕ) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) (i j : Fin m) : (dSVDensityRationalPublicLogPhaseHarmonicPureSource B N d L m).ofLp (((φ, a), i), (ψ, b), j) = (if φ = ψ then ↑(√↑B)⁻¹ else 0) * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (a, b) * (embezzlementState m).ofLp (i, j)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseHarmonicPureSource_norm {B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) : ‖dSVDensityRationalPublicLogPhaseHarmonicPureSource B N d L m‖ = 1

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex (B N d L : ℕ) : Type

Equations

• QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex B N d L = (Fin B × QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryCatalystIndex N d L)

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetSplitEquiv (B N d L : ℕ) : DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L ≃ Fin d × DSVDensityRationalPublicLogPhaseCatalystIndex B N d L

Equations

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

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseResidual (B N d L m : ℕ) : ℕ

Equations

• QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseResidual B N d L m = Fintype.card (QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex B N d L) * m

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv (B N d L m : ℕ) : DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m ≃ Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m)

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource (B N d L m : ℕ) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m) × Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m))

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource_apply (B N d L m : ℕ) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) (i j : Fin m) : (dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource B N d L m).ofLp ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((φ, a), i), (dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((ψ, b), j)) = (if φ = ψ then ↑(√↑B)⁻¹ else 0) * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (a, b) * (embezzlementState m).ofLp (i, j)

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource_norm {B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) : ‖dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource B N d L m‖ = 1

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseHistoryLocalIndex (S B N d L : ℕ) : Type

Equations

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

def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseResidual (S B N d L m : ℕ) : ℕ

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv (S B N d L m : ℕ) : DSVDensityRationalPublicMultiscalePhaseHistoryLocalIndex S B N d L × Fin m ≃ Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource (S B N d L m : ℕ) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource_norm {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) : ‖dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource S B N d L m‖ = 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift (B N d L m : ℕ) (U : ↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)) : ↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m)) ℂ)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift_apply (B N d L m : ℕ) (U : ↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)) (a b : DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) (i j : Fin m) : ↑(dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift B N d L m U) ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) (a, i)) ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) (b, j)) = if i = j then ↑U a b else 0

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary (B : ℕ) {N d L : ℕ} (U : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)) : ↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary_apply (B : ℕ) {N d L : ℕ} (U : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) : ↑(dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary B U) (φ, a) (ψ, b) = if φ = ψ then ↑U a b else 0