Quantum parallel repetition, part 09

theorem QuantumParallelRepetition.gameQuestionX_nonempty {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Nonempty X

theorem QuantumParallelRepetition.gameQuestionY_nonempty {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Nonempty Y

theorem QuantumParallelRepetition.exact_source_equation_twenty_three {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) : ExactSourceClassicalInformationBound G n S D base

theorem QuantumParallelRepetition.exact_source_equation_twenty_seven_support_preserving_unconditional {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) {gamma : ℝ} (gamma_positive : 0 < gamma) : ExactSourceSupportPreservingClassicalSampler G n S D base (exactSourcePinskerRate G n S D) gamma

def QuantumParallelRepetition.ExactSourceOneGameRounding {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) : Prop

The one-coordinate strategy and error data extracted from an exact source.

Equations

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

theorem QuantumParallelRepetition.exact_totalSamplingLoss_mono {K₀ α₁ α₂ η₁ η₂ lam₁ lam₂ : ℝ} (constant_nonnegative : 0 ≤ K₀) (alpha_nonnegative : 0 ≤ α₁) (alpha_le : α₁ ≤ α₂) (eta_nonnegative : 0 ≤ η₁) (eta_le : η₁ ≤ η₂) (lam_le : lam₁ ≤ lam₂) : totalSamplingLoss K₀ α₁ η₁ lam₁ ≤ totalSamplingLoss K₀ α₂ η₂ lam₂

theorem QuantumParallelRepetition.exact_standardQuantumParallelRepetition_of_source_rounding {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) (rounding : ExactSourceOneGameRounding G) : StandardQuantumParallelRepetition G

def QuantumParallelRepetition.unitaryConjugatePOVM {C d : Type} [Fintype C] [Fintype d] [DecidableEq d] (U : ↥(Matrix.unitaryGroup d ℂ)) (P : POVM C d) : POVM C d

The positive operator-valued measurement implementing unitary conjugate.

Equations

• QuantumParallelRepetition.unitaryConjugatePOVM U P = { effect := fun (c : C) => (↑U).conjTranspose * P.effect c * ↑U, positive := ⋯, complete := ⋯ }

theorem QuantumParallelRepetition.residualIdentity_quadratic {s t : Type} [Fintype s] [Fintype t] [DecidableEq s] [DecidableEq t] (M : Matrix s s ℂ) (z : EuclideanSpace ℂ s) (κ : EuclideanSpace ℂ t) (normalized : ‖κ‖ = 1) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1)) (WithLp.toLp 2 fun (q : s × t) => z.ofLp q.1 * κ.ofLp q.2) = quadraticExpectation (Matrix.toEuclideanCLM M) z

@[simp]

theorem QuantumParallelRepetition.exactSourceGlobalCatalystAlicePOVM_effect_global {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (e : ℕ) (a₀ a : A) (x : X) (i j : ExactGlobalHistoryLocalIndex G n S D) (k l : Fin e) : (exactSourceGlobalCatalystAlicePOVM G n S D e a₀ x).effect a (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) i, k)) (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) j, l)) = (exactSourceGlobalAlicePOVM G n S D a₀ x).effect a i j * if k = l then 1 else 0

theorem QuantumParallelRepetition.exactPsi_eq_padded_normalizedPureVector_of_ne_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) (nonzero : exactUnnormalizedPsi G n S D r x y ≠ 0) : exactPsi G n S D r x y = exactPaddedVector G n S D r (normalizedPureVector (exactUnnormalizedPsi G n S D r x y))

def QuantumParallelRepetition.unconditionalMatchedVerifierTensor {s : Type u_1} {t : Type u_2} (target : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : EuclideanSpace ℂ (s × t)

The unconditional matched verifier tensor construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.unconditionalMatchedVerifierTensor target work = WithLp.toLp 2 fun (q : s × t) => target.ofLp q.1 * work.ofLp q.2

theorem QuantumParallelRepetition.unconditionalMatchedVerifierTensor_norm_sq {s : Type u_1} {t : Type u_2} [Fintype s] [Fintype t] (target : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : ‖unconditionalMatchedVerifierTensor target work‖ ^ 2 = ‖target‖ ^ 2 * ‖work‖ ^ 2

theorem QuantumParallelRepetition.unconditionalMatchedVerifierTensor_norm {s : Type u_1} {t : Type u_2} [Fintype s] [Fintype t] (target : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : ‖unconditionalMatchedVerifierTensor target work‖ = ‖target‖ * ‖work‖

theorem QuantumParallelRepetition.unconditionalMatchedVerifierEffect_tensor_complement {s : Type u_1} {t : Type u_2} [DecidableEq s] [DecidableEq t] (effect : Matrix s s ℂ) : 1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) effect 1 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (1 - effect) 1

theorem QuantumParallelRepetition.unconditionalMatchedVerifierEffect_tensor_posSemidef {s : Type u_1} {t : Type u_2} [Finite s] [Finite t] [DecidableEq t] (effect : Matrix s s ℂ) (positive : effect.PosSemidef) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) effect 1).PosSemidef

theorem QuantumParallelRepetition.unconditionalMatchedVerifierEffect_tensor_complement_posSemidef {s : Type u_1} {t : Type u_2} [Finite s] [Finite t] [DecidableEq s] [DecidableEq t] (effect : Matrix s s ℂ) (complement : (1 - effect).PosSemidef) : (1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) effect 1).PosSemidef

theorem QuantumParallelRepetition.unconditionalMatchedVerifierEffect_tensor_quadratic {s : Type u_1} {t : Type u_2} [Fintype s] [Fintype t] [DecidableEq s] [DecidableEq t] (effect : Matrix s s ℂ) (target : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) effect 1)) (unconditionalMatchedVerifierTensor target work) = ‖work‖ ^ 2 * quadraticExpectation (Matrix.toEuclideanCLM effect) target

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalSelectedCopyLocalIndex (B d N m : ℕ) : Type

The type used to represent unconditional selected copy local index in the exact sampling construction.

Equations

• QuantumParallelRepetition.UnconditionalSelectedCopyLocalIndex B d N m = ((_ : Fin B × Fin d) × Fin (N * m))

noncomputable def QuantumParallelRepetition.unconditionalSelectedCopyCleanedStage {d N B m : ℕ} (Q : ℕ) (w : ℝ) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : EuclideanSpace ℂ (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m)

The selected mixed stage after applying its coherent local bucket resets.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSelectedCopyRetainedWork {S N d L : ℕ} {τ : Type u_1} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (rest : EuclideanSpace ℂ τ) : EuclideanSpace ℂ ((Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) × τ)

Tensor the common failure prefix with the work retained after the selected stage.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSelectedCopyCleanedMatchedBranch {S N d L B m : ℕ} {τ : Type u_1} (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (rest : EuclideanSpace ℂ τ) : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m) × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) × τ)

The unconditional selected copy cleaned matched branch construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.unconditionalSelectedCopy_tensor_sub {s : Type u_1} {τ : Type u_2} (x y : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ τ) : unconditionalMatchedVerifierTensor x work - unconditionalMatchedVerifierTensor y work = unconditionalMatchedVerifierTensor (x - y) work

theorem QuantumParallelRepetition.unconditionalSelectedCopy_weightedAffine {ι : Type u_1} [Fintype ι] (weight error asynchronous : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (coefficient residual : ℝ) (pointwise : ∀ (i : ι), error i ≤ coefficient * asynchronous i + residual) : ∑ i : ι, weight i * error i ≤ coefficient * ∑ i : ι, weight i * asynchronous i + residual

theorem QuantumParallelRepetition.unconditionalMatchedVerifierAggregate_dependent_continuity {J : Type u_1} [Fintype J] {H : J → Type u_2} [(j : J) → NormedAddCommGroup (H j)] [(j : J) → InnerProductSpace ℂ (H j)] (weight : J → ℝ) (nonnegative : ∀ (j : J), 0 ≤ weight j) (effect : (j : J) → H j →L[ℂ] H j) (contraction : ∀ (j : J), ‖effect j‖ ≤ 1) (actual ideal : (j : J) → H j) : |∑ j : J, weight j * quadraticExpectation (effect j) (actual j) - ∑ j : J, weight j * quadraticExpectation (effect j) (ideal j)| ≤ (√(∑ j : J, weight j * ‖actual j‖ ^ 2) + √(∑ j : J, weight j * ‖ideal j‖ ^ 2)) * √(∑ j : J, weight j * ‖actual j - ideal j‖ ^ 2)

theorem QuantumParallelRepetition.unconditionalMatchedVerifierAggregate_dependent_le {J : Type u_1} [Fintype J] {H : J → Type u_2} [(j : J) → NormedAddCommGroup (H j)] [(j : J) → InnerProductSpace ℂ (H j)] (weight : J → ℝ) (nonnegative : ∀ (j : J), 0 ≤ weight j) (effect : (j : J) → H j →L[ℂ] H j) (contraction : ∀ (j : J), ‖effect j‖ ≤ 1) (actual ideal : (j : J) → H j) (actual_mass : ∑ j : J, weight j * ‖actual j‖ ^ 2 ≤ 1) (ideal_mass : ∑ j : J, weight j * ‖ideal j‖ ^ 2 ≤ 1) (Δ : ℝ) (deviation : ∑ j : J, weight j * ‖actual j - ideal j‖ ^ 2 ≤ Δ) : |∑ j : J, weight j * quadraticExpectation (effect j) (actual j) - ∑ j : J, weight j * quadraticExpectation (effect j) (ideal j)| ≤ 2 * √Δ

def QuantumParallelRepetition.unconditionalConjugatePureVector {ι : Type u_1} (z : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The state vector representing unconditional conjugate pure.

Equations

• QuantumParallelRepetition.unconditionalConjugatePureVector z = WithLp.toLp 2 fun (i : ι) => star (z.ofLp i)

@[simp]

theorem QuantumParallelRepetition.unconditionalConjugatePureVector_apply {ι : Type u_1} (z : EuclideanSpace ℂ ι) (i : ι) : (unconditionalConjugatePureVector z).ofLp i = star (z.ofLp i)

theorem QuantumParallelRepetition.unconditionalConjugatePureVector_norm_sq {ι : Type u_1} [Fintype ι] (z : EuclideanSpace ℂ ι) : ‖unconditionalConjugatePureVector z‖ ^ 2 = ‖z‖ ^ 2

theorem QuantumParallelRepetition.unconditionalConjugatePureVector_norm {ι : Type u_1} [Fintype ι] (z : EuclideanSpace ℂ ι) : ‖unconditionalConjugatePureVector z‖ = ‖z‖

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

Transpose every effect of a POVM to obtain the conjugate measurement.

Equations

• QuantumParallelRepetition.unconditionalConjugatePOVM P = { effect := fun (a : A) => (P.effect a).transpose, positive := ⋯, complete := ⋯ }

theorem QuantumParallelRepetition.unconditionalConjugatePureVector_transpose_quadratic {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℂ) (z : EuclideanSpace ℂ ι) : quadraticExpectation (Matrix.toEuclideanCLM M.transpose) (unconditionalConjugatePureVector z) = quadraticExpectation (Matrix.toEuclideanCLM M) z

theorem QuantumParallelRepetition.unconditionalPublicBucketPhysicalCoherentTarget_apply {d N B n : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) (φ ψ : Fin B) (i j : Fin d) (a b : Fin (N * n)) : (dSVDensityRationalPublicBucketPhysicalCoherentTargetState w n ξ ζ).ofLp (⟨(φ, i), a⟩, ⟨(ψ, j), b⟩) = (ePRState B).ofLp (φ, ψ) * (↑‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ * dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j) * (↑√↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) * (embezzlementState (N * n)).ofLp (a, b))

theorem QuantumParallelRepetition.unconditionalCanonicalAcceptedCoefficient_sourceScale {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < d) (ξ : BipartiteUnitVector d) (i : Fin d) : √(w * ↑d) * ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ * √↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) = dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i

theorem QuantumParallelRepetition.unconditionalConjugateTranspose_eq_inverse {d : ℕ} (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : (↑(conjugateUnitary U)).transpose = ↑U⁻¹

theorem QuantumParallelRepetition.unconditionalConjugateBobBasisOverlapCancellation {d : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : ↑(unitaryBasisOverlap U V) * (↑(conjugateUnitary V)).transpose = (↑(conjugateUnitary U)).transpose

theorem QuantumParallelRepetition.unconditionalConjugateBobBasisOverlap_sum {d : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (i b : Fin d) : ∑ j : Fin d, ↑(unitaryBasisOverlap U V) i j * star (↑V b j) = star (↑U b i)

theorem QuantumParallelRepetition.unconditionalRationalMixedConjugateBobSpectral_sum {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i b : Fin d) : ∑ j : Fin d, dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j * star (↑(dSVUniformDensityThresholdLeftBobBasis ζ) b j) = star (↑(dSVUniformDensityThresholdLeftBobBasis ξ) b i)

theorem QuantumParallelRepetition.unconditionalConjugateCanonicalAcceptedTarget_apply {d N : ℕ} (w : ℝ) (ξ : BipartiteUnitVector d) (a b : Fin d) : star ((dSVDensityRationalCanonicalAcceptedTarget w N ξ).ofLp (a, b)) = ∑ i : Fin d, ↑(dSVDensityRationalCanonicalAcceptedCoefficient w N ξ i) * star (↑(dSVDensityRationalCanonicalAliceBasis ξ) a i) * star (↑(dSVUniformDensityThresholdLeftBobBasis ξ) b i)

theorem QuantumParallelRepetition.unconditionalMixedConjugateCanonicalAcceptedTarget_sum {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < d) (ξ ζ : BipartiteUnitVector d) (a b : Fin d) : ∑ i : Fin d, ∑ j : Fin d, ↑√(w * ↑d) * ↑‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ * ↑√↑↑(dSVDensityRationalPhysicalAcceptedRank w N ξ i) * star (↑(dSVDensityRationalCanonicalAliceBasis ξ) a i) * dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j * star (↑(dSVUniformDensityThresholdLeftBobBasis ζ) b j) = star ((dSVDensityRationalCanonicalAcceptedTarget w N ξ).ofLp (a, b))

def QuantumParallelRepetition.unconditionalMixedConjugateSigmaAtomLift {d m : ℕ} (B : ℕ) (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) : ↥(Matrix.unitaryGroup ((_ : Fin B × Fin d) × Fin m) ℂ)

The unconditional mixed conjugate sigma atom lift construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.unconditionalMixedConjugateSigmaAtomLift_apply {d m : ℕ} (B : ℕ) (U : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (φ ψ : Fin B) (i j : Fin d) (a b : Fin m) : ↑(unconditionalMixedConjugateSigmaAtomLift B U) ⟨(φ, i), a⟩ ⟨(ψ, j), b⟩ = if φ = ψ ∧ a = b then ↑U i j else 0

theorem QuantumParallelRepetition.unconditionalSelectedCopy_coherentPhaseSigma_norm_sq {H : Type u_1} [Fintype H] {B m : ℕ} (phases : 0 < B) (history : EuclideanSpace ℂ (H × H)) (work : H → H → EuclideanSpace ℂ (Fin m × Fin m)) : ‖dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history fun (x : Fin B) (i j : H) => work i j‖ ^ 2 = ‖dSVUniformDensityCorrectedMatchedSigmaWeightedResidual history work‖ ^ 2

theorem QuantumParallelRepetition.unconditionalSelectedCopy_coherentPhaseConstantWork_norm_sq {H : Type u_1} [Fintype H] {B m : ℕ} (phases : 0 < B) (history : EuclideanSpace ℂ (H × H)) (work : EuclideanSpace ℂ (Fin m × Fin m)) : ‖dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history fun (x : Fin B) (x_1 x_2 : H) => work‖ ^ 2 = ‖history‖ ^ 2 * ‖work‖ ^ 2

theorem QuantumParallelRepetition.unconditionalSelectedCopyCleanedMatchedBranch_norm_sq {S N d L B m : ℕ} {τ : Type u_1} [Fintype τ] (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (Q : ℕ) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (rest : EuclideanSpace ℂ τ) (rest_unit : ‖rest‖ = 1) : ‖unconditionalSelectedCopyCleanedMatchedBranch Q width schedule ξ ζ A C j rest‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j

def QuantumParallelRepetition.unconditionalMixedConjugateSelectedBranchUnitary {ι : Type u_1} {τ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype τ] [DecidableEq τ] (U V : ↥(Matrix.unitaryGroup ι ℂ)) : ↥(Matrix.unitaryGroup ((ι × ι) × τ) ℂ)

The unitary operator implementing unconditional mixed conjugate selected branch.

Equations

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

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

The operator action for unconditional mixed conjugate selected branch local.

Equations

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

theorem QuantumParallelRepetition.unconditionalMixedConjugateSelectedBranch_tensorAction {ι : Type u_1} {τ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype τ] [DecidableEq τ] (U V : ↥(Matrix.unitaryGroup ι ℂ)) (stage : EuclideanSpace ℂ (ι × ι)) (work : EuclideanSpace ℂ τ) : unconditionalMixedConjugateSelectedBranchLocalAction U V (unconditionalMatchedVerifierTensor stage work) = unconditionalMatchedVerifierTensor (WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).mulVec stage.ofLp)) work

theorem QuantumParallelRepetition.unconditionalMixedConjugateSelectedBranch_tensor_smul {s : Type u_1} {τ : Type u_2} (c : ℝ) (stage : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ τ) : c • unconditionalMatchedVerifierTensor stage work = unconditionalMatchedVerifierTensor (c • stage) work

theorem QuantumParallelRepetition.unconditionalPhysicalAcceptedCoherentStage_eq_phaseSigma {d N B m : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) (φ ψ : Fin B) (i j : Fin d) (a b : Fin (N * m)) : (dSVDensityRationalPublicBucketPhysicalCoherentMixedState w m ξ ζ).ofLp (⟨(φ, i), a⟩, ⟨(ψ, j), b⟩) = (ePRState B).ofLp (φ, ψ) * (dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState w m ξ ζ).ofLp (⟨i, a⟩, ⟨j, b⟩)

theorem QuantumParallelRepetition.unconditionalPhysicalAcceptedCoherentStage_apply {d N B m : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) (φ ψ : Fin B) (i j : Fin d) (k l : Fin N) (a b : Fin m) : (dSVDensityRationalPublicBucketPhysicalCoherentMixedState w m ξ ζ).ofLp (⟨(φ, i), finProdFinEquiv (k, a)⟩, ⟨(ψ, j), finProdFinEquiv (l, b)⟩) = (ePRState B).ofLp (φ, ψ) * (dSVDensityRationalCanonicalPrefixSpectralOutcome w N ξ ζ).ofLp (⟨k, i⟩, ⟨l, j⟩) * (embezzlementState m).ofLp (a, b)

def QuantumParallelRepetition.actualStoppingBranchVector {R : Type} {ι κ : R → Type} (z : EuclideanSpace ℂ (((r : R) × ι r) × (s : R) × κ s)) (r s : R) : EuclideanSpace ℂ (ι r × κ s)

The state vector representing actual stopping branch.

Equations

• QuantumParallelRepetition.actualStoppingBranchVector z r s = WithLp.toLp 2 fun (q : ι r × κ s) => z.ofLp (⟨r, q.1⟩, ⟨s, q.2⟩)

def QuantumParallelRepetition.actualStoppingBranchWinningEffect {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {ι κ : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (r s : R) (x : X) (y : Y) : Matrix (ι r × κ s) (ι r × κ s) ℂ

The measurement effect for actual stopping branch winning.

Equations

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

theorem QuantumParallelRepetition.actualStoppingBranchWinningEffect_posSemidef {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {ι κ : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (r s : R) (x : X) (y : Y) : (actualStoppingBranchWinningEffect G PA PB r s x y).PosSemidef

theorem QuantumParallelRepetition.actualStoppingBranchBorn_nonneg {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {ι κ : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (z : EuclideanSpace ℂ (((r : R) × ι r) × (s : R) × κ s)) (r s : R) (x : X) (y : Y) : 0 ≤ quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G PA PB r s x y)) (actualStoppingBranchVector z r s)

theorem QuantumParallelRepetition.unitaryConjugatePOVM_jointEffect {A B d : Type} [Fintype A] [Fintype B] [Fintype d] [DecidableEq d] (U V : ↥(Matrix.unitaryGroup d ℂ)) (P : POVM A d) (Q : POVM B d) (a : A) (b : B) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((unitaryConjugatePOVM U P).effect a) ((unitaryConjugatePOVM V Q).effect b) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) (Q.effect b) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V

def QuantumParallelRepetition.actualStoppingQuestionLocalAction {R : Type} [Fintype R] [DecidableEq R] {ι : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] (U V : ↥(Matrix.unitaryGroup ((r : R) × ι r) ℂ)) (z : EuclideanSpace ℂ (((r : R) × ι r) × (r : R) × ι r)) : EuclideanSpace ℂ (((r : R) × ι r) × (r : R) × ι r)

The operator action for actual stopping question local.

Equations

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

theorem QuantumParallelRepetition.actualStoppingQuestionLocalWinningProbability_eq_sum {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype R] [DecidableEq R] {ι : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (r : R) → Y → POVM B (ι r)) (U : X → ↥(Matrix.unitaryGroup ((r : R) × ι r) ℂ)) (V : Y → ↥(Matrix.unitaryGroup ((r : R) × ι r) ℂ)) (z : EuclideanSpace ℂ (((r : R) × ι r) × (r : R) × ι r)) (normalized : ‖z‖ = 1) : (pureVectorStrategy G z normalized (fun (x : X) => unitaryConjugatePOVM (U x) (dependentBlockPOVM fun (r : R) => PA r x)) fun (y : Y) => unitaryConjugatePOVM (V y) (dependentBlockPOVM fun (r : R) => PB r y)).winProbability = ∑ x : X, ∑ y : Y, G.questionWeight x y * ∑ r : R, ∑ s : R, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G PA PB r s x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (U x) (V y) z) r s)

theorem QuantumParallelRepetition.actualStoppingQuestionLocalWinningProbability_ge_matched {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {L : ℕ} {ι : Fin (L + 1) → Type} [(r : Fin (L + 1)) → Fintype (ι r)] [(r : Fin (L + 1)) → DecidableEq (ι r)] (G : Game X Y A B) (PA : (r : Fin (L + 1)) → X → POVM A (ι r)) (PB : (r : Fin (L + 1)) → Y → POVM B (ι r)) (U : X → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (V : Y → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (z : EuclideanSpace ℂ (((r : Fin (L + 1)) × ι r) × (r : Fin (L + 1)) × ι r)) (normalized : ‖z‖ = 1) : ∑ x : X, ∑ y : Y, G.questionWeight x y * ∑ j : Fin L, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G PA PB j.succ j.succ x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (U x) (V y) z) j.succ j.succ) ≤ (pureVectorStrategy G z normalized (fun (x : X) => unitaryConjugatePOVM (U x) (dependentBlockPOVM fun (r : Fin (L + 1)) => PA r x)) fun (y : Y) => unitaryConjugatePOVM (V y) (dependentBlockPOVM fun (r : Fin (L + 1)) => PB r y)).winProbability

theorem QuantumParallelRepetition.actualStoppingQuestionLocalFlaggedWinningProbability_ge_matched {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {L : ℕ} {J : Type} [Fintype J] [DecidableEq J] {ι : Fin (L + 1) → Type} [(r : Fin (L + 1)) → Fintype (ι r)] [(r : Fin (L + 1)) → DecidableEq (ι r)] (G : Game X Y A B) (weight : J → ℝ) (weight_nonnegative : ∀ (j : J), 0 ≤ weight j) (weight_normalized : ∑ j : J, weight j = 1) (PA : J → (r : Fin (L + 1)) → X → POVM A (ι r)) (PB : J → (r : Fin (L + 1)) → Y → POVM B (ι r)) (U : J → X → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (V : J → Y → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (z : J → EuclideanSpace ℂ (((r : Fin (L + 1)) × ι r) × (r : Fin (L + 1)) × ι r)) (normalized : ∀ (j : J), ‖z j‖ = 1) : ∑ q : J, weight q * ∑ x : X, ∑ y : Y, G.questionWeight x y * ∑ j : Fin L, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G (PA q) (PB q) j.succ j.succ x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (U q x) (V q y) (z q)) j.succ j.succ) ≤ (pureFlaggedStrategy G weight weight_nonnegative weight_normalized z normalized (fun (q : J) (x : X) => unitaryConjugatePOVM (U q x) (dependentBlockPOVM fun (r : Fin (L + 1)) => PA q r x)) fun (q : J) (y : Y) => unitaryConjugatePOVM (V q y) (dependentBlockPOVM fun (r : Fin (L + 1)) => PB q r y)).winProbability

theorem QuantumParallelRepetition.directDSVRemainingCopyProductSplit {M : Type u_1} [CommMonoid M] {L : ℕ} (j : Fin L) (f : Fin L → M) : ∏ i : Fin L, f i = (∏ i : Fin ↑j, f ⟨↑i, ⋯⟩) * ∏ i : Fin (L - ↑j), f ⟨↑j + ↑i, ⋯⟩

@[reducible, inline]

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

The type used to represent unconditional source physical stopping phase fiber in the exact sampling construction.

Equations

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

def QuantumParallelRepetition.unconditionalSourcePhysicalStoppingPhaseHarmonicIndexEquiv (S B N d L m : ℕ) : (DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) × Fin m ≃ (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m

Regroup phase, stopped history, and harmonic indices by their stopping flag.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalStoppingTargetFirstIndexEquiv (S B N d L m : ℕ) : Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) ≃ (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m

Convert the target-first index into stopping flags and their physical fibers.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalStoppingTargetFirstStateEquiv (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)) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) × (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m)

The bipartite isometry induced by the target-first stopping index equivalence.

Equations

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

theorem QuantumParallelRepetition.unconditionalSourcePhysicalStoppingBranch_sigmaContinuation {R κ : Type} [Fintype R] [DecidableEq R] [Fintype κ] [DecidableEq κ] (U V : R → ↥(Matrix.unitaryGroup κ ℂ)) (z : EuclideanSpace ℂ (((_ : R) × κ) × (_ : R) × κ)) (r s : R) : actualStoppingBranchVector (dSVUniformDensityPhysicalAsyncSigmaContinuation U V z) r s = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑(U r) ↑(V s)).mulVec (actualStoppingBranchVector z r s).ofLp)

def QuantumParallelRepetition.unconditionalSourceFixedPureStoppedSigmaReindexedUnitary {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : ↥(Matrix.unitaryGroup ι ℂ)) : ↥(Matrix.unitaryGroup κ ℂ)

Transport a unitary matrix along an equivalence of its row and column indices.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSelectedMultiscalePhaseIndexEquiv {S B : ℕ} (scale : Fin (S + 1)) : Fin B × Fin (Fintype.card (Fin S → Fin B)) ≃ DSVDensityRationalPublicMultiscalePhaseIndex (S + 1) B

Insert the selected phase into the family of phases at all other scales.

Equations

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

theorem QuantumParallelRepetition.unconditionalSelectedMultiscalePhase_card (S B : ℕ) : Fintype.card (DSVDensityRationalPublicMultiscalePhase (S + 1) B) = B * Fintype.card (Fin S → Fin B)

noncomputable def QuantumParallelRepetition.unconditionalActualMultiscalePhaseIndexEquiv {S B : ℕ} (scale : Fin S) : Fin B × Fin (Fintype.card (Fin (S - 1) → Fin B)) ≃ DSVDensityRationalPublicMultiscalePhaseIndex S B

Split the actual phase family into its selected phase and remaining phases.

Equations

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

def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedReindexedUnitary {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : ↥(Matrix.unitaryGroup ι ℂ)) : ↥(Matrix.unitaryGroup κ ℂ)

Reindex a cleaned unitary through an equivalence of its local index spaces.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedTargetFirstUnitary (S B N d L m : ℕ) (U : ↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)) ℂ)) : ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) ℂ)

Transport a target-first unitary to the physical stopping fibers.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedStoppingFixedSource (S B N d L m : ℕ) : EuclideanSpace ℂ (((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) × (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m)

The source object for unconditional source physical cleaned stopping fixed.

Equations

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

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

def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedSelectedHistoryEquiv {L : ℕ} (j : Fin L) (β : Type u_1) : (Fin (L + 1) → β) ≃ β × (Fin ↑j → β) × (Fin (L - ↑j) → β)

Split a history into the selected coordinate, its prefix, and its suffix.

Equations

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

def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedFullLocalIndexEquiv {P : Type u_1} {R : Type u_2} {B N d L m : ℕ} (phaseSplit : P ≃ Fin B × R) (j : Fin L) : (_ : P × (Fin (L + 1) → DSVUniformDensityThresholdLocalIndex N d)) × Fin m ≃ UnconditionalSelectedCopyLocalIndex B d N m × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × R

The finite equivalence encoding unconditional source physical cleaned full local index.

Equations

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

def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedFullBilateralRegroup {R : Type u_1} {B N d L m : ℕ} (j : Fin L) : (UnconditionalSelectedCopyLocalIndex B d N m × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × R) × UnconditionalSelectedCopyLocalIndex B d N m × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × R ≃ (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m) × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) × ((Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d)) × R × R

Group the selected pair together and retain the bilateral prefix and tail indices.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalCleanedFullBilateralStateIsometry {P : Type u_1} {R : Type u_2} [Fintype P] [Fintype R] {B N d L m : ℕ} (phaseSplit : P ≃ Fin B × R) (j : Fin L) : EuclideanSpace ℂ (((_ : P × (Fin (L + 1) → DSVUniformDensityThresholdLocalIndex N d)) × Fin m) × (_ : P × (Fin (L + 1) → DSVUniformDensityThresholdLocalIndex N d)) × Fin m) ≃ₗᵢ[ℂ] EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m) × (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) × ((Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d)) × R × R)

The linear isometry implementing unconditional source physical cleaned full bilateral state.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalActualCleanedSelectedRetainedIndex {N d L : ℕ} (j : Fin L) (R : Type) : Type

Retained local histories before and after the selected stopping stage.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalSourceFlagControlledRetainedIndex {N d L : ℕ} (j : Fin L) (R : Type) : Type

The type used to represent unconditional source flag controlled retained index in the exact sampling construction.

Equations

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

def QuantumParallelRepetition.unconditionalSourceFlagControlledTensorUnitary {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (U : ↥(Matrix.unitaryGroup ι ℂ)) (V : ↥(Matrix.unitaryGroup κ ℂ)) : ↥(Matrix.unitaryGroup (ι × κ) ℂ)

The tensor product of two unitaries acting on paired local indices.

Equations

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

def QuantumParallelRepetition.unconditionalSourceFlagControlledStagePhysicalIndexEquiv (B N d m : ℕ) : (_ : Fin B) × DSVUniformDensityThresholdLocalIndex N d × Fin m ≃ UnconditionalSelectedCopyLocalIndex B d N m

Regroup phase, threshold, spectral, and harmonic indices into the selected-copy index.

Equations

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

def QuantumParallelRepetition.unconditionalSourceFlagControlledStageSpectralUnitary {B N d m : ℕ} (spectral : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)) : ↥(Matrix.unitaryGroup (UnconditionalSelectedCopyLocalIndex B d N m) ℂ)

Apply the spectral unitary at each public phase, retaining the harmonic coordinate.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourceFlagControlledStageBucketUnitary {B N d m : ℕ} (Q : ℕ) (w : ℝ) (ξ : BipartiteUnitVector d) (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : ↥(Matrix.unitaryGroup (UnconditionalSelectedCopyLocalIndex B d N m) ℂ)

Apply the unitary selected by the public phase and the accepted-rank bucket.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourceFlagControlledFullStageUnitary {S B N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex S B ≃ Fin B × R) (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (spectral : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)) (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) : ↥(Matrix.unitaryGroup (UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) ℂ)

The controlled physical unitary at a selected stage of the scheduled source.

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourceFlagControlledFiniteStageDecoder {S B N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex S B ≃ Fin B × R) (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (spectral : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)) (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : Fin (L + 1) → ↥(Matrix.unitaryGroup (UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) ℂ)

The family of controlled decoding unitaries indexed by the stopping flag.

Equations

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

theorem QuantumParallelRepetition.unconditionalActualPhysicalMixedAcceptedSpectralGauge_sum {N d : ℕ} (f : DSVUniformDensityThresholdLocalIndex N d → DSVUniformDensityThresholdLocalIndex N d → ℂ) : ∑ i : Fin d, ∑ k : Fin N, ∑ j : Fin d, ∑ l : Fin N, f ⟨k, i⟩ ⟨l, j⟩ = ∑ x : DSVUniformDensityThresholdLocalIndex N d, ∑ y : DSVUniformDensityThresholdLocalIndex N d, f x y

@[reducible, inline]

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

The type used to represent unconditional actual canonical retained phase index in the exact sampling construction.

Equations

• QuantumParallelRepetition.UnconditionalActualCanonicalRetainedPhaseIndex S B = Fin (Fintype.card (Fin (S - 1) → Fin B))

noncomputable def QuantumParallelRepetition.unconditionalActualCanonicalRetainedPhaseTail {S B N d L : ℕ} (j : Fin L) : EuclideanSpace ℂ (((Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d)) × UnconditionalActualCanonicalRetainedPhaseIndex S B × UnconditionalActualCanonicalRetainedPhaseIndex S B)

The unconditional actual canonical retained phase tail construction used in the quantum parallel-repetition argument.

Equations

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

def QuantumParallelRepetition.directDSVActualReindexedRetainedPOVM {C : Type u_1} {s : Type u_2} {t : Type u_3} {ι : Type u_4} [Fintype C] [Fintype s] [Fintype t] [Fintype ι] [DecidableEq s] [DecidableEq t] [DecidableEq ι] (e : ι ≃ s × t) (P : POVM C s) : POVM C ι

The positive operator-valued measurement implementing direct DSV actual reindexed retained.

Equations

• QuantumParallelRepetition.directDSVActualReindexedRetainedPOVM e P = QuantumParallelRepetition.reindexedPOVM e.symm (QuantumParallelRepetition.purificationAlicePOVM P)

@[simp]

theorem QuantumParallelRepetition.directDSVActualReindexedRetainedPOVM_effect {C : Type u_1} {s : Type u_2} {t : Type u_3} {ι : Type u_4} [Fintype C] [Fintype s] [Fintype t] [Fintype ι] [DecidableEq s] [DecidableEq t] [DecidableEq ι] (e : ι ≃ s × t) (P : POVM C s) (a : C) (i j : ι) : (directDSVActualReindexedRetainedPOVM e P).effect a i j = P.effect a (e i).1 (e j).1 * if (e i).2 = (e j).2 then 1 else 0

def QuantumParallelRepetition.directDSVActualBilateralRetainedIndexEquiv {s : Type u_1} {t : Type u_2} {u : Type u_3} {v : Type u_4} {ι : Type u_5} {κ : Type u_6} (eA : ι ≃ s × t) (eB : κ ≃ u × v) : ι × κ ≃ (s × u) × t × v

The finite equivalence encoding direct DSV actual bilateral retained index.

Equations

• QuantumParallelRepetition.directDSVActualBilateralRetainedIndexEquiv eA eB = (eA.prodCongr eB).trans (Equiv.prodProdProdComm s t u v)

def QuantumParallelRepetition.directDSVActualLocalPOVMWinningEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {s : Type u_5} {t : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype s] [Fintype t] [DecidableEq s] [DecidableEq t] (G : Game X Y A B) (PA : POVM A s) (PB : POVM B t) (x : X) (y : Y) : Matrix (s × t) (s × t) ℂ

The measurement effect for direct DSV actual local POVM winning.

Equations

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

theorem QuantumParallelRepetition.actualStoppingBranchWinningEffect_eq_direct {X Y A B R : Type} {ι κ : R → Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (r s : R) (x : X) (y : Y) : actualStoppingBranchWinningEffect G PA PB r s x y = directDSVActualLocalPOVMWinningEffect G (PA r x) (PB s y) x y

A stopping branch uses the winning effect of its two selected measurements.

theorem QuantumParallelRepetition.directDSVActualReindexedRetainedPOVMWinningEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {s : Type u_5} {t : Type u_6} {u : Type u_7} {v : Type u_8} {ι : Type u_9} {κ : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype s] [Fintype t] [Fintype u] [Fintype v] [Fintype ι] [Fintype κ] [DecidableEq s] [DecidableEq t] [DecidableEq u] [DecidableEq v] [DecidableEq ι] [DecidableEq κ] (G : Game X Y A B) (eA : ι ≃ s × t) (eB : κ ≃ u × v) (PA : POVM A s) (PB : POVM B u) (x : X) (y : Y) : directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA PA) (directDSVActualReindexedRetainedPOVM eB PB) x y = (Matrix.reindex (directDSVActualBilateralRetainedIndexEquiv eA eB).symm (directDSVActualBilateralRetainedIndexEquiv eA eB).symm) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G PA PB x y) 1)

theorem QuantumParallelRepetition.directDSVActualReindexedWinningEffect_quadratic {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (winning : Matrix κ κ ℂ) (z : EuclideanSpace ℂ ι) : quadraticExpectation (Matrix.toEuclideanCLM ((Matrix.reindex e.symm e.symm) winning)) z = quadraticExpectation (Matrix.toEuclideanCLM winning) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) z)

theorem QuantumParallelRepetition.directDSVActualReindexedRetainedPOVMWinningEffect_tensor_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {s : Type u_5} {t : Type u_6} {u : Type u_7} {v : Type u_8} {ι : Type u_9} {κ : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype s] [Fintype t] [Fintype u] [Fintype v] [Fintype ι] [Fintype κ] [DecidableEq s] [DecidableEq t] [DecidableEq u] [DecidableEq v] [DecidableEq ι] [DecidableEq κ] (G : Game X Y A B) (eA : ι ≃ s × t) (eB : κ ≃ u × v) (PA : POVM A s) (PB : POVM B u) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) (target : EuclideanSpace ℂ (s × u)) (work : EuclideanSpace ℂ (t × v)) (selected : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z = unconditionalMatchedVerifierTensor target work) : quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA PA) (directDSVActualReindexedRetainedPOVM eB PB) x y)) z = ‖work‖ ^ 2 * quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G PA PB x y)) target

theorem QuantumParallelRepetition.unconditionalSelectedBranchLocalAction_mul {s : Type u_1} {t : Type u_2} [Fintype s] [DecidableEq s] [Fintype t] [DecidableEq t] (U₁ U₂ V₁ V₂ : ↥(Matrix.unitaryGroup s ℂ)) (z : EuclideanSpace ℂ ((s × s) × t)) : unconditionalMixedConjugateSelectedBranchLocalAction (U₁ * U₂) (V₁ * V₂) z = unconditionalMixedConjugateSelectedBranchLocalAction U₁ V₁ (unconditionalMixedConjugateSelectedBranchLocalAction U₂ V₂ z)

def QuantumParallelRepetition.unconditionalActualFixedSourceRetainedHistoryPairEquiv {N d L : ℕ} {R : Type} (j : Fin L) : UnconditionalActualCleanedSelectedRetainedIndex j R × UnconditionalActualCleanedSelectedRetainedIndex j R ≃ (Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) × ((Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) × (Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d)) × R × R

The finite equivalence encoding unconditional actual fixed source retained history pair.

Equations

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

theorem QuantumParallelRepetition.exactSourceHistoryFlag_nonempty_of_positive {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) : Nonempty (ExactHistoryFlag X Y A B D)

def QuantumParallelRepetition.physical8SelectedGlobalTargetWorkEquiv (P N d m : ℕ) : UnconditionalSelectedCopyLocalIndex P d N m ≃ Fin d × Fin P × Fin (N * m)

The finite equivalence encoding physical 8 selected global target work.

Equations

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

def QuantumParallelRepetition.physical8OneScaleActualGlobalFiberEquiv {P N d L m : ℕ} {R : Type} (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (j : Fin L) : UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m ≃ Fin d × (Fin P × Fin (N * m)) × UnconditionalSourceFlagControlledRetainedIndex j R

The finite equivalence encoding physical 8 one scale actual global fiber.

Equations

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

noncomputable def QuantumParallelRepetition.physical8OneScaleOriginalFlagPOVM {C : Type u_1} {Z : Type u_2} [Fintype C] [DecidableEq C] {P N d L m : ℕ} {R : Type} [Fintype R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (default : C) (sourcePOVM : Z → POVM C (Fin d)) : Fin (L + 1) → Z → POVM C (UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m)

The positive operator-valued measurement implementing physical 8 one scale original flag.

Equations

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

noncomputable def QuantumParallelRepetition.physical8OneScaleActualAliceStoppingUnitary {F : Type u_1} {Z : Type u_2} {P N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (target : F → Z → BipartiteUnitVector d) (cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : F → Z → ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m) ℂ)

The unitary operator implementing physical 8 one scale actual alice stopping.

Equations

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

noncomputable def QuantumParallelRepetition.physical8OneScaleActualBobStoppingUnitary {F : Type u_1} {Z : Type u_2} {P N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (target : F → Z → BipartiteUnitVector d) (cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : F → Z → ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m) ℂ)

The unitary operator implementing physical 8 one scale actual bob stopping.

Equations

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

theorem QuantumParallelRepetition.exactSourceAnswerTypes_nonempty_of_remaining {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) : Nonempty A ∧ Nonempty B

noncomputable def QuantumParallelRepetition.unconditionalActualOneScaleFixedSourcePhaseSplit (P : ℕ) : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × UnconditionalActualCanonicalRetainedPhaseIndex 1 P

The unconditional actual one scale fixed source phase split construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.unconditionalActualOneScaleFixedSourcePhaseSplit P = (QuantumParallelRepetition.unconditionalActualMultiscalePhaseIndexEquiv 0).symm

theorem QuantumParallelRepetition.unconditionalActualOneScalePhysicalQuestionDecodedMatchedBranch {F X Y : Type} {P N d L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (ξ : F → X → BipartiteUnitVector d) (ζ : F → Y → BipartiteUnitVector d) (A C : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (grid : 0 < N) (flag : F) (x : X) (y : Y) (j : Fin L) (positive : 0 < width (schedule j)) : (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (physical8OneScaleActualAliceStoppingUnitary (unconditionalActualOneScaleFixedSourcePhaseSplit P) Q width schedule ξ A flag x) (physical8OneScaleActualBobStoppingUnitary (unconditionalActualOneScaleFixedSourcePhaseSplit P) Q width schedule ζ C flag y) (unconditionalSourcePhysicalCleanedStoppingFixedSource 1 P N d L m)) j.succ j.succ) = unconditionalSelectedCopyCleanedMatchedBranch Q width schedule (ξ flag x) (ζ flag y) A C j (unconditionalActualCanonicalRetainedPhaseTail j)

theorem QuantumParallelRepetition.unconditionalConjugatePureVector_sub_norm {ι : Type u_1} [Fintype ι] (x y : EuclideanSpace ℂ ι) : ‖unconditionalConjugatePureVector x - unconditionalConjugatePureVector y‖ = ‖x - y‖

theorem QuantumParallelRepetition.unconditionalClippedConjugateUnitTarget_distance_sq_le {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (gamma : BipartiteUnitVector d) (psi : EuclideanSpace ℂ (Fin d × Fin d)) : ‖unconditionalConjugatePureVector psi - unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma)‖ ^ 2 ≤ 2 * ‖psi - ↑gamma‖ ^ 2 + 8 * (1 / w + ↑d * w / ↑N)

theorem QuantumParallelRepetition.unconditionalMatchedVerifierTensor_sub_right {s : Type u_1} {t : Type u_2} (x y : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : unconditionalMatchedVerifierTensor x work - unconditionalMatchedVerifierTensor y work = unconditionalMatchedVerifierTensor (x - y) work

theorem QuantumParallelRepetition.unconditionalWeightedClippedConjugateUnitSource_distance_sq_le {J : Type u_1} [Fintype J] {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (weight : J → ℝ) (weight_nonnegative : ∀ (j : J), 0 ≤ weight j) (weight_normalized : ∑ j : J, weight j = 1) (gamma : J → BipartiteUnitVector d) (psi : J → EuclideanSpace ℂ (Fin d × Fin d)) (energy : ℝ) (energy_bound : ∑ j : J, weight j * ‖psi j - ↑(gamma j)‖ ^ 2 ≤ energy) : ∑ j : J, weight j * ‖unconditionalConjugatePureVector (psi j) - unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine (gamma j))‖ ^ 2 ≤ 2 * energy + 8 * (1 / w + ↑d * w / ↑N)

noncomputable def QuantumParallelRepetition.unconditionalExactFairGammaUnit {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (u : ExactLocallySampleableTuple X Y A B D) : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

The unconditional exact fair gamma unit construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.unconditionalExactFairGammaUnit G n S D u = ⟨QuantumParallelRepetition.exactSourceTupleGamma G n S D u, ⋯⟩

theorem QuantumParallelRepetition.unconditionalExactFairGammaUnit_eq_global {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (u : ExactLocallySampleableTuple X Y A B D) : unconditionalExactFairGammaUnit G n S D u = exactGlobalHistoryFinGamma G n S D u.2.2.2 u.2.1

theorem QuantumParallelRepetition.unconditionalCoherentPhaseConstantWork_sub {H : Type u_1} {B m : ℕ} (x y : EuclideanSpace ℂ (H × H)) (work : EuclideanSpace ℂ (Fin m × Fin m)) : ((dSVDensityRationalPublicBucketCoherentPhaseSigmaState B x fun (x : Fin B) (x_1 x_2 : H) => work) - dSVDensityRationalPublicBucketCoherentPhaseSigmaState B y fun (x : Fin B) (x_1 x_2 : H) => work) = dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (x - y) fun (x : Fin B) (x_1 x_2 : H) => work

theorem QuantumParallelRepetition.unconditionalStoppedPhaseHarmonic_distance_sq {H : Type u_1} [Fintype H] {B m : ℕ} (phases : 0 < B) (harmonic : 0 < m) (x y : EuclideanSpace ℂ (H × H)) : ‖(dSVDensityRationalPublicBucketCoherentPhaseSigmaState B x fun (x : Fin B) (x_1 x_2 : H) => embezzlementState m) - dSVDensityRationalPublicBucketCoherentPhaseSigmaState B y fun (x : Fin B) (x_1 x_2 : H) => embezzlementState m‖ ^ 2 = ‖x - y‖ ^ 2

theorem QuantumParallelRepetition.unconditionalStoppedPhaseHarmonicDistance_sum_le {J : Type u_1} {K : Type u_2} [Fintype K] {d B m : ℕ} (phases : 0 < B) (harmonic : 0 < m) (x y : J → EuclideanSpace ℂ (Fin d × Fin d)) {T : J × K → Type u_3} [(p : J × K) → Fintype (T p)] (work : (p : J × K) → EuclideanSpace ℂ (T p)) (work_row : ∀ (j : J), ∑ k : K, ‖work (j, k)‖ ^ 2 ≤ 1) (j : J) : ∑ k : K, ‖unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (x j) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) (work (j, k)) - unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (y j) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) (work (j, k))‖ ^ 2 ≤ ‖x j - y j‖ ^ 2

theorem QuantumParallelRepetition.unconditionalWeightedStoppedPhaseHarmonicClippedUnit_le {J : Type u_1} {K : Type u_2} [Fintype J] [Fintype K] {d N B m : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (phases : 0 < B) (harmonic : 0 < m) (weight : J → ℝ) (weight_nonnegative : ∀ (j : J), 0 ≤ weight j) (weight_normalized : ∑ j : J, weight j = 1) (gamma : J → BipartiteUnitVector d) (psi : J → EuclideanSpace ℂ (Fin d × Fin d)) (energy : ℝ) (energy_bound : ∑ j : J, weight j * ‖psi j - ↑(gamma j)‖ ^ 2 ≤ energy) {T : J × K → Type u_3} [(p : J × K) → Fintype (T p)] (work : (p : J × K) → EuclideanSpace ℂ (T p)) (work_row : ∀ (j : J), ∑ k : K, ‖work (j, k)‖ ^ 2 ≤ 1) : ∑ j : J, weight j * ∑ k : K, ‖unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector (psi j)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) (work (j, k)) - unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine (gamma j))) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) (work (j, k))‖ ^ 2 ≤ 2 * energy + 8 * (1 / w + ↑d * w / ↑N)

theorem QuantumParallelRepetition.unconditionalExactFairStoppedPhaseHarmonicClippedUnit_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 : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) {w : ℝ} {N P m : ℕ} (width : 0 < w) (grid : 0 < N) (fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1)) (phases : 0 < P) (harmonic : 0 < m) {K : Type u_5} [Fintype K] {T : ExactLocallySampleableTuple X Y A B D × K → Type u_6} [(p : ExactLocallySampleableTuple X Y A B D × K) → Fintype (T p)] (work : (p : ExactLocallySampleableTuple X Y A B D × K) → EuclideanSpace ℂ (T p)) (work_row : ∀ (u : ExactLocallySampleableTuple X Y A B D), ∑ k : K, ‖work (u, k)‖ ^ 2 ≤ 1) : ∑ u : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D u * ∑ k : K, ‖unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState P (unconditionalConjugatePureVector (exactSourceTuplePsi G n S D u)) fun (x : Fin P) (x_1 x_2 : Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))) => embezzlementState m) (work (u, k)) - unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState P (unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine (unconditionalExactFairGammaUnit G n S D u))) fun (x : Fin P) (x_1 x_2 : Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))) => embezzlementState m) (work (u, k))‖ ^ 2 ≤ 16 * martingaleRate G n S D + 8 * (1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N)

theorem QuantumParallelRepetition.unconditionalCanonicalRaw_eq_norm_smul_unit {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (gamma : BipartiteUnitVector d) : dSVDensityRationalCanonicalAcceptedTarget w N gamma = ‖dSVDensityRationalCanonicalAcceptedTarget w N gamma‖ • ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma)

theorem QuantumParallelRepetition.unconditionalConjugateCanonicalRaw_eq_norm_smul_unit {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (gamma : BipartiteUnitVector d) : unconditionalConjugatePureVector (dSVDensityRationalCanonicalAcceptedTarget w N gamma) = ‖dSVDensityRationalCanonicalAcceptedTarget w N gamma‖ • unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma)

theorem QuantumParallelRepetition.unconditionalPhaseCanonicalRaw_eq_norm_smul_unit {d N B m : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (w + 1)) (gamma : BipartiteUnitVector d) : (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector (dSVDensityRationalCanonicalAcceptedTarget w N gamma)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) = ‖dSVDensityRationalCanonicalAcceptedTarget w N gamma‖ • dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m

theorem QuantumParallelRepetition.unconditionalMatchedTensor_real_smul_work {s : Type u_1} {t : Type u_2} (c : ℝ) (stage : EuclideanSpace ℂ s) (work : EuclideanSpace ℂ t) : c • unconditionalMatchedVerifierTensor stage work = unconditionalMatchedVerifierTensor stage (c • work)

theorem QuantumParallelRepetition.unconditionalPhaseCanonical_sourceScale_absorbed {d N B m : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < d) (fine : ↑d / ↑N < 1 / (w + 1)) (gamma : BipartiteUnitVector d) {T : Type u_1} (work : EuclideanSpace ℂ T) : √(w * ↑d) • unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget width grid fine gamma)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) ((‖dSVDensityRationalCanonicalAcceptedTarget w N gamma‖ / √(w * ↑d)) • work) = unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector (dSVDensityRationalCanonicalAcceptedTarget w N gamma)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState m) work

theorem QuantumParallelRepetition.unconditionalCanonicalAcceptedScale_sq_eq_diagonalBorn {d N : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < d) (gamma : BipartiteUnitVector d) : (‖dSVDensityRationalCanonicalAcceptedTarget w N gamma‖ / √(w * ↑d)) ^ 2 = dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w gamma

theorem QuantumParallelRepetition.integratorActualCanonicalRetainedPhaseTail_norm {S B N d L : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (j : Fin L) : ‖unconditionalActualCanonicalRetainedPhaseTail j‖ = 1

@[reducible, inline]

abbrev QuantumParallelRepetition.IntegratorActualC485TailIndex (S B N d L : ℕ) (j : Fin L) : Type

The type used to represent integrator actual c 485 tail index in the exact sampling construction.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.IntegratorActualC485RetainedIndex (S B N d L : ℕ) (j : Fin L) : Type

The type used to represent integrator actual c 485 retained index in the exact sampling construction.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.IntegratorActualC485BranchSpace (S B N d L m : ℕ) (j : Fin L) : Type

The type used to represent integrator actual c 485 branch space in the exact sampling construction.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485OriginalRetainedWork {S B N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : EuclideanSpace ℂ (IntegratorActualC485RetainedIndex S B N d L j)

The original retained prefix and canonical phase tail at the selected stage.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485NormalizedDiagonalWork {S B N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : EuclideanSpace ℂ (IntegratorActualC485RetainedIndex S B N d L j)

The integrator actual c 485 normalized diagonal work construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485CleanedVector {S B N d L m : ℕ} (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) : IntegratorActualC485BranchSpace S B N d L m j

The state vector representing integrator actual c 485 cleaned.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485CanonicalVector {S B N d L m : ℕ} {width : Fin S → ℝ} (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (positive : 0 < width (schedule j)) (grid : 0 < N) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : IntegratorActualC485BranchSpace S B N d L m j

The state vector representing integrator actual c 485 canonical.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485SourceVector {S B N d L m : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (ψ : EuclideanSpace ℂ (Fin d × Fin d)) (j : Fin L) : IntegratorActualC485BranchSpace S B N d L m j

The state vector representing integrator actual c 485 source.

Equations

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

theorem QuantumParallelRepetition.unconditionalActualC485NormalizedDiagonalWork_mass_sum_le_one {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ∑ j : Fin L, ‖integratorActualC485NormalizedDiagonalWork width schedule ξ ζ j‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualSelectedBranchLocalAction_decidableEq_irrel {ι : Type u_1} {τ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype τ] (left right : DecidableEq τ) (U V : ↥(Matrix.unitaryGroup ι ℂ)) (z : EuclideanSpace ℂ ((ι × ι) × τ)) : unconditionalMixedConjugateSelectedBranchLocalAction U V z = unconditionalMixedConjugateSelectedBranchLocalAction U V z

theorem QuantumParallelRepetition.unconditionalActualSelectedBranchLocalAction_norm {ι : Type u_1} {τ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype τ] [DecidableEq τ] (U V : ↥(Matrix.unitaryGroup ι ℂ)) (z : EuclideanSpace ℂ ((ι × ι) × τ)) : ‖unconditionalMixedConjugateSelectedBranchLocalAction U V z‖ = ‖z‖

theorem QuantumParallelRepetition.unconditionalActualSelectedBranchLocalAction_sub {ι : Type u_1} {τ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype τ] [DecidableEq τ] (U V : ↥(Matrix.unitaryGroup ι ℂ)) (x y : EuclideanSpace ℂ ((ι × ι) × τ)) : unconditionalMixedConjugateSelectedBranchLocalAction U V x - unconditionalMixedConjugateSelectedBranchLocalAction U V y = unconditionalMixedConjugateSelectedBranchLocalAction U V (x - y)

theorem QuantumParallelRepetition.unconditionalActualC485CleanDeviation_sq {S B N d L m : ℕ} (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (positive : 0 < width (schedule j)) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j - integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousCommonStopGaugeStageError Q (width (schedule j)) m ξ ζ A C

theorem QuantumParallelRepetition.unconditionalActualC485CleanDeviation_eq_hazard {S B N d L m : ℕ} (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (positive : ∀ (s : Fin S), 0 < width s) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1)) : ∑ j : Fin L, ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j - integratorActualC485CanonicalVector schedule ξ ζ j ⋯ grid ⋯‖ ^ 2 = dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m width schedule ξ ζ A C

theorem QuantumParallelRepetition.unconditionalActualC485WeightedCleanDeviation_eq_hazard {ι : Type u_1} [Fintype ι] {S B N d L m : ℕ} (law : ι → ℝ) (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : ι → BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (positive : ∀ (s : Fin S), 0 < width s) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1)) : ∑ u : ι, law u * ∑ j : Fin L, ‖integratorActualC485CleanedVector Q width schedule (ξ u) (ζ u) A C j - integratorActualC485CanonicalVector schedule (ξ u) (ζ u) j ⋯ grid ⋯‖ ^ 2 = ∑ u : ι, law u * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m width schedule (ξ u) (ζ u) A C

theorem QuantumParallelRepetition.unconditionalFairMatchedFlag_history_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (matched : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) : exactSourceAlicePermutationHistory D denominator numerator nonempty flag x = exactSourceBobPermutationHistory D denominator numerator nonempty flag y

theorem QuantumParallelRepetition.unconditionalFairMatchedFlag_bobTarget_eq_aliceSample {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (matched : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) : exactGlobalHistoryFinPhi G n S D (exactSourceBobPermutationHistory D denominator numerator nonempty flag y) y = exactGlobalHistoryFinPhi G n S D (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)).2.2.2 y

theorem QuantumParallelRepetition.unconditionalFairMatchedFlag_aliceTarget_eq_aliceSample {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) : exactGlobalHistoryFinGamma G n S D (exactSourceAlicePermutationHistory D denominator numerator nonempty flag x) x = exactGlobalHistoryFinGamma G n S D (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)).2.2.2 x

theorem QuantumParallelRepetition.unconditionalActualOneScaleDecodedMatchedCleanedVector {F X Y : Type} {P N d L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (ξ : F → X → BipartiteUnitVector d) (ζ : F → Y → BipartiteUnitVector d) (A C : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (grid : 0 < N) (flag : F) (x : X) (y : Y) (j : Fin L) (positive : 0 < width (schedule j)) : unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis (ξ flag x)))) (unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis (ζ flag y)))) ((unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (physical8OneScaleActualAliceStoppingUnitary (unconditionalActualOneScaleFixedSourcePhaseSplit P) Q width schedule ξ A flag x) (physical8OneScaleActualBobStoppingUnitary (unconditionalActualOneScaleFixedSourcePhaseSplit P) Q width schedule ζ C flag y) (unconditionalSourcePhysicalCleanedStoppingFixedSource 1 P N d L m)) j.succ j.succ)) = integratorActualC485CleanedVector Q width schedule (ξ flag x) (ζ flag y) A C j

noncomputable def QuantumParallelRepetition.integratorActualC485SourceAlicePOVM {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (a₀ : A) (x : X) : POVM A (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)))

The positive operator-valued measurement implementing integrator actual c 485 source alice.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485SourceBobPOVM {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (b₀ : B) (y : Y) : POVM B (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)))

The positive operator-valued measurement implementing integrator actual c 485 source bob.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485SelectedAlicePOVM {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (a₀ : A) (P N m : ℕ) (x : X) : POVM A (UnconditionalSelectedCopyLocalIndex P (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) N m)

The positive operator-valued measurement implementing integrator actual c 485 selected alice.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485SelectedBobPOVM {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (b₀ : B) (P N m : ℕ) (y : Y) : POVM B (UnconditionalSelectedCopyLocalIndex P (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) N m)

The positive operator-valued measurement implementing integrator actual c 485 selected bob.

Equations

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

noncomputable def QuantumParallelRepetition.integratorActualC485WinningEffect {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (a₀ : A) (b₀ : B) {P N L m : ℕ} (j : Fin L) (x : X) (y : Y) : IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j →L[ℂ] IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j

The measurement effect for integrator actual c 485 winning.

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFairSourceEmbezzlementOne_apply : (embezzlementState 1).ofLp (0, 0) = 1

theorem QuantumParallelRepetition.unconditionalActualFairSourceTensorEmbezzlementOne_reindex {d : ℕ} (ξ : BipartiteUnitVector d) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((finCongr ⋯).prodCongr (finCongr ⋯))) (tensorEmbezzlementTarget ξ) = ↑ξ

theorem QuantumParallelRepetition.unconditionalActualFairSourceConjugateTensorEmbezzlementOne_inverse_reindex {d : ℕ} (ξ : BipartiteUnitVector d) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((finCongr ⋯).symm.prodCongr (finCongr ⋯).symm)) (unconditionalConjugatePureVector ↑ξ) = unconditionalConjugatePureVector (tensorEmbezzlementTarget ξ)

theorem QuantumParallelRepetition.unconditionalActualFairSourceEOneReindexedGlobalWinningBorn {d : ℕ} (winning : Matrix (Fin (d * 1) × Fin (d * 1)) (Fin (d * 1) × Fin (d * 1)) ℂ) (ξ : BipartiteUnitVector d) : quadraticExpectation (Matrix.toEuclideanCLM ((Matrix.reindex ((finCongr ⋯).prodCongr (finCongr ⋯)) ((finCongr ⋯).prodCongr (finCongr ⋯))) winning)) (unconditionalConjugatePureVector ↑ξ) = quadraticExpectation (Matrix.toEuclideanCLM winning) (unconditionalConjugatePureVector (tensorEmbezzlementTarget ξ))

theorem QuantumParallelRepetition.unconditionalActualFairSourceSupportedBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (a₀ : A) (b₀ : B) (h : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D h ≠ 0) {P N L m : ℕ} (phases : 0 < P) (grid : 0 < N) (harmonic : 0 < m) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (j : Fin L) : quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (integratorActualC485SourceVector width schedule (exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1) (exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) (exactSourceTuplePsi G n S D h) j) = ‖integratorActualC485SourceVector width schedule (exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1) (exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) (exactSourceTuplePsi G n S D h) j‖ ^ 2 * exactSourceConditionalWinningProbability G n S D h