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)

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

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

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

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

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

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

Equations

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

noncomputable def QuantumParallelRepetition.physical8OneScaleActualSourceFlaggedStrategy {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) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (w : ℝ) (N L P Q m : ℕ) (phases : 0 < P) (grid : 0 < N) (harmonic : 0 < m) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : Strategy G

Equations

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

@[reducible, inline]

noncomputable abbrev QuantumParallelRepetition.unconditionalOneScaleActualSourceFlaggedStrategy {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) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (w : ℝ) (N L P Q m : ℕ) (phases : 0 < P) (grid : 0 < N) (harmonic : 0 < m) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : Strategy G

Equations

• @QuantumParallelRepetition.unconditionalOneScaleActualSourceFlaggedStrategy = @QuantumParallelRepetition.physical8OneScaleActualSourceFlaggedStrategy

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

Equations

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

theorem QuantumParallelRepetition.unconditionalActualOneScaleFlagControlledFiniteStageDecoder_eq {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)) ℂ)) : unconditionalSourceFlagControlledFiniteStageDecoder phaseSplit Q width schedule ξ spectral A = unconditionalActualCleanedSelectedFiniteStageDecoder phaseSplit Q width schedule ξ spectral A

noncomputable def QuantumParallelRepetition.unconditionalActualOneScaleFixedSourceDecodedState {P N d L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (ξ ζ : BipartiteUnitVector d) (A C : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : EuclideanSpace ℂ (((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m) × (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m)

Equations

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

theorem QuantumParallelRepetition.unconditionalActualOneScaleFixedSourcePhysicalQuestionAction {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)) ℂ)) (flag : F) (x : X) (y : Y) : 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) = unconditionalActualOneScaleFixedSourceDecodedState Q width schedule (ξ flag x) (ζ flag y) A C

theorem QuantumParallelRepetition.unconditionalActualOneScaleFixedSourceDecodedMatchedBranch {P N d L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (ξ ζ : BipartiteUnitVector d) (A C : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (positive : 0 < width (schedule j)) (grid : 0 < N) : (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (actualStoppingBranchVector (unconditionalActualOneScaleFixedSourceDecodedState Q width schedule ξ ζ A C) j.succ j.succ) = unconditionalSelectedCopyCleanedMatchedBranch Q width schedule ξ ζ A C j (unconditionalActualCanonicalRetainedPhaseTail j)

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} [Fintype s] [Fintype t] (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))

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} [Fintype H] {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} [Fintype s] [Fintype t] (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} [Fintype T] (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.unconditionalNormalizedCanonicalRetainedWork_norm_sq {S N d L B m : ℕ} {T : Type u_1} [Fintype T] (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (gamma phi : BipartiteUnitVector d) (j : Fin L) (rest : EuclideanSpace ℂ T) (rest_unit : ‖rest‖ = 1) : ‖(‖dSVDensityRationalCanonicalAcceptedTarget (width (schedule j)) N gamma‖ / √(width (schedule j) * ↑d)) • unconditionalSelectedCopyRetainedWork width schedule gamma phi j rest‖ ^ 2 = ‖unconditionalSelectedCopyIdealMatchedBranch width schedule gamma phi j rest‖ ^ 2

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

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

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

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)

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)

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

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

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

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.unconditionalActualC485CanonicalCorrectedIdeal_generic {S N d L B m : ℕ} {T : Type u_1} [Fintype T] [DecidableEq T] {width : Fin S → ℝ} (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (positive : 0 < width (schedule j)) (grid : 0 < N) (dimension : 0 < d) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) (rest : EuclideanSpace ℂ T) : unconditionalMatchedVerifierTensor (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B (unconditionalConjugatePureVector ↑(dSVDensityRationalCanonicalAcceptedUnitTarget positive grid fine ξ)) fun (x : Fin B) (x_1 x_2 : Fin d) => embezzlementState (N * m)) ((‖dSVDensityRationalCanonicalAcceptedTarget (width (schedule j)) N ξ‖ / √(width (schedule j) * ↑d)) • unconditionalSelectedCopyRetainedWork width schedule ξ ζ j rest) = unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis ξ))) (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis ζ))) (unconditionalSelectedCopyIdealMatchedBranch width schedule ξ ζ j rest)

theorem QuantumParallelRepetition.unconditionalActualC485CanonicalVector_eq_correctedIdeal {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) (dimension : 0 < d) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine = unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis ξ))) (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis ζ))) (unconditionalSelectedCopyIdealMatchedBranch width schedule ξ ζ j (unconditionalActualCanonicalRetainedPhaseTail j))

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

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

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)

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)

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

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.unconditionalActualFairSourceWinningEffect_reindex {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [decA : DecidableEq A] [decB : DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (a₀ : A) (b₀ : B) (x : X) (y : Y) : directDSVActualLocalPOVMWinningEffect G (integratorActualC485SourceAlicePOVM G n S D a₀ x) (integratorActualC485SourceBobPOVM G n S D b₀ y) x y = (Matrix.reindex ((finCongr ⋯).prodCongr (finCongr ⋯)) ((finCongr ⋯).prodCongr (finCongr ⋯))) (unconditionalConjugateSourceGlobalCatalystWinningEffect G n S D 1 a₀ b₀ x y)

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceBaseWinningCLM {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) (x : X) (y : Y) : ExactSourceGlobalState G n S D →L[ℂ] ExactSourceGlobalState G n S D

Equations

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

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.unconditionalActualFairSourceBaseSupportedBorn {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) : quadraticExpectation (unconditionalActualFairSourceBaseWinningCLM G n S D a₀ b₀ h.2.1 h.2.2.1) (unconditionalConjugatePureVector (exactSourceTuplePsi G n S D h)) = exactSourceConditionalWinningProbability G n S D h

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourcePhaseHarmonicWork (P k : ℕ) : EuclideanSpace ℂ ((Fin P × Fin k) × Fin P × Fin k)

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFairSourcePhaseHarmonicWork_norm {P k : ℕ} (phases : 0 < P) (harmonic : 0 < k) : ‖unconditionalActualFairSourcePhaseHarmonicWork P k‖ = 1

theorem QuantumParallelRepetition.unconditionalActualFairSourcePhaseHarmonicStage_sourceProduct {P N d m : ℕ} (ψ : EuclideanSpace ℂ (Fin d × Fin d)) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv (physical8SelectedGlobalTargetWorkEquiv P N d m) (physical8SelectedGlobalTargetWorkEquiv P N d m))) (dSVDensityRationalPublicBucketCoherentPhaseSigmaState P (unconditionalConjugatePureVector ψ) fun (x : Fin P) (x_1 x_2 : Fin d) => embezzlementState (N * m)) = unconditionalMatchedVerifierTensor (unconditionalConjugatePureVector ψ) (unconditionalActualFairSourcePhaseHarmonicWork P (N * m))

theorem QuantumParallelRepetition.unconditionalActualFairSourceSelectedBorn_of_base {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 m : ℕ} (phases : 0 < P) (grid : 0 < N) (harmonic : 0 < m) (x : X) (y : Y) (ψ : EuclideanSpace ℂ (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) × Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)))) (value : ℝ) (base_born : quadraticExpectation (unconditionalActualFairSourceBaseWinningCLM G n S D a₀ b₀ x y) (unconditionalConjugatePureVector ψ) = value) : quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (integratorActualC485SelectedAlicePOVM G n S D a₀ P N m x) (integratorActualC485SelectedBobPOVM G n S D b₀ P N m y) x y)) (dSVDensityRationalPublicBucketCoherentPhaseSigmaState P (unconditionalConjugatePureVector ψ) fun (x : Fin P) (x_1 x_2 : Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))) => embezzlementState (N * m)) = value

theorem QuantumParallelRepetition.unconditionalActualFairSourceOuterBorn_of_base {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 : ℕ} (phases : 0 < P) (grid : 0 < N) (harmonic : 0 < m) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (ξ ζ : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))) (ψ : EuclideanSpace ℂ (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) × Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)))) (ψ_unit : ‖ψ‖ = 1) (j : Fin L) (x : X) (y : Y) (value : ℝ) (base_born : quadraticExpectation (unconditionalActualFairSourceBaseWinningCLM G n S D a₀ b₀ x y) (unconditionalConjugatePureVector ψ) = value) : quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j x y) (integratorActualC485SourceVector width schedule ξ ζ ψ j) = ‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ ^ 2 * value

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

theorem QuantumParallelRepetition.unconditionalActualRetainedPOVM_ext {C : Type u_1} {ι : Type u_2} [Fintype C] [Fintype ι] [DecidableEq ι] (P Q : POVM C ι) (same : ∀ (a : C) (i j : ι), P.effect a i j = Q.effect a i j) : P = Q

theorem QuantumParallelRepetition.unconditionalPhysicalOneScaleActualGlobalFiberPOVM_nested {C : Type u_1} [Fintype C] {P N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (j : Fin L) (source : POVM C (Fin d)) : directDSVActualReindexedRetainedPOVM (physical8OneScaleActualGlobalFiberEquiv phaseSplit j) source = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phaseSplit j) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)

theorem QuantumParallelRepetition.unconditionalPhysicalOneScaleOriginalFlagPOVM_succ_nested {C : Type u_1} {Z : Type u_2} [Fintype C] [DecidableEq C] {P N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R) (default : C) (source : Z → POVM C (Fin d)) (j : Fin L) (x : Z) : physical8OneScaleOriginalFlagPOVM phaseSplit default source j.succ x = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phaseSplit j) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (source x))

theorem QuantumParallelRepetition.unconditionalSelectedGaugeRetainedPOVMNaturality_effect {C : Type} [Fintype C] {P N d m : ℕ} (basis : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (source : POVM C (Fin d)) (a : C) : (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM basis source)).effect a = (unitaryConjugatePOVM (unconditionalMixedConjugateSigmaAtomLift P basis) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)).effect a

theorem QuantumParallelRepetition.unconditionalSelectedGaugeRetainedPOVMNaturality {C : Type} [Fintype C] {P N d m : ℕ} (basis : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (source : POVM C (Fin d)) : directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM basis source) = unitaryConjugatePOVM (unconditionalMixedConjugateSigmaAtomLift P basis) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)

theorem QuantumParallelRepetition.unconditionalActualFairSourceSelectedRetainedWinningEffectGauge {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (x : X) (y : Y) : have e := physical8SelectedGlobalTargetWorkEquiv P N d m; have U := unconditionalMixedConjugateSigmaAtomLift P alice; have V := unconditionalMixedConjugateSigmaAtomLift P bob; directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM alice PA)) (directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM bob PB)) x y = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).conjTranspose * directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e PA) (directDSVActualReindexedRetainedPOVM e PB) x y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V

theorem QuantumParallelRepetition.unconditionalActualFairSourceSelectedRetainedWinningBornGauge {X Y A B τ : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype τ] [DecidableEq τ] {P N d m : ℕ} (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (x : X) (y : Y) (z : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × τ)) : have e := physical8SelectedGlobalTargetWorkEquiv P N d m; have U := unconditionalMixedConjugateSigmaAtomLift P alice; have V := unconditionalMixedConjugateSigmaAtomLift P bob; quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM alice PA)) (directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM bob PB)) x y) 1)) z = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e PA) (directDSVActualReindexedRetainedPOVM e PB) x y) 1)) (unconditionalMixedConjugateSelectedBranchLocalAction U V z)

theorem QuantumParallelRepetition.unconditionalActualC485RetainedPureWorkReindexBorn {s t v : Type} [Fintype s] [DecidableEq s] [Fintype t] [DecidableEq t] [Fintype v] [DecidableEq v] (e : t ≃ v) (winning : Matrix s s ℂ) (z : EuclideanSpace ℂ (s × t)) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) winning 1)) z = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) winning 1)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl s).prodCongr e)) z)

def QuantumParallelRepetition.unconditionalActualC485RetainedHistoryPairEquiv {P N d L : ℕ} (j : Fin L) : UnconditionalSourceFlagControlledRetainedIndex j (UnconditionalActualCanonicalRetainedPhaseIndex 1 P) × UnconditionalSourceFlagControlledRetainedIndex j (UnconditionalActualCanonicalRetainedPhaseIndex 1 P) ≃ IntegratorActualC485RetainedIndex 1 P N d L j

Equations

• QuantumParallelRepetition.unconditionalActualC485RetainedHistoryPairEquiv j = QuantumParallelRepetition.unconditionalActualFixedSourceRetainedHistoryPairEquiv j

theorem QuantumParallelRepetition.unconditionalActualC485FullBilateralWorkRegroup {P N d L m : ℕ} (j : Fin L) (z : EuclideanSpace ℂ (UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m)) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr (unconditionalActualC485RetainedHistoryPairEquiv j))) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P) j))) z) = (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) z

theorem QuantumParallelRepetition.unconditionalWeightedClippedMatchedVerifierAndMassLoss {I : Type u_1} {K : Type u_2} [Fintype I] [Fintype K] (weight : I → ℝ) (weight_nonnegative : ∀ (i : I), 0 ≤ weight i) (weight_normalized : ∑ i : I, weight i = 1) (win : I → ℝ) (win_bounded : ∀ (i : I), win i ≤ 1) {H : I × K → Type u_3} [(p : I × K) → NormedAddCommGroup (H p)] [(p : I × K) → InnerProductSpace ℂ (H p)] (effect : (p : I × K) → H p →L[ℂ] H p) (contraction : ∀ (p : I × K), ‖effect p‖ ≤ 1) (actual canonical source : (p : I × K) → H p) (actual_mass : ∑ i : I, weight i * ∑ k : K, ‖actual (i, k)‖ ^ 2 ≤ 1) (canonical_mass : ∑ i : I, weight i * ∑ k : K, ‖canonical (i, k)‖ ^ 2 ≤ 1) (canonical_row_mass : ∀ (i : I), ∑ k : K, ‖canonical (i, k)‖ ^ 2 ≤ 1) (same_work_mass : ∀ (i : I) (k : K), ‖source (i, k)‖ = ‖canonical (i, k)‖) (supported_born : ∀ (i : I), weight i ≠ 0 → ∀ (k : K), quadraticExpectation (effect (i, k)) (source (i, k)) = ‖source (i, k)‖ ^ 2 * win i) (Δclean Δclip bad : ℝ) (clean_deviation : ∑ i : I, weight i * ∑ k : K, ‖actual (i, k) - canonical (i, k)‖ ^ 2 ≤ Δclean) (clip_deviation : ∑ i : I, weight i * ∑ k : K, ‖canonical (i, k) - source (i, k)‖ ^ 2 ≤ Δclip) (actual_success : 1 - bad ≤ ∑ i : I, weight i * ∑ k : K, ‖actual (i, k)‖ ^ 2) : ∑ i : I, weight i * win i - bad - 4 * √Δclean - 2 * √Δclip ≤ ∑ i : I, weight i * ∑ k : K, quadraticExpectation (effect (i, k)) (actual (i, k))

theorem QuantumParallelRepetition.unconditionalFairPhysicalFlaggedStoppingTransfer {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) (denominator : ℕ) (denominator_positive : 0 < denominator) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (rational_normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (support_preserving : ∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D), 0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history → 0 < numerator index history) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) {L : ℕ} {ι : Fin (L + 1) → Type} [(r : Fin (L + 1)) → Fintype (ι r)] [(r : Fin (L + 1)) → DecidableEq (ι r)] (PA : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → X → POVM A (ι r)) (PB : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → Y → POVM B (ι r)) (U : ExactSourceSharedFlag X Y A B D denominator → X → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (V : ExactSourceSharedFlag X Y A B D denominator → Y → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (z : ExactSourceSharedFlag X Y A B D denominator → EuclideanSpace ℂ (((r : Fin (L + 1)) × ι r) × (r : Fin (L + 1)) × ι r)) (z_normalized : ∀ (flag : ExactSourceSharedFlag X Y A B D denominator), ‖z flag‖ = 1) (matched : ExactSourceSharedFlag X Y A B D denominator × X × Y → Bool) {K : Type u_1} [Fintype K] {H : ExactLocallySampleableTuple X Y A B D × K → Type u_2} [(p : ExactLocallySampleableTuple X Y A B D × K) → NormedAddCommGroup (H p)] [(p : ExactLocallySampleableTuple X Y A B D × K) → InnerProductSpace ℂ (H p)] (effect : (p : ExactLocallySampleableTuple X Y A B D × K) → H p →L[ℂ] H p) (contraction : ∀ (p : ExactLocallySampleableTuple X Y A B D × K), ‖effect p‖ ≤ 1) (actual canonical source : (p : ExactLocallySampleableTuple X Y A B D × K) → H p) (actual_mass : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k)‖ ^ 2 ≤ 1) (canonical_mass : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖canonical (h, k)‖ ^ 2 ≤ 1) (canonical_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ k : K, ‖canonical (h, k)‖ ^ 2 ≤ 1) (same_work_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D) (k : K), ‖source (h, k)‖ = ‖canonical (h, k)‖) (supported_born : ∀ (h : ExactLocallySampleableTuple X Y A B D), exactLocallySampleableLaw G n S D h ≠ 0 → ∀ (k : K), quadraticExpectation (effect (h, k)) (source (h, k)) = ‖source (h, k)‖ ^ 2 * exactSourceConditionalWinningProbability G n S D h) (epsilon lam deviation clipping bad : ℝ) (clean_deviation : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k) - canonical (h, k)‖ ^ 2 ≤ deviation) (clip_deviation : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖canonical (h, k) - source (h, k)‖ ^ 2 ≤ clipping) (actual_success : 1 - bad ≤ ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k)‖ ^ 2) (history_born_nonnegative : ∀ (h : ExactLocallySampleableTuple X Y A B D), 0 ≤ ∑ k : K, quadraticExpectation (effect (h, k)) (actual (h, k))) (history_born_bounded : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ k : K, quadraticExpectation (effect (h, k)) (actual (h, k)) ≤ 1) (source_failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < epsilon / 2) (total_variation : Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) (exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ lam) (mismatch : (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if matched outcome = true then 0 else 1) ≤ 4 * lam) (matched_physical_branch : ∀ (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y), matched (flag, x, y) = true → ∑ k : K, quadraticExpectation (effect (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k)) (actual (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k)) ≤ ∑ j : Fin L, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G (PA flag) (PB flag) j.succ j.succ x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (U flag x) (V flag y) (z flag)) j.succ j.succ)) : 1 - epsilon / 2 - 5 * lam - (bad + 4 * √deviation + 2 * √clipping) ≤ (pureFlaggedStrategy G (exactSourceSharedFlagWeight D denominator) ⋯ ⋯ z z_normalized (fun (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) => unitaryConjugatePOVM (U flag x) (dependentBlockPOVM fun (r : Fin (L + 1)) => PA flag r x)) fun (flag : ExactSourceSharedFlag X Y A B D denominator) (y : Y) => unitaryConjugatePOVM (V flag y) (dependentBlockPOVM fun (r : Fin (L + 1)) => PB flag r y)).winProbability

def QuantumParallelRepetition.unconditionalActualLocalPOVMLosingEffect {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) ℂ

Equations

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

theorem QuantumParallelRepetition.unconditionalActualLocalPOVMWinningEffect_posSemidef {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) : (directDSVActualLocalPOVMWinningEffect G PA PB x y).PosSemidef

theorem QuantumParallelRepetition.unconditionalActualLocalPOVMLosingEffect_posSemidef {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) : (unconditionalActualLocalPOVMLosingEffect G PA PB x y).PosSemidef

theorem QuantumParallelRepetition.unconditionalActualLocalPOVMWinningEffect_add_losingEffect {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) : directDSVActualLocalPOVMWinningEffect G PA PB x y + unconditionalActualLocalPOVMLosingEffect G PA PB x y = 1

theorem QuantumParallelRepetition.unconditionalActualLocalPOVMWinningEffect_complement_posSemidef {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) : (1 - directDSVActualLocalPOVMWinningEffect G PA PB x y).PosSemidef

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_isPositive {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) : (integratorActualC485WinningEffect G n S D a₀ b₀ j x y).IsPositive

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_complement_isPositive {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) : (1 - integratorActualC485WinningEffect G n S D a₀ b₀ j x y).IsPositive

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_norm_le_one {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) : ‖integratorActualC485WinningEffect G n S D a₀ b₀ j x y‖ ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_born_nonnegative {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) (z : IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j) : 0 ≤ quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j x y) z

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_born_le_mass {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) (z : IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j) : quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j x y) z ≤ ‖z‖ ^ 2

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_bounds {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 : ℕ} (actual : ExactLocallySampleableTuple X Y A B D → (j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j) (actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1) (h : ExactLocallySampleableTuple X Y A B D) : 0 ≤ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ∧ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_nonnegative {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 : ℕ} (actual : ExactLocallySampleableTuple X Y A B D → (j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j) (actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1) (h : ExactLocallySampleableTuple X Y A B D) : 0 ≤ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j)

theorem QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_bounded {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 : ℕ} (actual : ExactLocallySampleableTuple X Y A B D → (j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j) (actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1) (h : ExactLocallySampleableTuple X Y A B D) : ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ≤ 1

noncomputable def QuantumParallelRepetition.unconditionalActualC485FairSourceDiagonalWork {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)) (w : ℝ) (N P : ℕ) {L : ℕ} (schedule : Fin L → Fin 1) (u : ExactLocallySampleableTuple X Y A B D) (j : Fin L) : EuclideanSpace ℂ (IntegratorActualC485RetainedIndex 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L j)

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy {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)) {w : ℝ} {N P L m : ℕ} (width : 0 < w) (grid : 0 < N) (fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1)) (schedule : Fin L → Fin 1) : ℝ

Equations

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

theorem QuantumParallelRepetition.unconditionalActualC485FairSourceDiagonalWork_row {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)) {w : ℝ} {N P L m : ℕ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) (phases : 0 < P) (harmonic : 0 < m) (schedule : Fin L → Fin 1) (u : ExactLocallySampleableTuple X Y A B D) : ∑ j : Fin L, ‖unconditionalActualC485FairSourceDiagonalWork G n S D w N P schedule u j‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy_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) (source_positive : 0 < repeatedPostselectionMass G n S D) {w : ℝ} {N P L m : ℕ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) (fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1)) (phases : 0 < P) (harmonic : 0 < m) (schedule : Fin L → Fin 1) : unconditionalActualC485FairSourceClipEnergy G n S D width grid fine schedule ≤ 16 * martingaleRate G n S D + 8 * (1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N)

theorem QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy_le_budget {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) (source_positive : 0 < repeatedPostselectionMass G n S D) {w δ : ℝ} {N P L m : ℕ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) (fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1)) (phases : 0 < P) (harmonic : 0 < m) (schedule : Fin L → Fin 1) (scalar : 1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N ≤ 3 * δ / 2) : unconditionalActualC485FairSourceClipEnergy G n S D width grid fine schedule ≤ 16 * martingaleRate G n S D + 8 * (3 * δ / 2)

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

theorem QuantumParallelRepetition.unconditionalActualFairCleanedVector_norm_sq {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (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) : ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j

theorem QuantumParallelRepetition.unconditionalActualFairCleanedRow_eq_stoppedSuccess {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (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, ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ

theorem QuantumParallelRepetition.unconditionalActualFairCleanedRow_le_one {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (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, ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairWeightedCleanedMass_le_one {I : Type} [Fintype I] {S B N d L m : ℕ} (weight : I → ℝ) (weight_nonnegative : ∀ (h : I), 0 ≤ weight h) (weight_normalized : ∑ h : I, weight h = 1) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : I → BipartiteUnitVector d) (Q : ℕ) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : ∑ h : I, weight h * ∑ j : Fin L, ‖integratorActualC485CleanedVector Q width schedule (ξ h) (ζ h) A C j‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairWeightedStoppedSuccess {I : Type} [Fintype I] {S B N d L m : ℕ} (weight : I → ℝ) (weight_normalized : ∑ h : I, weight h = 1) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : I → BipartiteUnitVector d) (Q : ℕ) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (async terminal : ℝ) (asynchronous_bound : ∑ h : I, weight h * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ h) (ζ h) ≤ async) (terminal_bound : ∑ h : I, weight h * dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ h) (ζ h) ≤ terminal) : 1 - (async + terminal) ≤ ∑ h : I, weight h * ∑ j : Fin L, ‖integratorActualC485CleanedVector Q width schedule (ξ h) (ζ h) A C j‖ ^ 2

theorem QuantumParallelRepetition.unconditionalActualFairCanonicalVector_norm_sq {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (positive : 0 < width (schedule j)) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : ‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖ ^ 2 = ‖integratorActualC485NormalizedDiagonalWork width schedule ξ ζ j‖ ^ 2

theorem QuantumParallelRepetition.unconditionalActualFairCanonicalRow_le_one {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1)) : ∑ j : Fin L, ‖integratorActualC485CanonicalVector schedule ξ ζ j ⋯ grid ⋯‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairWeightedCanonicalMass_le_one {I : Type} [Fintype I] {S B N d L m : ℕ} (weight : I → ℝ) (weight_nonnegative : ∀ (h : I), 0 ≤ weight h) (weight_normalized : ∑ h : I, weight h = 1) (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : I → BipartiteUnitVector d) (fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1)) : ∑ h : I, weight h * ∑ j : Fin L, ‖integratorActualC485CanonicalVector schedule (ξ h) (ζ h) j ⋯ grid ⋯‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairSourceVector_norm_sq {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (ψ : EuclideanSpace ℂ (Fin d × Fin d)) (unit : ‖ψ‖ = 1) (j : Fin L) : ‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ ^ 2 = ‖integratorActualC485NormalizedDiagonalWork width schedule ξ ζ j‖ ^ 2

theorem QuantumParallelRepetition.unconditionalActualFairSourceCanonicalVector_norm_sq {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (ψ : EuclideanSpace ℂ (Fin d × Fin d)) (unit : ‖ψ‖ = 1) (j : Fin L) (positive : 0 < width (schedule j)) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : ‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ ^ 2 = ‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖ ^ 2

theorem QuantumParallelRepetition.unconditionalActualFairSourceCanonicalVector_norm {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (ψ : EuclideanSpace ℂ (Fin d × Fin d)) (unit : ‖ψ‖ = 1) (j : Fin L) (positive : 0 < width (schedule j)) (fine : ↑d / ↑N < 1 / (width (schedule j) + 1)) : ‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ = ‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖

theorem QuantumParallelRepetition.unconditionalActualSourceSamplerBounds {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) : ∃ (denominator : ℕ), 0 < denominator ∧ ∃ (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ), (∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) ∧ (∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D), 0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history → 0 < numerator index history) ∧ ∃ (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty), Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) (exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ exactSourcePinskerRate G n S D + gamma ∧ (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if exactSourcePermutationMatched D denominator numerator nonempty outcome = true then 0 else 1) ≤ 4 * (exactSourcePinskerRate G n S D + gamma)

theorem QuantumParallelRepetition.unconditionalSourcePhysicalSameGridWeightedStoppingLedger {d N : ℕ} (dimension : 0 < d) (grid : 0 < N) (w δ : ℝ) (large : 1 ≤ w) (precision : 0 < δ) (bounded : δ ≤ 1) (grid_budget : 2 * (w + 1) * (↑d / ↑N) ≤ δ) (t : ℝ) (t_positive : 0 < t) (t_bounded : t ≤ 1) (rho : ℝ) (rho_positive : 0 < rho) {ι : Type} [Fintype ι] (weight : ι → ℝ) (weight_nonnegative : ∀ (i : ι), 0 ≤ weight i) (weight_normalized : ∑ i : ι, weight i = 1) (ξ ζ : ι → BipartiteUnitVector d) (eta : ℝ) (source_energy : ∑ i : ι, weight i * ‖↑(ξ i) - ↑(ζ i)‖ ^ 2 ≤ 32 * eta) : ∃ (L : ℕ) (B : ℕ) (Q : ℕ) (m : ℕ), 0 < L ∧ 0 < B ∧ 0 < Q ∧ 0 < m ∧ ∃ (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)), have width := fun (x : Fin 1) => w; have schedule := fun (x : Fin L) => 0; (∀ (i : ι), dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ i) (ζ i) ≤ 8 * √2 * ‖↑(ξ i) - ↑(ζ i)‖ + δ) ∧ (∀ (i : ι), dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ i) (ζ i) ≤ δ ^ 2) ∧ ∑ i : ι, weight i * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ i) (ζ i) ≤ 64 * √eta + δ ∧ ∑ i : ι, weight i * dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ i) (ζ i) ≤ δ ^ 2 ∧ ∑ i : ι, weight i * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m width schedule (ξ i) (ζ i) A C ≤ 34 / t * (64 * √eta + δ) + 4 * rho ^ 2 + (16 * (Real.exp 1 - 1) + 4) * t

theorem QuantumParallelRepetition.unconditionalSmallSource_eta_le_one (eta alpha : ℝ) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) : eta ≤ 1

theorem QuantumParallelRepetition.unconditionalSmallSource_eta_scaled_root (eta : ℝ) (eta_nonnegative : 0 ≤ eta) : eta ^ (1 / 12) ≤ (32 * eta) ^ (1 / 12)

theorem QuantumParallelRepetition.unconditionalSmallSource_root_estimates (eta alpha : ℝ) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) : have δ := alpha ^ (1 / 3); have R := alpha ^ (1 / 12) + (32 * eta) ^ (1 / 12); 0 ≤ R ∧ √eta ≤ R ∧ δ ≤ R ∧ δ ^ 2 ≤ R ∧ √δ ≤ R

theorem QuantumParallelRepetition.unconditionalSmallSource_clipping_sqrt_le (eta alpha clipping : ℝ) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) (actual_clipping : clipping ≤ 16 * eta + 8 * (3 * alpha ^ (1 / 3) / 2)) : √clipping ≤ 8 * (alpha ^ (1 / 12) + (32 * eta) ^ (1 / 12))

theorem QuantumParallelRepetition.unconditionalSmallSource_deviation_sqrt_le (eta alpha deviation : ℝ) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) (actual_deviation : deviation ≤ 34 / √(64 * √eta + alpha ^ (1 / 3)) * (64 * √eta + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √eta + alpha ^ (1 / 3))) : √deviation ≤ (4 * √(34 + unconditionalPrefactorBucketCoefficient) + 2) * (alpha ^ (1 / 12) + (32 * eta) ^ (1 / 12))

theorem QuantumParallelRepetition.unconditionalSmallSourcePhysicalLoss (K eta alpha deviation clipping : ℝ) (constant : 1024 + 8 * (4 * √(34 + unconditionalPrefactorBucketCoefficient) + 2) ≤ K) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) (actual_deviation : deviation ≤ 34 / √(64 * √eta + alpha ^ (1 / 3)) * (64 * √eta + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √eta + alpha ^ (1 / 3))) (actual_clipping : clipping ≤ 16 * eta + 8 * (3 * alpha ^ (1 / 3) / 2)) : 64 * √eta + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 4 * √clipping ≤ K * (alpha ^ (1 / 12) + (32 * eta) ^ (1 / 12))

theorem QuantumParallelRepetition.unconditionalSmallSourcePhysicalRoundedLower (K eta alpha deviation clipping epsilon lam actual : ℝ) (constant : 1024 + 8 * (4 * √(34 + unconditionalPrefactorBucketCoefficient) + 2) ≤ K) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √eta + alpha ^ (1 / 3) ≤ 1) (actual_deviation : deviation ≤ 34 / √(64 * √eta + alpha ^ (1 / 3)) * (64 * √eta + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √eta + alpha ^ (1 / 3))) (actual_clipping : clipping ≤ 16 * eta + 8 * (3 * alpha ^ (1 / 3) / 2)) (lam_nonnegative : 0 ≤ lam) (actual_original_verifier : 1 - epsilon / 2 - 5 * lam - (64 * √eta + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 4 * √clipping + 2 * √(8 * eta)) ≤ actual) : roundedWinningLowerBound epsilon K alpha eta lam ≤ actual

theorem QuantumParallelRepetition.pdfGreedyCeilingHorizon_le (n : ℕ) (τ d : ℝ) (threshold : 0 < τ) (small : d ≤ τ / 2) : ⌈d * ↑n / τ⌉₊ ≤ n

theorem QuantumParallelRepetition.pdfGreedyCeilingHorizon_pow_le_exp (n : ℕ) (τ d : ℝ) (threshold : 0 < τ) (at_most_one : τ ≤ 1) : (1 - τ) ^ ⌈d * ↑n / τ⌉₊ ≤ Real.exp (-d * ↑n)

theorem QuantumParallelRepetition.pdfGreedyCard_lt_of_ceil (k n : ℕ) (τ d : ℝ) (below : k < ⌈d * ↑n / τ⌉₊) : ↑k < d * ↑n / τ

theorem QuantumParallelRepetition.pdfQuantitativeGreedyConditioning {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 θ : ℝ) (_n_positive : 0 < n) (threshold : 0 < τ) (threshold_lt_one : τ < 1) (_rate_positive : 0 < d) (rate_small : d ≤ τ / 2) (above_exponential : Real.exp (-d * ↑n) < θ) (realized : θ ≤ S.winProbability) : ∃ (D : Finset (Fin n)), ↑D.card < d * ↑n / τ ∧ ↑n / 2 < ↑(Finset.univ \ D).card ∧ θ ≤ repeatedPostselectionMass G n S D ∧ S.winProbability ≤ repeatedPostselectionMass G n S D ∧ 0 < repeatedPostselectionMass G n S D ∧ 0 < (Finset.univ \ D).card ∧ uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < τ

noncomputable def QuantumParallelRepetition.pdfUniversalRate (B : ℝ) : ℝ

Equations

• QuantumParallelRepetition.pdfUniversalRate B = 1 / (8 * (4 * B) ^ 12)

noncomputable def QuantumParallelRepetition.pdfGapRate (B ε ell : ℝ) : ℝ

Equations

• QuantumParallelRepetition.pdfGapRate B ε ell = QuantumParallelRepetition.pdfUniversalRate B * ε ^ 13 / (ε + ell)

noncomputable def QuantumParallelRepetition.pdfConditioningTolerance (ε : ℝ) : ℝ

Equations

• QuantumParallelRepetition.pdfConditioningTolerance ε = ε / 4

noncomputable def QuantumParallelRepetition.pdfCatalystAccuracy (K ε : ℝ) : ℝ

Equations

• QuantumParallelRepetition.pdfCatalystAccuracy K ε = (ε / (16 * K)) ^ 12

theorem QuantumParallelRepetition.pdfUniversalRate_pos {B : ℝ} (positive : 0 < B) : 0 < pdfUniversalRate B

theorem QuantumParallelRepetition.pdfGapRate_pos {B ε ell : ℝ} (constant : 0 < B) (gap : 0 < ε) (alphabet : 0 ≤ ell) : 0 < pdfGapRate B ε ell

theorem QuantumParallelRepetition.pdfGapRate_eq_scaled_twelfth_power {B ε ell : ℝ} (constant : 0 < B) (gap : 0 < ε) (alphabet : 0 ≤ ell) : pdfGapRate B ε ell = ε / (8 * (ε + ell)) * (ε / (4 * B)) ^ 12

theorem QuantumParallelRepetition.pdfGapBase_le_gap {B ε : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) : 0 < ε / (4 * B) ∧ ε / (4 * B) ≤ ε

theorem QuantumParallelRepetition.pdfGapBase_twelfth_le_gap {B ε : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (unit : ε ≤ 1) : (ε / (4 * B)) ^ 12 ≤ ε

theorem QuantumParallelRepetition.pdfGapBase_twelfth_le_one {B ε : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (unit : ε ≤ 1) : (ε / (4 * B)) ^ 12 ≤ 1

theorem QuantumParallelRepetition.pdfGapRate_le_gap_div_eight {B ε ell : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (unit : ε ≤ 1) (alphabet : 0 ≤ ell) : pdfGapRate B ε ell ≤ ε / 8

theorem QuantumParallelRepetition.pdfConditioningTolerance_bounds {ε : ℝ} (gap : 0 < ε) (unit : ε ≤ 1) : 0 < pdfConditioningTolerance ε ∧ pdfConditioningTolerance ε ≤ 1 / 4

theorem QuantumParallelRepetition.pdfGapRate_le_half_conditioningTolerance {B ε ell : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (unit : ε ≤ 1) (alphabet : 0 ≤ ell) : pdfGapRate B ε ell ≤ pdfConditioningTolerance ε / 2

theorem QuantumParallelRepetition.pdfGapRate_entropy_factor {B ε ell : ℝ} (constant : 0 < B) (gap : 0 < ε) (alphabet : 0 ≤ ell) : 2 * pdfGapRate B ε ell * (1 + 4 * ell / ε) = (ε / (4 * B)) ^ 12 * ((ε + 4 * ell) / (4 * (ε + ell)))

theorem QuantumParallelRepetition.pdfAlphabetEntropyFactor_le_one {ε ell : ℝ} (gap : 0 < ε) (alphabet : 0 ≤ ell) : (ε + 4 * ell) / (4 * (ε + ell)) ≤ 1

theorem QuantumParallelRepetition.pdfGapRate_entropy_le_twelfth_power {B ε ell : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (alphabet : 0 ≤ ell) : 2 * pdfGapRate B ε ell * (1 + 4 * ell / ε) ≤ (ε / (4 * B)) ^ 12

theorem QuantumParallelRepetition.pdfCatalystAccuracy_bounds {K ε : ℝ} (constant : 1 ≤ K) (gap : 0 < ε) (unit : ε ≤ 1) : 0 < pdfCatalystAccuracy K ε ∧ pdfCatalystAccuracy K ε ≤ 1

theorem QuantumParallelRepetition.pdfQuantitativeEntropyRate_lt {n m k : ℕ} {t d τ ell : ℝ} (length : 0 < n) (rate : 0 < d) (tolerance : 0 < τ) (alphabet : 0 ≤ ell) (remaining : ↑n / 2 < ↑m) (postselection : t < d * ↑n) (conditioned : ↑k < d * ↑n / τ) : (t + ↑k * ell) / ↑m < 2 * d * (1 + ell / τ)

theorem QuantumParallelRepetition.pdfQuantitativeEntropyRate_lt_twelfth_power {B ε ell : ℝ} {n m k : ℕ} {t : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (unit : ε ≤ 1) (alphabet : 0 ≤ ell) (length : 0 < n) (remaining : ↑n / 2 < ↑m) (postselection : t < pdfGapRate B ε ell * ↑n) (conditioned : ↑k < pdfGapRate B ε ell * ↑n / pdfConditioningTolerance ε) : (t + ↑k * ell) / ↑m < (ε / (4 * B)) ^ 12

theorem QuantumParallelRepetition.pdfCatalystAccuracy_twelfth_root {K ε : ℝ} (constant : 1 ≤ K) (gap : 0 < ε) : pdfCatalystAccuracy K ε ^ (1 / 12) = ε / (16 * K)

theorem QuantumParallelRepetition.pdfGapBase_twelfth_root {B ε : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) : ((ε / (4 * B)) ^ 12) ^ (1 / 12) = ε / (4 * B)

theorem QuantumParallelRepetition.pdfEntropyRoot_lt_gapBase {B ε η : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (entropy : 0 ≤ η) (small : η < (ε / (4 * B)) ^ 12) : η ^ (1 / 12) < ε / (4 * B)

theorem QuantumParallelRepetition.pdfEntropyRoundingLoss_lt_gapQuarter {B ε η : ℝ} (constant : 1 ≤ B) (gap : 0 < ε) (entropy : 0 ≤ η) (small : η < (ε / (4 * B)) ^ 12) : B * η ^ (1 / 12) < ε / 4

theorem QuantumParallelRepetition.pdfCatalystAccuracy_samplingLoss {K ε : ℝ} (constant : 1 ≤ K) (gap : 0 < ε) : 2 * K * pdfCatalystAccuracy K ε ^ (1 / 12) = ε / 8

noncomputable def QuantumParallelRepetition.pdfRoundingCoefficient (K : ℝ) : ℝ

Equations

• QuantumParallelRepetition.pdfRoundingCoefficient K = (5 + 2 * QuantumParallelRepetition.universalErrorCeiling K) * √(3 / 2) + 2 * K * 32 ^ (1 / 12) + 2 * √8

theorem QuantumParallelRepetition.pdfUniversalErrorCeiling_pos {K : ℝ} (constant : 1 ≤ K) : 0 < universalErrorCeiling K

theorem QuantumParallelRepetition.pdfRoundingCoefficient_two_le {K : ℝ} (constant : 1 ≤ K) : 2 ≤ pdfRoundingCoefficient K

theorem QuantumParallelRepetition.pdfRoundingCoefficient_one_le {K : ℝ} (constant : 1 ≤ K) : 1 ≤ pdfRoundingCoefficient K

theorem QuantumParallelRepetition.pdfSqrt_le_twelfthRoot {eta : ℝ} (nonnegative : 0 ≤ eta) (bounded : eta ≤ 1) : √eta ≤ eta ^ (1 / 12)

theorem QuantumParallelRepetition.pdfPinskerRoot_le_twelfthRoot {eta kappa : ℝ} (nonnegative : 0 ≤ eta) (bounded : eta ≤ 1) (pinsker : kappa ≤ √(3 / 2 * eta)) : kappa ≤ √(3 / 2) * eta ^ (1 / 12)

theorem QuantumParallelRepetition.pdfSqrtEight_le_twelfthRoot {eta : ℝ} (nonnegative : 0 ≤ eta) (bounded : eta ≤ 1) : √(8 * eta) ≤ √8 * eta ^ (1 / 12)

theorem QuantumParallelRepetition.pdfQuantitativeRoundingLoss {K alpha eta kappa gamma : ℝ} (constant : 0 ≤ K) (nonnegative : 0 ≤ eta) (bounded : eta ≤ 1) (pinsker : kappa ≤ √(3 / 2 * eta)) : totalSamplingLoss K alpha eta (kappa + gamma) ≤ 2 * K * alpha ^ (1 / 12) + pdfRoundingCoefficient K * eta ^ (1 / 12) + (5 + 2 * universalErrorCeiling K) * gamma

theorem QuantumParallelRepetition.pdfExistsRepeatedStrategyAboveExponential {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 : ℝ) (failure : Real.exp (-d * ↑n) < repeatedEntangledValue G n) : ∃ (S : Strategy (G.repeat n)), Real.exp (-d * ↑n) < S.winProbability

theorem QuantumParallelRepetition.pdfFixedExponentialBound_of_sourceEquationTwentyNine {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 : ℝ) (construct : ∀ (S : Strategy (G.repeat n)), Real.exp (-d * ↑n) < S.winProbability → ∃ (rounded : Strategy G) (K₀ : ℝ) (α : ℝ) (η : ℝ) (lam : ℝ), roundedWinningLowerBound (1 - entangledValue G) K₀ α η lam ≤ rounded.winProbability ∧ totalSamplingLoss K₀ α η lam < (1 - entangledValue G) / 2) : repeatedEntangledValue G n ≤ Real.exp (-d * ↑n)

theorem QuantumParallelRepetition.entangledValue_eq_zero_of_strategyWinProbability_eq_zero {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) (hzero : ∀ (S : Strategy G), S.winProbability = 0) : entangledValue G = 0

def QuantumParallelRepetition.pdfConstantDensity : DensityMatrix (PUnit.{u_6 + 1} × PUnit.{u_5 + 1})

Equations

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

noncomputable def QuantumParallelRepetition.pdfConstantPOVM {C : Type u_5} [Fintype C] (answer : C) : POVM C PUnit.{u_6 + 1}

Equations

• QuantumParallelRepetition.pdfConstantPOVM answer = { effect := fun (c : C) => if c = answer then 1 else 0, positive := ⋯, complete := ⋯ }

noncomputable def QuantumParallelRepetition.pdfConstantStrategy {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) (a : A) (b : B) : Strategy G

Equations

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

theorem QuantumParallelRepetition.pdfConstantStrategy_outcomeProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (a : A) (b : B) (x : X) (y : Y) (a' : A) (b' : B) : (pdfConstantStrategy G a b).outcomeProbability x y a' b' = if a' = a ∧ b' = b then 1 else 0

theorem QuantumParallelRepetition.pdfConstantStrategy_winProbability {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (a : A) (b : B) : (pdfConstantStrategy G a b).winProbability = ∑ x : X, ∑ y : Y, if G.predicate x y a b = true then G.questionWeight x y else 0

theorem QuantumParallelRepetition.pdfQuestionWeight_le_constantStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (x : X) (y : Y) (a : A) (b : B) (accepted : G.predicate x y a b = true) : G.questionWeight x y ≤ (pdfConstantStrategy G a b).winProbability

theorem QuantumParallelRepetition.pdfPredicate_not_accepted_of_entangledValue_eq_zero {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) (zero : entangledValue G = 0) (x : X) (y : Y) (a : A) (b : B) (supported : 0 < G.questionWeight x y) : G.predicate x y a b ≠ true

theorem QuantumParallelRepetition.pdfRepeatedEntangledValue_eq_zero_of_entangledValue_eq_zero {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) (zero : entangledValue G = 0) {n : ℕ} (positive : 0 < n) : repeatedEntangledValue G n = 0

theorem QuantumParallelRepetition.pdfAlphabetEntropy_nonneg {A B : Type} [Fintype A] [Fintype B] (alice : Nonempty A) (bob : Nonempty B) : 0 ≤ Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

theorem QuantumParallelRepetition.pdfGap_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : 1 - entangledValue G ≤ 1

theorem QuantumParallelRepetition.pdfPostselectionLogCost_lt_of_exponential {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)) (d : ℝ) (above : Real.exp (-d * ↑n) < repeatedPostselectionMass G n S D) : postselectionLogCost G n S D < d * ↑n

theorem QuantumParallelRepetition.pdfPinskerRate_le_sqrt_martingaleRate {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) : exactSourcePinskerRate G n S D ≤ √(3 / 2 * martingaleRate G n S D)

theorem QuantumParallelRepetition.pdfActualMartingaleRate_lt_twelfth_power {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)) (Bqs ε ell : ℝ) (constant : 1 ≤ Bqs) (gap : 0 < ε) (unit : ε ≤ 1) (alphabet : 0 ≤ ell) (alphabet_eq : ell = Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) (length : 0 < n) (remaining : ↑n / 2 < ↑(Finset.univ \ D).card) (above : Real.exp (-pdfGapRate Bqs ε ell * ↑n) < repeatedPostselectionMass G n S D) (conditioned : ↑D.card < pdfGapRate Bqs ε ell * ↑n / pdfConditioningTolerance ε) : martingaleRate G n S D < (ε / (4 * Bqs)) ^ 12

theorem QuantumParallelRepetition.pdfFullQuantitativeSamplingLoss {K ε eta kappa : ℝ} (constant : 1 ≤ K) (gap : 0 < ε) (unit : ε ≤ 1) (entropy : 0 ≤ eta) (small : eta < (ε / (4 * pdfRoundingCoefficient K)) ^ 12) (pinsker : kappa ≤ √(3 / 2 * eta)) : totalSamplingLoss K (pdfCatalystAccuracy K ε) eta (kappa + ε / (16 * (5 + 2 * universalErrorCeiling K))) < ε / 2

theorem QuantumParallelRepetition.pdf_distributionUniformExponential_of_uniform_source_rounding (rounding : ∃ (K : ℝ), 1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)), 0 < (Finset.univ \ D).card → 0 < repeatedPostselectionMass G n S D → ∀ (alpha gamma : ℝ), 0 < alpha → alpha ≤ 1 → 0 < gamma → uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 → ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability) : ∃ (c : ℝ), 0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B), Nonempty A → Nonempty B → 0 < 1 - entangledValue G → ∀ (n : ℕ), 0 < n → repeatedEntangledValue G n ≤ Real.exp (-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalRoundingUniversalConstant : ℝ

Equations

• QuantumParallelRepetition.unconditionalSourcePhysicalRoundingUniversalConstant = 1024 + 8 * (4 * √(34 + QuantumParallelRepetition.unconditionalPrefactorBucketCoefficient) + 2)

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRoundingUniversalConstant_ge : 128 ≤ unconditionalSourcePhysicalRoundingUniversalConstant

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_sourceSampler {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) (gamma : ℝ) (gamma_positive : 0 < gamma) : ∃ (base : ExactHistoryFlag X Y A B D) (denominator : ℕ), 0 < denominator ∧ ∃ (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ), (∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) ∧ (∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D), 0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history → 0 < numerator index history) ∧ ∃ (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty), Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) (exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ exactSourcePinskerRate G n S D + gamma ∧ (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if exactSourcePermutationMatched D denominator numerator nonempty outcome = true then 0 else 1) ≤ 4 * (exactSourcePinskerRate G n S D + gamma)

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_fairTargetEnergy {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) : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ‖↑(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)‖ ^ 2 ≤ 32 * martingaleRate G n S D

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_fairStoppingHazard {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) (alpha : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) : ∃ (w : ℝ) (N : ℕ) (L : ℕ) (B' : ℕ) (Q : ℕ) (m : ℕ), 1 ≤ w ∧ 0 < N ∧ 0 < L ∧ 0 < B' ∧ 0 < Q ∧ 0 < m ∧ 2 * (w + 1) * (↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N) ≤ alpha ^ (1 / 3) ∧ ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1) ∧ 1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N ≤ 3 * alpha ^ (1 / 3) / 2 ∧ ∃ (UA : Fin B' → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (UB : Fin B' → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)), have width := fun (x : Fin 1) => w; have schedule := fun (x : Fin L) => 0; have eta := martingaleRate G n S D; have delta := alpha ^ (1 / 3); have t := √(64 * √eta + delta); have rho := alpha ^ (1 / 12); (∀ (ξ : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))), ‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 ≤ 3 * delta / 2) ∧ ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N 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) ≤ 64 * √eta + delta ∧ ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalTerminalMass N 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) ≤ delta ^ 2 ∧ ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m 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) UA UB ≤ 34 / t * (64 * √eta + delta) + 4 * rho ^ 2 + unconditionalPrefactorBucketCoefficient * t

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_largeVerifierBound (K eta alpha lam epsilon : ℝ) (constant : 128 ≤ K) (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (lam_nonnegative : 0 ≤ lam) (epsilon_nonnegative : 0 ≤ epsilon) (large : 1 < 64 * √eta + alpha ^ (1 / 3)) : roundedWinningLowerBound epsilon K alpha eta lam ≤ 0

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_large {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) (K alpha gamma : ℝ) (constant : 128 ≤ K) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (large : 1 < 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) : ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_smallRoundedLower {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) (alpha gamma deviation clipping : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) (actual_deviation : deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3))) (actual_clipping : clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2)) (rounded : Strategy G) (actual_original_verifier : 1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 4 * √clipping + 2 * √(8 * martingaleRate G n S D)) ≤ rounded.winProbability) : roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_smallRoundedLower_of_stoppedVerifier {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) (alpha gamma deviation clipping : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) (actual_deviation : deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3))) (actual_clipping : clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2)) (rounded : Strategy G) (stopped_verifier : 1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 2 * √clipping) ≤ rounded.winProbability) : roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalSourceOneGameRounding_uniform_of_small (small_rounding : ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)), 0 < (Finset.univ \ D).card → 0 < repeatedPostselectionMass G n S D → ∀ (alpha gamma : ℝ), 0 < alpha → alpha ≤ 1 → 0 < gamma → 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1 → uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 → ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)), 0 < (Finset.univ \ D).card → 0 < repeatedPostselectionMass G n S D → ∀ (alpha gamma : ℝ), 0 < alpha → alpha ≤ 1 → 0 < gamma → uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 → ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalActualC485GenericRetainedWinningBorn {X Y A B s t u v ι κ : Type} [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 ℂ (ι × κ)) : quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA PA) (directDSVActualReindexedRetainedPOVM eB PB) x y)) z = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G PA PB x y) 1)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)

theorem QuantumParallelRepetition.unconditionalActualC485GenericSelectedWinningRegroupGauge {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} {ι κ R T : Type} [Fintype ι] [Fintype κ] [Fintype R] [Fintype T] [DecidableEq ι] [DecidableEq κ] [DecidableEq R] [DecidableEq T] (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (pair : R × R ≃ T) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) : let selected := UnconditionalSelectedCopyLocalIndex P d N m; have stage := physical8SelectedGlobalTargetWorkEquiv P N d m; have gaugedAlice := directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM alice PA); have gaugedBob := directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM bob PB); have plainAlice := directDSVActualReindexedRetainedPOVM stage PA; have plainBob := directDSVActualReindexedRetainedPOVM stage PB; have regrouped := (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (selected × selected)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z); quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA gaugedAlice) (directDSVActualReindexedRetainedPOVM eB gaugedBob) x y)) z = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G plainAlice plainBob x y) 1)) (unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice) (unconditionalMixedConjugateSigmaAtomLift P bob) regrouped)

theorem QuantumParallelRepetition.unconditionalActualC485GenericDecodedWinningBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} {ι κ R T : Type} [Fintype ι] [Fintype κ] [Fintype R] [Fintype T] [DecidableEq ι] [DecidableEq κ] [DecidableEq R] [DecidableEq T] (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (pair : R × R ≃ T) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) (actual : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T)) (decoded : unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice) (unconditionalMixedConjugateSigmaAtomLift P bob) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = actual) : let selected := UnconditionalSelectedCopyLocalIndex P d N m; have stage := physical8SelectedGlobalTargetWorkEquiv P N d m; quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM stage PA) (directDSVActualReindexedRetainedPOVM stage PB) x y) 1)) actual = quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA (directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM alice PA))) (directDSVActualReindexedRetainedPOVM eB (directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM bob PB))) x y)) z

theorem QuantumParallelRepetition.unconditionalActualC485SourceSelectedDecodedWinningBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} {ι κ R T : Type} [Fintype ι] [Fintype κ] [Fintype R] [Fintype T] [DecidableEq ι] [DecidableEq κ] [DecidableEq R] [DecidableEq T] (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (selectedA : POVM A (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedB : POVM B (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedA_eq : selectedA = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PA) (selectedB_eq : selectedB = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PB) (eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (pair : R × R ≃ T) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) (actual : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T)) (decoded : unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice) (unconditionalMixedConjugateSigmaAtomLift P bob) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = actual) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G selectedA selectedB x y) 1)) actual = quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM alice PA))) (directDSVActualReindexedRetainedPOVM eB (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM bob PB))) x y)) z

theorem QuantumParallelRepetition.unconditionalActualC485CompleteDecodedPhysicalBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} {ι κ R T : Type} [Fintype ι] [Fintype κ] [Fintype R] [Fintype T] [DecidableEq ι] [DecidableEq κ] [DecidableEq R] [DecidableEq T] (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (selectedA : POVM A (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedB : POVM B (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedA_eq : selectedA = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PA) (selectedB_eq : selectedB = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PB) (eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (pair : R × R ≃ T) (rawA : POVM A ι) (rawB : POVM B κ) (rawA_eq : rawA = directDSVActualReindexedRetainedPOVM eA (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM alice PA))) (rawB_eq : rawB = directDSVActualReindexedRetainedPOVM eB (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM bob PB))) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) (source cleaned : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T)) (source_eq : source = cleaned) (decoded : unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice) (unconditionalMixedConjugateSigmaAtomLift P bob) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = cleaned) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G selectedA selectedB x y) 1)) source = quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G rawA rawB x y)) z

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceAliceTarget {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) : ExactSourceSharedFlag X Y A B D denominator → X → BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceBobTarget {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) : ExactSourceSharedFlag X Y A B D denominator → Y → BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceAliceFlagPOVM {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)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (a₀ : A) (P N L m : ℕ) : ExactSourceSharedFlag X Y A B D denominator → Fin (L + 1) → X → POVM A (UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceBobFlagPOVM {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq 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) (b₀ : B) (P N L m : ℕ) : ExactSourceSharedFlag X Y A B D denominator → Fin (L + 1) → Y → POVM B (UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceAliceStoppingUnitary {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) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : ExactSourceSharedFlag X Y A B D denominator → X → ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m) ℂ)

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceBobStoppingUnitary {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) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : ExactSourceSharedFlag X Y A B D denominator → Y → ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m) ℂ)

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFairSourceAliceFlagPOVM_succ_nested {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [decA : DecidableEq A] (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) (a₀ : A) {P N L m : ℕ} (flag : ExactSourceSharedFlag X Y A B D denominator) (j : Fin L) (x : X) : unconditionalActualFairSourceAliceFlagPOVM G n S D denominator numerator nonempty a₀ P N L m flag j.succ x = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) m) (unitaryConjugatePOVM (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis (unconditionalActualFairSourceAliceTarget G n S D denominator numerator nonempty flag x))) (integratorActualC485SourceAlicePOVM G n S D a₀ x)))

theorem QuantumParallelRepetition.unconditionalActualFairSourceBobFlagPOVM_succ_nested {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [decB : DecidableEq 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) (b₀ : B) {P N L m : ℕ} (flag : ExactSourceSharedFlag X Y A B D denominator) (j : Fin L) (y : Y) : unconditionalActualFairSourceBobFlagPOVM G n S D denominator numerator nonempty b₀ P N L m flag j.succ y = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P) j) (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) m) (unitaryConjugatePOVM (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis (unconditionalActualFairSourceBobTarget G n S D denominator numerator nonempty flag y))) (integratorActualC485SourceBobPOVM G n S D b₀ y)))

theorem QuantumParallelRepetition.unconditionalActualPairedDecodedMatchedCleanedVector {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)) : have phase := unconditionalActualOneScaleFixedSourcePhaseSplit P; have outer := unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phase j; have pair := unconditionalActualC485RetainedHistoryPairEquiv j; have stopped := actualStoppingBranchVector (actualStoppingQuestionLocalAction (physical8OneScaleActualAliceStoppingUnitary phase Q width schedule ξ A flag x) (physical8OneScaleActualBobStoppingUnitary phase Q width schedule ζ C flag y) (unconditionalSourcePhysicalCleanedStoppingFixedSource 1 P N d L m)) j.succ j.succ; unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis (ξ flag x)))) (unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis (ζ flag y)))) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv outer outer)) stopped)) = integratorActualC485CleanedVector Q width schedule (ξ flag x) (ζ flag y) A C j

noncomputable def QuantumParallelRepetition.unconditionalActualC485SelectedVerifierBorn {X Y A B ι T : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [DecidableEq ι] [Fintype T] [DecidableEq T] (G : Game X Y A B) (PA : POVM A ι) (PB : POVM B ι) (x : X) (y : Y) (z : EuclideanSpace ℂ ((ι × ι) × T)) : ℝ

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualC485RawPhysicalVerifierBorn {X Y A B ι κ : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (G : Game X Y A B) (PA : POVM A ι) (PB : POVM B κ) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) : ℝ

Equations

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

theorem QuantumParallelRepetition.unconditionalActualC485CompleteDecodedScalarBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {P N d m : ℕ} {ι κ R T : Type} [Fintype ι] [Fintype κ] [Fintype R] [Fintype T] [DecidableEq ι] [DecidableEq κ] [DecidableEq R] [DecidableEq T] (G : Game X Y A B) (alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (PA : POVM A (Fin d)) (PB : POVM B (Fin d)) (selectedA : POVM A (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedB : POVM B (UnconditionalSelectedCopyLocalIndex P d N m)) (selectedA_eq : selectedA = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PA) (selectedB_eq : selectedB = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PB) (eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R) (pair : R × R ≃ T) (rawA : POVM A ι) (rawB : POVM B κ) (rawA_eq : rawA = directDSVActualReindexedRetainedPOVM eA (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM alice PA))) (rawB_eq : rawB = directDSVActualReindexedRetainedPOVM eB (directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (unitaryConjugatePOVM bob PB))) (x : X) (y : Y) (z : EuclideanSpace ℂ (ι × κ)) (source cleaned : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T)) (source_eq : source = cleaned) (decoded : unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice) (unconditionalMixedConjugateSigmaAtomLift P bob) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr pair)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = cleaned) : unconditionalActualC485SelectedVerifierBorn G selectedA selectedB x y source = unconditionalActualC485RawPhysicalVerifierBorn G rawA rawB x y z

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceHistoryStopBorn {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 : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (h : ExactLocallySampleableTuple X Y A B D) (j : Fin L) : ℝ

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourcePhysicalStopBorn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (a₀ : A) (b₀ : B) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (j : Fin L) : ℝ

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFairSourceHistoryStopBorn_eq_selected {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 : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (h : ExactLocallySampleableTuple X Y A B D) (j : Fin L) : unconditionalActualFairSourceHistoryStopBorn G n S D a₀ b₀ Q width schedule UA UB h j = unconditionalActualC485SelectedVerifierBorn G (integratorActualC485SelectedAlicePOVM G n S D a₀ P N m h.2.1) (integratorActualC485SelectedBobPOVM G n S D b₀ P N m h.2.2.1) h.2.1 h.2.2.1 (integratorActualC485CleanedVector Q width schedule (unconditionalExactFairGammaUnit G n S D h) (exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) UA UB j)

theorem QuantumParallelRepetition.unconditionalActualFairSourcePhysicalStopBorn_eq_raw {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (a₀ : A) (b₀ : B) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (j : Fin L) : let d := Fintype.card (ExactGlobalHistoryLocalIndex G n S D); have PA := unconditionalActualFairSourceAliceFlagPOVM G n S D denominator numerator nonempty a₀ P N L m flag; have PB := unconditionalActualFairSourceBobFlagPOVM G n S D denominator numerator nonempty b₀ P N L m flag; have stopped := actualStoppingBranchVector (actualStoppingQuestionLocalAction (unconditionalActualFairSourceAliceStoppingUnitary G n S D denominator numerator nonempty Q width schedule UA flag x) (unconditionalActualFairSourceBobStoppingUnitary G n S D denominator numerator nonempty Q width schedule UB flag y) (unconditionalSourcePhysicalCleanedStoppingFixedSource 1 P N d L m)) j.succ j.succ; unconditionalActualFairSourcePhysicalStopBorn G n S D denominator numerator nonempty a₀ b₀ Q width schedule UA UB flag x y j = unconditionalActualC485RawPhysicalVerifierBorn G (PA j.succ x) (PB j.succ y) x y stopped

theorem QuantumParallelRepetition.unconditionalActualFairSourceMatchedHistoryGamma {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) : unconditionalExactFairGammaUnit G n S D (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)) = unconditionalActualFairSourceAliceTarget G n S D denominator numerator nonempty flag x

theorem QuantumParallelRepetition.unconditionalActualFairSourceMatchedHistoryPhi {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) (matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) : exactGlobalHistoryFinPhi G n S D (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)).2.2.2 y = unconditionalActualFairSourceBobTarget G n S D denominator numerator nonempty flag y

theorem QuantumParallelRepetition.unconditionalActualFairSourceMatchedHistoryCleanedVector {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) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) (j : Fin L) : have h := exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y); integratorActualC485CleanedVector Q width schedule (unconditionalExactFairGammaUnit G n S D h) (exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) UA UB j = integratorActualC485CleanedVector Q width schedule (unconditionalActualFairSourceAliceTarget G n S D denominator numerator nonempty flag x) (unconditionalActualFairSourceBobTarget G n S D denominator numerator nonempty flag y) UA UB j

theorem QuantumParallelRepetition.unconditionalActualFairSourcePhysicalStopBornWitness {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (a₀ : A) (b₀ : B) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (grid : 0 < N) (width_positive : ∀ (s : Fin 1), 0 < width s) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) (j : Fin L) : unconditionalActualFairSourceHistoryStopBorn G n S D a₀ b₀ Q width schedule UA UB (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)) j = unconditionalActualFairSourcePhysicalStopBorn G n S D denominator numerator nonempty a₀ b₀ Q width schedule UA UB flag x y j

theorem QuantumParallelRepetition.unconditionalActualFairSourcePhysicalBranchWitness {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) (a₀ : A) (b₀ : B) {P N L m : ℕ} (Q : ℕ) (width : Fin 1 → ℝ) (schedule : Fin L → Fin 1) (UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (grid : 0 < N) (width_positive : ∀ (s : Fin 1), 0 < width s) (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y) (matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true) : ∑ j : Fin L, unconditionalActualFairSourceHistoryStopBorn G n S D a₀ b₀ Q width schedule UA UB (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)) j = ∑ j : Fin L, unconditionalActualFairSourcePhysicalStopBorn G n S D denominator numerator nonempty a₀ b₀ Q width schedule UA UB flag x y j

structure QuantumParallelRepetition.UnconditionalActualFairSourceSamplerData {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)) (gamma : ℝ) : Type

• base : ExactHistoryFlag X Y A B D
• denominator : ℕ
• denominator_positive : 0 < self.denominator
• numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ
• rational_normalized (index : ExactLocalSamplerIndex X Y D) : ∑ history : ExactHistoryFlag X Y A B D, self.numerator index history = self.denominator
• support_preserving (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D) : 0 < exactLocalConditionalFamily D self.base (exactLocallySampleableLaw G n S D) index history → 0 < self.numerator index history
• nonempty (index : ExactLocalSamplerIndex X Y D) : (ClassicalSampling.rationalMarked self.denominator (self.numerator index)).Nonempty
• total_variation : Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D self.denominator)) (exactSourceAliceFlagCoupling G n S D self.denominator self.numerator ⋯) ≤ exactSourcePinskerRate G n S D + gamma
• mismatch : (∑ outcome : ExactSourceSharedFlag X Y A B D self.denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D self.denominator) outcome * if exactSourcePermutationMatched D self.denominator self.numerator ⋯ outcome = true then 0 else 1) ≤ 4 * (exactSourcePinskerRate G n S D + gamma)

theorem QuantumParallelRepetition.unconditionalActualFairSourceSamplerData_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) (gamma : ℝ) (gamma_positive : 0 < gamma) : Nonempty (UnconditionalActualFairSourceSamplerData G n S D gamma)

structure QuantumParallelRepetition.UnconditionalActualFairSourceStoppingHazardData {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)) (alpha : ℝ) : Type

• w : ℝ
• N : ℕ
• L : ℕ
• P : ℕ
• Q : ℕ
• m : ℕ
• width_large : 1 ≤ self.w
• grid : 0 < self.N
• phases : 0 < self.P
• harmonic : 0 < self.m
• fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑self.N < 1 / (self.w + 1)
• scalar : 1 / self.w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * self.w / ↑self.N ≤ 3 * alpha ^ (1 / 3) / 2
• UA : Fin self.P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (self.N * self.m)) ℂ)
• UB : Fin self.P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (self.N * self.m)) ℂ)
• asynchronous : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass self.N (fun (x : Fin 1) => self.w) (fun (x : Fin self.L) => 0) (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) ≤ 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)
• terminal : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalTerminalMass self.N (fun (x : Fin 1) => self.w) (fun (x : Fin self.L) => 0) (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) ≤ (alpha ^ (1 / 3)) ^ 2
• hazard : ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard self.Q self.m (fun (x : Fin 1) => self.w) (fun (x : Fin self.L) => 0) (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) self.UA self.UB ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3))

theorem QuantumParallelRepetition.unconditionalActualFairSourceStoppingHazardData_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) (alpha : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) : Nonempty (UnconditionalActualFairSourceStoppingHazardData G n S D alpha)

structure QuantumParallelRepetition.UnconditionalActualFairCachedStoppedAnalyticLedger {I K : Type} [Fintype I] [Fintype K] {H : I × K → Type} [(p : I × K) → NormedAddCommGroup (H p)] [(p : I × K) → InnerProductSpace ℂ (H p)] (law : I → ℝ) (actual canonical source : (p : I × K) → H p) (deviation clipping bad : ℝ) : Prop

• actual_mass : ∑ h : I, law h * ∑ j : K, ‖actual (h, j)‖ ^ 2 ≤ 1
• canonical_mass : ∑ h : I, law h * ∑ j : K, ‖canonical (h, j)‖ ^ 2 ≤ 1
• canonical_row_mass (h : I) : ∑ j : K, ‖canonical (h, j)‖ ^ 2 ≤ 1
• same_work_mass (h : I) (j : K) : ‖source (h, j)‖ = ‖canonical (h, j)‖
• clean_deviation : ∑ h : I, law h * ∑ j : K, ‖actual (h, j) - canonical (h, j)‖ ^ 2 ≤ deviation
• clip_deviation : ∑ h : I, law h * ∑ j : K, ‖canonical (h, j) - source (h, j)‖ ^ 2 ≤ clipping
• actual_success : 1 - bad ≤ ∑ h : I, law h * ∑ j : K, ‖actual (h, j)‖ ^ 2

structure QuantumParallelRepetition.UnconditionalActualFairCachedSourceVerifierLedger {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)) {K : Type} [Fintype K] {H : ExactLocallySampleableTuple X Y A B D × K → Type} [(p : ExactLocallySampleableTuple X Y A B D × K) → NormedAddCommGroup (H p)] [(p : ExactLocallySampleableTuple X Y A B D × K) → InnerProductSpace ℂ (H p)] (effect : (p : ExactLocallySampleableTuple X Y A B D × K) → H p →L[ℂ] H p) (actual source : (p : ExactLocallySampleableTuple X Y A B D × K) → H p) : Prop

• contraction (p : ExactLocallySampleableTuple X Y A B D × K) : ‖effect p‖ ≤ 1
• supported_born (h : ExactLocallySampleableTuple X Y A B D) : exactLocallySampleableLaw G n S D h ≠ 0 → ∀ (j : K), quadraticExpectation (effect (h, j)) (source (h, j)) = ‖source (h, j)‖ ^ 2 * exactSourceConditionalWinningProbability G n S D h
• history_born_nonnegative (h : ExactLocallySampleableTuple X Y A B D) : 0 ≤ ∑ j : K, quadraticExpectation (effect (h, j)) (actual (h, j))
• history_born_bounded (h : ExactLocallySampleableTuple X Y A B D) : ∑ j : K, quadraticExpectation (effect (h, j)) (actual (h, j)) ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairCachedLedgerStoppingTransfer {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) (denominator : ℕ) (denominator_positive : 0 < denominator) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (rational_normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (support_preserving : ∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D), 0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history → 0 < numerator index history) (nonempty : ∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty) {L : ℕ} {ι : Fin (L + 1) → Type} [(r : Fin (L + 1)) → Fintype (ι r)] [(r : Fin (L + 1)) → DecidableEq (ι r)] (PA : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → X → POVM A (ι r)) (PB : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → Y → POVM B (ι r)) (U : ExactSourceSharedFlag X Y A B D denominator → X → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (V : ExactSourceSharedFlag X Y A B D denominator → Y → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ)) (z : ExactSourceSharedFlag X Y A B D denominator → EuclideanSpace ℂ (((r : Fin (L + 1)) × ι r) × (r : Fin (L + 1)) × ι r)) (z_normalized : ∀ (flag : ExactSourceSharedFlag X Y A B D denominator), ‖z flag‖ = 1) (matched : ExactSourceSharedFlag X Y A B D denominator × X × Y → Bool) {K : Type} [Fintype K] {H : ExactLocallySampleableTuple X Y A B D × K → Type} [(p : ExactLocallySampleableTuple X Y A B D × K) → NormedAddCommGroup (H p)] [(p : ExactLocallySampleableTuple X Y A B D × K) → InnerProductSpace ℂ (H p)] (effect : (p : ExactLocallySampleableTuple X Y A B D × K) → H p →L[ℂ] H p) (actual canonical source : (p : ExactLocallySampleableTuple X Y A B D × K) → H p) (epsilon lam deviation clipping bad : ℝ) (analytic : UnconditionalActualFairCachedStoppedAnalyticLedger (exactLocallySampleableLaw G n S D) actual canonical source deviation clipping bad) (verifier : UnconditionalActualFairCachedSourceVerifierLedger G n S D effect actual source) (source_failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < epsilon / 2) (total_variation : Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) (exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ lam) (mismatch : (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if matched outcome = true then 0 else 1) ≤ 4 * lam) (matched_physical_branch : ∀ (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y), matched (flag, x, y) = true → ∑ k : K, quadraticExpectation (effect (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k)) (actual (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k)) ≤ ∑ j : Fin L, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G (PA flag) (PB flag) j.succ j.succ x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (U flag x) (V flag y) (z flag)) j.succ j.succ)) : 1 - epsilon / 2 - 5 * lam - (bad + 4 * √deviation + 2 * √clipping) ≤ (pureFlaggedStrategy G (exactSourceSharedFlagWeight D denominator) ⋯ ⋯ z z_normalized (fun (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) => unitaryConjugatePOVM (U flag x) (dependentBlockPOVM fun (r : Fin (L + 1)) => PA flag r x)) fun (flag : ExactSourceSharedFlag X Y A B D denominator) (y : Y) => unitaryConjugatePOVM (V flag y) (dependentBlockPOVM fun (r : Fin (L + 1)) => PB flag r y)).winProbability

structure QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext {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)) (alpha gamma : ℝ) : Type

• remaining : 0 < (Finset.univ \ D).card
• positive : 0 < repeatedPostselectionMass G n S D
• failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2
• sampler : UnconditionalActualFairSourceSamplerData G n S D gamma
• stopping : UnconditionalActualFairSourceStoppingHazardData G n S D alpha

noncomputable def QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_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) (alpha gamma : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) (failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2) : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma

Equations

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

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.d {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)} {alpha gamma : ℝ} (_c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : ℕ

Equations

• _c.d = Fintype.card (QuantumParallelRepetition.ExactGlobalHistoryLocalIndex G n S D)

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.dimension_pos {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : 0 < c.d

def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.width {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Fin 1 → ℝ

Equations

• c.width x✝ = c.stopping.w

def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.schedule {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Fin c.stopping.L → Fin 1

Equations

• c.schedule x✝ = 0

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.width_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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : 0 < c.stopping.w

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.width_all {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (s : Fin 1) : 0 < c.width s

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.fine_all {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (s : Fin 1) : ↑c.d / ↑c.stopping.N < 1 / (c.width s + 1)

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.sourceIndex {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)} {alpha gamma : ℝ} (_c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Type

Equations

• _c.sourceIndex = QuantumParallelRepetition.ExactLocallySampleableTuple X Y A B D

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.law {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.sourceIndex → ℝ

Equations

• c.law = QuantumParallelRepetition.exactLocallySampleableLaw G n S D

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.gammaVector {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.sourceIndex → BipartiteUnitVector c.d

Equations

• c.gammaVector h = QuantumParallelRepetition.unconditionalExactFairGammaUnit G n S D h

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.phiVector {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.sourceIndex → BipartiteUnitVector c.d

Equations

• c.phiVector h = QuantumParallelRepetition.exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.psiVector {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.sourceIndex → EuclideanSpace ℂ (Fin c.d × Fin c.d)

Equations

• c.psiVector h = QuantumParallelRepetition.exactSourceTuplePsi G n S D h

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.branchSpace {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (p : c.sourceIndex × Fin c.stopping.L) : Type

Equations

• c.branchSpace p = QuantumParallelRepetition.IntegratorActualC485BranchSpace 1 c.stopping.P c.stopping.N c.d c.stopping.L c.stopping.m p.2

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.actual {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (p : c.sourceIndex × Fin c.stopping.L) : c.branchSpace p

Equations

• c.actual p = QuantumParallelRepetition.integratorActualC485CleanedVector c.stopping.Q c.width c.schedule (c.gammaVector p.1) (c.phiVector p.1) c.stopping.UA c.stopping.UB p.2

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.canonical {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (p : c.sourceIndex × Fin c.stopping.L) : c.branchSpace p

Equations

• c.canonical p = QuantumParallelRepetition.integratorActualC485CanonicalVector c.schedule (c.gammaVector p.1) (c.phiVector p.1) p.2 ⋯ ⋯ ⋯

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.source {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (p : c.sourceIndex × Fin c.stopping.L) : c.branchSpace p

Equations

• c.source p = QuantumParallelRepetition.integratorActualC485SourceVector c.width c.schedule (c.gammaVector p.1) (c.phiVector p.1) (c.psiVector p.1) p.2

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.answerNonempty {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Nonempty A ∧ Nonempty B

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.aliceDefault {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : A

Equations

• c.aliceDefault = Classical.choice ⋯

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.bobDefault {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : B

Equations

• c.bobDefault = Classical.choice ⋯

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.effect {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (p : c.sourceIndex × Fin c.stopping.L) : c.branchSpace p →L[ℂ] c.branchSpace p

Equations

• c.effect p = QuantumParallelRepetition.integratorActualC485WinningEffect G n S D c.aliceDefault c.bobDefault p.2 p.1.2.1 p.1.2.2.1

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.deviation {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : ℝ

Equations

• c.deviation = ∑ h : c.sourceIndex, c.law h * ∑ j : Fin c.stopping.L, ‖c.actual (h, j) - c.canonical (h, j)‖ ^ 2

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.clipping {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : ℝ

Equations

• c.clipping = QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy G n S D ⋯ ⋯ ⋯ c.schedule

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.bad {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)} {alpha gamma : ℝ} (_c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : ℝ

Equations

• _c.bad = 64 * √(QuantumParallelRepetition.martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.flag {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Type

Equations

• c.flag = QuantumParallelRepetition.ExactSourceSharedFlag X Y A B D c.sampler.denominator

@[reducible, inline]

abbrev QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.fiber {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Type

Equations

• c.fiber = QuantumParallelRepetition.UnconditionalSourcePhysicalStoppingPhaseFiber 1 c.stopping.P c.stopping.N c.d c.stopping.L c.stopping.m

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.PA {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.flag → Fin (c.stopping.L + 1) → X → POVM A c.fiber

Equations

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

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.PB {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.flag → Fin (c.stopping.L + 1) → Y → POVM B c.fiber

Equations

• c.PB = QuantumParallelRepetition.unconditionalActualFairSourceBobFlagPOVM G n S D c.sampler.denominator c.sampler.numerator ⋯ c.bobDefault c.stopping.P c.stopping.N c.stopping.L c.stopping.m

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.U {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.flag → X → ↥(Matrix.unitaryGroup ((_ : Fin (c.stopping.L + 1)) × c.fiber) ℂ)

Equations

• c.U = QuantumParallelRepetition.unconditionalActualFairSourceAliceStoppingUnitary G n S D c.sampler.denominator c.sampler.numerator ⋯ c.stopping.Q c.width c.schedule c.stopping.UA

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.V {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.flag → Y → ↥(Matrix.unitaryGroup ((_ : Fin (c.stopping.L + 1)) × c.fiber) ℂ)

Equations

• c.V = QuantumParallelRepetition.unconditionalActualFairSourceBobStoppingUnitary G n S D c.sampler.denominator c.sampler.numerator ⋯ c.stopping.Q c.width c.schedule c.stopping.UB

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.prepared {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.flag → EuclideanSpace ℂ (((_ : Fin (c.stopping.L + 1)) × c.fiber) × (_ : Fin (c.stopping.L + 1)) × c.fiber)

Equations

• c.prepared x✝ = QuantumParallelRepetition.unconditionalSourcePhysicalCleanedStoppingFixedSource 1 c.stopping.P c.stopping.N c.d c.stopping.L c.stopping.m

theorem QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.prepared_normalized {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (f : c.flag) : ‖c.prepared f‖ = 1

noncomputable def QuantumParallelRepetition.UnconditionalActualFairSourceRoundingContext.rounded {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : Strategy G

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_actualRow {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (h : ExactLocallySampleableTuple X Y A B D) : ∑ j : Fin c.stopping.L, ‖c.actual (h, j)‖ ^ 2 ≤ 1

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_clippingBound {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2)

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_cleanBound {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : c.deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3))

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_analyticLedger {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : UnconditionalActualFairCachedStoppedAnalyticLedger c.law c.actual c.canonical c.source c.deviation c.clipping c.bad

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_verifierLedger {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : UnconditionalActualFairCachedSourceVerifierLedger G n S D c.effect c.actual c.source

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_physicalBranch {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) (flag : ExactSourceSharedFlag X Y A B D c.sampler.denominator) (x : X) (y : Y) (matching : exactSourcePermutationMatched D c.sampler.denominator c.sampler.numerator ⋯ (flag, x, y) = true) : ∑ j : Fin c.stopping.L, quadraticExpectation (c.effect (exactSourceAliceSampleTuple D c.sampler.denominator c.sampler.numerator ⋯ (flag, x, y), j)) (c.actual (exactSourceAliceSampleTuple D c.sampler.denominator c.sampler.numerator ⋯ (flag, x, y), j)) ≤ ∑ j : Fin c.stopping.L, quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G (c.PA flag) (c.PB flag) j.succ j.succ x y)) (actualStoppingBranchVector (actualStoppingQuestionLocalAction (c.U flag x) (c.V flag y) (c.prepared flag)) j.succ j.succ)

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingContext_stoppedVerifier {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)} {alpha gamma : ℝ} (c : UnconditionalActualFairSourceRoundingContext G n S D alpha gamma) : 1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √c.deviation + 2 * √c.clipping) ≤ c.rounded.winProbability

theorem QuantumParallelRepetition.unconditionalActualFairSourceRoundingData_exists_stoppedVerifier {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) (alpha gamma : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) (failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2) : ∃ (deviation : ℝ) (clipping : ℝ) (rounded : Strategy G), deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) ∧ clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2) ∧ 1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 2 * √clipping) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_small {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) (alpha gamma : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (gamma_positive : 0 < gamma) (small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1) (failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2) : ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.unconditionalSourceOneGameRounding_uniform : ∃ (K : ℝ), 1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)), 0 < (Finset.univ \ D).card → 0 < repeatedPostselectionMass G n S D → ∀ (alpha gamma : ℝ), 0 < alpha → alpha ≤ 1 → 0 < gamma → uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 → ∃ (rounded : Strategy G), roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability

theorem QuantumParallelRepetition.pdf_distributionUniformExponential_unconditional : ∃ (c : ℝ), 0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B), Nonempty A → Nonempty B → 0 < 1 - entangledValue G → ∀ (n : ℕ), 0 < n → repeatedEntangledValue G n ≤ Real.exp (-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

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

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

theorem QuantumParallelRepetition.distributionUniformExponential : ∃ (c : ℝ), 0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B), Nonempty A → Nonempty B → 0 < 1 - entangledValue G → ∀ (n : ℕ), 0 < n → repeatedEntangledValue G n ≤ Real.exp (-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

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