Quantum parallel repetition, part 03

@[instance_reducible]

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

The local matrix norm instance used while elaborating part three.

Equations

• QuantumParallelRepetition.matrixComplexContinuousENormPartThree = SeminormedAddGroup.toContinuousENorm

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

The DSV density rational physical diagonal born success construction used in the quantum parallel-repetition argument.

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

The DSV density rational physical projector cross hazard construction used in the quantum parallel-repetition argument.

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

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

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

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

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)

The finite outcome encoding for DSV density rational complete projective.

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

The DSV density rational canonical accepted coefficient construction used in the quantum parallel-repetition argument.

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

The DSV density rational canonical alice basis construction used in the quantum parallel- repetition argument.

Equations

• QuantumParallelRepetition.dSVDensityRationalCanonicalAliceBasis ξ = Classical.choose ⋯

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

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

The target object for DSV density rational canonical accepted.

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, (dSVUniformLeftDensitySchmidtCoefficient ξ 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) : (dSVUniformLeftDensitySchmidtCoefficient ξ 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.dSVDensityRationalCanonicalAcceptedUnitTarget {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (ξ : BipartiteUnitVector d) : BipartiteUnitVector d

The target object for DSV density rational canonical accepted unit.

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)

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

The DSV density rational complete physical stopping copy accepted construction used in the quantum parallel-repetition argument.

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)

The finite outcome encoding for DSV density rational physical accepted.

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)

The rank map for DSV density rational physical accepted.

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

The DSV density rational prefix rank mismatch construction used in the quantum parallel- repetition argument.

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.dSVDensityRationalPhysicalMixedAcceptedIntersectionRank {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : Fin (N + 1)

The rank map for DSV density rational physical mixed accepted intersection.

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)

The DSV density rational physical mixed accepted prefix work construction used in the quantum parallel-repetition argument.

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.dSVDensityRationalCanonicalPrefixSpectralOutcome {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The finite outcome encoding for DSV density rational canonical prefix spectral.

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

The measurement effect for DSV density rational complete stopped optional local.

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)

The finite outcome encoding for DSV density rational complete stopped optional.

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

The finite schedule for DSV density rational complete stopped optional local.

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

The DSV density rational first accept local spectral mask construction used in the quantum parallel-repetition argument.

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

The DSV density rational first accept actual tensor basis construction used in the quantum parallel-repetition argument.

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} (B : ℕ) (history : EuclideanSpace ℂ (H × H)) : EuclideanSpace ℂ ((Fin B × H) × Fin B × H)

The transcript representation for DSV density rational public bucket coherent phase.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory_apply {H : Type u_1} (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} {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} {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)

The quantum state representing DSV density rational public bucket coherent phase sigma.

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

The unitary operator implementing DSV density rational public bucket coherent phase local.

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] {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)) : ℕ

The DSV density rational public log rank fine label construction used in the quantum parallel- repetition argument.

Equations

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

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

The probability weight for DSV density rational public log rank phase.

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 ℕ

The DSV density rational public log rank bucket construction used in the quantum parallel- repetition argument.

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.dSVDensityRationalPublicLogRankBucketRepresentative {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) : Fin (N + 1)

The DSV density rational public log rank bucket representative construction used in the quantum parallel-repetition argument.

Equations

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

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

The type used to represent DSV density rational public multiscale phase in the exact sampling construction.

Equations

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

@[reducible, inline]

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

The type used to represent DSV density rational public multiscale phase index in the exact sampling construction.

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

The overlap quantity for DSV density rational prefix harmonic spectral.

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

The overlap quantity for DSV density rational local spectral pair basis.

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)

The transcript representation for DSV density rational local spectral pair.

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.dSVDensityRationalMixedCanonicalRawSource {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The source object for DSV density rational mixed canonical raw.

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.dSVDensityRationalMixedCanonicalSpectralOutcome_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalCanonicalPrefixSpectralOutcome w N ξ ζ = ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ • dSVDensityRationalMixedCanonicalRawSource w N ξ ζ

@[reducible, inline]

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

The type used to represent DSV density rational public log phase history local index in the exact sampling construction.

Equations

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

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

The DSV density rational public log phase residual construction used in the quantum parallel- repetition argument.

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)

The finite equivalence encoding DSV density rational public log phase target first index.

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

The source object for DSV density rational public log phase target first prepared.

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

The type used to represent DSV density rational public multiscale phase history local index in the exact sampling construction.

Equations

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

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

The DSV density rational public multiscale phase residual construction used in the quantum parallel-repetition argument.

Equations

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

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

The finite equivalence encoding DSV density rational public multiscale phase target first index.

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

The source object for DSV density rational public multiscale phase target first prepared.

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

The DSV density rational public log phase actual target first local lift construction used in the quantum parallel-repetition argument.

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

The unitary operator implementing DSV density rational public log phase physical history.

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) : Fin (L + 1)

The DSV density rational heterogeneous actual first accepted construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_prefix_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (j : Fin L) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = j.succ ↔ accepted j (history j.castSucc) ∧ ∀ i < j, ¬accepted i (history i.castSucc)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_zero_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = 0 ↔ ∀ (i : Fin L), ¬accepted i (history i.castSucc)

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

The unitary operator implementing DSV density rational heterogeneous actual first accept.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_mulVec {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (_ : Fin (L + 1)) × (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) : (↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec v ⟨flag, history⟩ = v ⟨(Equiv.swap 0 (dSVDensityRationalHeterogeneousActualFirstAccepted accepted history)) flag, history⟩

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_zeroFlag {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) : (↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec (fun (q : (_ : Fin (L + 1)) × (Fin (L + 1) → β)) => if q.fst = 0 then v q.snd else 0) ⟨flag, history⟩ = if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then v history else 0

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyAccepted {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (j : Fin L) (atom : DSVUniformDensityThresholdLocalIndex N d) : Prop

The DSV density rational heterogeneous actual copy accepted construction used in the quantum parallel-repetition argument.

Equations

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

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyCondition {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (flag i : Fin (L + 1)) (atom : β) : Prop

The DSV density rational heterogeneous actual copy condition construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_allFlags_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (flag : Fin (L + 1)) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = flag ↔ ∀ (i : Fin (L + 1)), dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i (history i)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_sourceProduct {β : Type u_1} [Fintype β] {L : ℕ} (accepted : Fin L → β → Prop) (flag : Fin (L + 1)) (A D : Fin (L + 1) → β → ℂ) : (∑ history : Fin (L + 1) → β, (∏ i : Fin (L + 1), A i (history i)) * if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then ∏ i : Fin (L + 1), D i (history i) else 0) = ∏ i : Fin (L + 1), ∑ atom : β, A i atom * if dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i atom then D i atom else 0

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

The unitary operator implementing DSV density rational heterogeneous actual physical local.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAliceUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual alice.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualBobUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ζ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual bob.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

The quantum state representing DSV density rational heterogeneous actual physical.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState_norm {S N d L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ‖dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ‖ = 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) : ℝ

The finite outcome encoding for DSV density rational heterogeneous physical stage.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

The DSV density rational heterogeneous physical stage continue construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageSuccess {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

The DSV density rational heterogeneous physical stage success construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

The DSV density rational heterogeneous physical stage asynchronous construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalStageOutcome N width schedule ξ ζ k alice bob

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k = 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k = dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

The DSV density rational heterogeneous physical survival construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

The total probability mass of DSV density rational heterogeneous physical stopped success.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

The total probability mass of DSV density rational heterogeneous physical stopped asynchronous.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

The total probability mass of DSV density rational heterogeneous physical terminal.

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ L

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStopped_mass_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ = ∑ k : Fin L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑k * dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_lower {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) : 1 / (2 * (width (schedule k) + 1) * ↑d) ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_escape_ge_diagonal {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_relative_diagonal_le {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (width (schedule k) + 1) * (↑d / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedEscape_budget {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ∑ k ∈ Finset.range L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k * (dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k) ≤ 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_le_targetDistance {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (upper : ∀ (s : Fin S), width s ≤ W) (W_nonnegative : 0 ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (W + 1) * (↑d / ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate (d : ℕ) (W : ℝ) : ℝ

The error rate associated with DSV density rational heterogeneous physical uniform escape.

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W = 1 / (2 * (W + 1) * ↑d)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_pos {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) : 0 < dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_le_half {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) : dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ 1 / 2

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_ge_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue_le_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑k ≤ 1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_pow {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysical_exists_positive_horizon {d : ℕ} (dimension : 0 < d) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (precision : 0 < ε) : ∃ (L : ℕ), 0 < L ∧ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_horizon {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (tail : (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ ε ^ 2

noncomputable def QuantumParallelRepetition.fairPartitionWeight (α : Type u_2) [Fintype α] : ℝ

The probability weight for fair partition.

Equations

• QuantumParallelRepetition.fairPartitionWeight α = (2 ^ Fintype.card α)⁻¹

noncomputable def QuantumParallelRepetition.reversePartitionWeight {α : Type u_1} [Fintype α] (s : Finset α) : ℝ

The probability weight for reverse partition.

Equations

• QuantumParallelRepetition.reversePartitionWeight s = QuantumParallelRepetition.fairPartitionWeight α * (2 * ↑s.card / ↑(Fintype.card α))

noncomputable def QuantumParallelRepetition.forwardMarkedPartitionWeight (α : Type u_2) [Fintype α] : ℝ

The probability weight for forward marked partition.

Equations

• QuantumParallelRepetition.forwardMarkedPartitionWeight α = 2 * QuantumParallelRepetition.fairPartitionWeight α / ↑(Fintype.card α)

noncomputable def QuantumParallelRepetition.reverseMarkedPartitionWeight {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (i : α) : ℝ

The probability weight for reverse marked partition.

Equations

• QuantumParallelRepetition.reverseMarkedPartitionWeight s i = if i ∈ s then QuantumParallelRepetition.reversePartitionWeight s / ↑s.card else 0

theorem QuantumParallelRepetition.fairPartitionWeight_pos {α : Type u_1} [Fintype α] : 0 < fairPartitionWeight α

theorem QuantumParallelRepetition.fairPartitionWeight_nonneg {α : Type u_1} [Fintype α] : 0 ≤ fairPartitionWeight α

theorem QuantumParallelRepetition.fairPartitionWeight_sum {α : Type u_1} [Fintype α] : ∑ _s : Finset α, fairPartitionWeight α = 1

theorem QuantumParallelRepetition.reversePartitionWeight_nonneg {α : Type u_1} [Fintype α] (s : Finset α) : 0 ≤ reversePartitionWeight s

@[simp]

theorem QuantumParallelRepetition.reversePartitionWeight_empty {α : Type u_1} [Fintype α] : reversePartitionWeight ∅ = 0

theorem QuantumParallelRepetition.reversePartitionWeight_pos_iff {α : Type u_1} [Fintype α] (hα : 0 < Fintype.card α) (s : Finset α) : 0 < reversePartitionWeight s ↔ s.Nonempty

theorem QuantumParallelRepetition.reverseMarkedPartitionWeight_eq_forward {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {i : α} (hi : i ∈ s) : reverseMarkedPartitionWeight s i = forwardMarkedPartitionWeight α

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

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

theorem QuantumParallelRepetition.fullHistoryWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) : ∑ h : FullSubsetHistory X Y n D L, fullHistoryWeight G h = 1

theorem QuantumParallelRepetition.fullHistoryWinIndicator_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G h α β ≤ 1

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

The full history answer count construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.fullHistoryAnswerCount D = ↑(Fintype.card (↥D → A)) * ↑(Fintype.card (↥D → B))

theorem QuantumParallelRepetition.fullHistoryAnswerCount_eq {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : fullHistoryAnswerCount D = ↑(Fintype.card A) ^ D.card * ↑(Fintype.card B) ^ D.card

@[reducible, inline]

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

The type used to represent full history entropy atom in the exact sampling construction.

Equations

• QuantumParallelRepetition.FullHistoryEntropyAtom X Y A B n D L = (QuantumParallelRepetition.FullSubsetHistory X Y n D L × (↥D → A) × (↥D → B))

def QuantumParallelRepetition.fullHistoryAtomCountingWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : ℝ

The probability weight for full history atom counting.

Equations

• QuantumParallelRepetition.fullHistoryAtomCountingWeight G D L t = QuantumParallelRepetition.fullHistoryWeight G t.1 * QuantumParallelRepetition.fullHistoryWinIndicator G t.1 t.2.1 t.2.2

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

The total probability mass of full history atom born.

Equations

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

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : 0 ≤ fullHistoryAtomCountingWeight G D L t

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : 0 ≤ fullHistoryAtomBornMass G n S D L t

theorem QuantumParallelRepetition.bornTracePairing_contractions_le_one {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : ((bornTracePairing ρ.matrix) F) G ≤ 1

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : fullHistoryAtomBornMass G n S D L t ≤ 1

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t ≤ fullHistoryAnswerCount D

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * fullHistoryAtomBornMass G n S D L t = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)

theorem QuantumParallelRepetition.fullHistoryAtomEntropy_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * (fullHistoryAtomBornMass G n S D L t).negMulLog ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_lower_bound {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) : -((strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))) ≤ fullHistoryAliceEntropyPotential G n S D L

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

A transcript in which one additional coordinate is being revealed.

• aliceConditioned : ↥D → X

  Alice's conditioned part of the transcript.

• bobConditioned : ↥D → Y

  Bob's conditioned part of the transcript.

• aliceRevealed : ↥L → X

  Alice's already revealed questions.

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

  Bob's questions outside the revealed coordinates.

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

@[instance_reducible]

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

Equations

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

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

def QuantumParallelRepetition.fullCoordinateOldHistory {X : Type u_1} {Y : Type u_2} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) : FullSubsetHistory X Y n D L

The transcript representation for full coordinate old.

Equations

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

def QuantumParallelRepetition.fullCoordinateNewHistory {X : Type u_1} {Y : Type u_2} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) : FullSubsetHistory X Y n D (insert i L)

The transcript representation for full coordinate new.

Equations

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

theorem QuantumParallelRepetition.finsetSubtype_prod_insert {ι : Type u_1} {T : Type u_2} [DecidableEq ι] [CommMonoid T] (s : Finset ι) (i : ι) (hi : i ∉ s) (f : ↥(insert i s) → T) : ∏ j : ↥(insert i s), f j = f ⟨i, ⋯⟩ * ∏ j : ↥s, f ⟨↑j, ⋯⟩

theorem QuantumParallelRepetition.fullHistoryRemaining_prod_split {n : ℕ} {T : Type u_1} [CommMonoid T] (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : ↥(fullHistoryRemaining n D L) → T) : ∏ j : ↥(fullHistoryRemaining n D L), f j = f ⟨i, ⋯⟩ * ∏ j : ↥(fullHistoryRemaining n D (insert i L)), f ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullCoordinateBaseWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) : ℝ

The probability weight for full coordinate base.

Equations

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

theorem QuantumParallelRepetition.fullCoordinateBaseWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) : 0 ≤ fullCoordinateBaseWeight G D L i h

theorem QuantumParallelRepetition.fullCoordinateOldHistory_weight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) : fullHistoryWeight G (fullCoordinateOldHistory D L i h y) = fullCoordinateBaseWeight G D L i h * G.marginalY y

theorem QuantumParallelRepetition.fullCoordinateNewHistory_weight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) : fullHistoryWeight G (fullCoordinateNewHistory D L i h x) = fullCoordinateBaseWeight G D L i h * G.marginalX x

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_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 b : ι) (i j : d) : ((finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b)) i j = ∑ r : d, inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - ensemblePurificationSubspaceEntry F M positive hM b r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - ensemblePurificationSubspaceEntry F M positive hM b r j)

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

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_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 b : ι) : (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s) * (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB = finiteLocalPurificationVector S (KA - KA') KB

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB KB' : Matrix eB S.Bob ℂ) : finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB' = finiteLocalPurificationVector S KA (KB - KB')

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left_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 KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : ‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB‖ ^ 2 = ((bornTracePairing S.state.matrix) ((KA - KA').conjTranspose * (KA - KA'))) (KB.conjTranspose * KB)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right_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 KB' : Matrix eB S.Bob ℂ) : ‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB'‖ ^ 2 = ((bornTracePairing S.state.matrix) (KA.conjTranspose * KA)) ((KB - KB').conjTranspose * (KB - KB'))

theorem QuantumParallelRepetition.matrixLogEntropy_weighted_jensen_posSemidef {ι : 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) : (∑ i : ι, weight i • cfc (fun (z : ℝ) => z * Real.log z) (F i) - cfc (fun (z : ℝ) => z * Real.log z) M).PosSemidef

theorem QuantumParallelRepetition.conditionalAlice_matrixLogEntropy_gap_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {d : Type u_5} [Fintype d] [DecidableEq d] (G : Game X Y A B) (H : X → Matrix d d ℂ) (hH : ∀ (x : X), (H x).PosSemidef) (y : Y) (hy : 0 < G.marginalY y) : (conditionalAliceAverage G (fun (x : X) => cfc (fun (z : ℝ) => z * Real.log z) (H x)) y - cfc (fun (z : ℝ) => z * Real.log z) (conditionalAliceAverage G H y)).PosSemidef

def QuantumParallelRepetition.fullCoordinateBaseWinIndicator {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : ℝ

The indicator function for full coordinate base win.

Equations

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

theorem QuantumParallelRepetition.fullCoordinateBaseWinIndicator_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : 0 ≤ fullCoordinateBaseWinIndicator G D L i r α β

theorem QuantumParallelRepetition.fullCoordinateOldHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (y : Y) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G (fullCoordinateOldHistory D L i r y) α β = fullCoordinateBaseWinIndicator G D L i r α β

theorem QuantumParallelRepetition.fullCoordinateNewHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G (fullCoordinateNewHistory D L i r x) α β = fullCoordinateBaseWinIndicator G D L i r α β

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

theorem QuantumParallelRepetition.fullCoordinateOldHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D L → T) : ∑ h : FullSubsetHistory X Y n D L, f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ y : Y, f (fullCoordinateOldHistory D L i r y)

theorem QuantumParallelRepetition.fullCoordinateNewHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D (insert i L) → T) : ∑ h : FullSubsetHistory X Y n D (insert i L), f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ x : X, f (fullCoordinateNewHistory D L i r x)

theorem QuantumParallelRepetition.fullCoordinateWeightedOldSum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D L → (↥D → A) → (↥D → B) → ℝ) : ∑ h : FullSubsetHistory X Y n D L, ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ y : Y, G.marginalY y * value (fullCoordinateOldHistory D L i r y) α β

theorem QuantumParallelRepetition.fullCoordinateWeightedNewSum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D (insert i L) → (↥D → A) → (↥D → B) → ℝ) : ∑ h : FullSubsetHistory X Y n D (insert i L), ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ x : X, G.marginalX x * value (fullCoordinateNewHistory D L i r x) α β

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

The information increment contributed by full coordinate alice total entropy.

Equations

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

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_increment {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : fullHistoryAliceEntropyPotential G n S D (insert i L) - fullHistoryAliceEntropyPotential G n S D L = fullCoordinateAliceTotalEntropyIncrement G n S D L i

theorem QuantumParallelRepetition.fullCoordinateAliceTotalEntropyIncrement_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : 0 ≤ fullCoordinateAliceTotalEntropyIncrement G n S D L i