Quantum parallel repetition, part 07

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (i : Fin (L + 1)) : EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The finite outcome encoding for DSV density rational heterogeneous actual common stop scheduled.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_before {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (i : Fin (L + 1)) (before : ↑i < ↑j) : dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j i = dSVDensityRationalCompleteProjectiveOutcome (width (schedule ⟨↑i, ⋯⟩)) N ξ ζ false false

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_hit {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j j.castSucc = dSVDensityRationalCompleteProjectiveOutcome (width (schedule j)) N ξ ζ true true

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_after {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (i : Fin (L + 1)) (after : ↑j < ↑i) : dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j i = dSVUniformDensityThresholdSharedState N d

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopPhysicalState_eq_outcomeProduct {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (alice bob : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d) : (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (⟨j.succ, alice⟩, ⟨j.succ, bob⟩) = ∏ i : Fin (L + 1), (dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j i).ofLp (alice i, bob i)

theorem QuantumParallelRepetition.dSVDensityRationalPureMatchedFlagIndicator_sum {L : ℕ} (a b : Fin (L + 1)) : (∑ flag : Fin (L + 1), if a = flag ∧ b = flag then 1 else 0) = if a = b then 1 else 0

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_eq_optionalProduct {S d N L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (flagAlice flagBob : Fin (L + 1)) : dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ flagAlice flagBob = ∏ i : Fin (L + 1), ‖dSVDensityRationalCompleteStoppedOptionalOutcome (dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagAlice i) (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagBob i)‖ ^ 2

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysical_firstHitProduct {L : ℕ} (continuation : ℕ → ℝ) (success : ℝ) (j : Fin L) : (∏ i : Fin (L + 1), if ↑i < ↑j then continuation ↑i else if ↑i = ↑j then success else 1) = dSVHeterogeneousRealPrefix continuation ↑j * success

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalMatchedCopyBorn {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (i : Fin (L + 1)) : ‖dSVDensityRationalCompleteStoppedOptionalOutcome (dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L j.succ i) (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L j.succ i)‖ ^ 2 = if ↑i < ↑j then dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑i else if ↑i = ↑j then dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j else 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_succ_succ_eq_stage {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalNoHitCopyBorn {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (i : Fin (L + 1)) : ‖dSVDensityRationalCompleteStoppedOptionalOutcome (dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L 0 i) (dSVDensityRationalCompleteStoppedOptionalLocalSchedule L 0 i)‖ ^ 2 = if ↑i < L then dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑i else 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_zero_zero_eq_terminal {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ 0 0 = dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalMatchedFlagMass_eq_stoppedSuccess {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ∑ j : Fin L, dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBorn_mass_partition {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ 0 0 + ∑ j : Fin L, dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAsynchronousFlagMass_eq_stoppedAsynchronousMass {S d N L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ = dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalLocalAction_real_smul {n : ℕ} (A B : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (r : ℝ) (z : EuclideanSpace ℂ (Fin n × Fin n)) : localUnitaryAction A B (r • z) = r • localUnitaryAction A B z

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor_real_smul {N : ℕ} (n : ℕ) (r : ℝ) (z : EuclideanSpace ℂ (Fin N × Fin N)) : dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (r • z) = r • dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n z

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalRawHarmonicTensor_eq {N : ℕ} (grid : 0 < N) (n : ℕ) (rank : Fin (N + 1)) : dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (dSVCanonicalFailurePrefix rank) = √↑↑rank • tensorEmbezzlementTarget (dSVCanonicalFailureUnitRankFamily N grid rank)

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState_apply {d N n : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) (k l : Fin N) (a b : Fin n) : (dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState w n ξ ζ).ofLp (⟨i, finProdFinEquiv (k, a)⟩, ⟨j, finProdFinEquiv (l, b)⟩) = (dSVDensityRationalCanonicalPrefixSpectralOutcome w N ξ ζ).ofLp (⟨k, i⟩, ⟨l, j⟩) * (embezzlementState n).ofLp (a, b)

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalRankWeightedAtomError_eq {N n : ℕ} (grid : 0 < N) (rank : Fin (N + 1)) (A B : ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) : ‖localUnitaryAction A B (dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (dSVCanonicalFailurePrefix rank)) - √↑↑rank • embezzlementState (N * n)‖ ^ 2 = ↑↑rank * ‖localUnitaryAction A B (tensorEmbezzlementTarget (dSVCanonicalFailureUnitRankFamily N grid rank)) - embezzlementState (N * n)‖ ^ 2

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentMixedState {d N B : ℕ} (w : ℝ) (n : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (((_ : Fin B × Fin d) × Fin (N * n)) × (_ : Fin B × Fin d) × Fin (N * n))

The quantum state representing DSV density rational public bucket physical coherent mixed.

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentTargetState {d N B : ℕ} (w : ℝ) (n : ℕ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (((_ : Fin B × Fin d) × Fin (N * n)) × (_ : Fin B × Fin d) × Fin (N * n))

The quantum state representing DSV density rational public bucket physical coherent target.

Equations

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

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

The DSV density rational public bucket physical coherent local reset construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicShiftedResidue_sum {B : ℕ} (positive : 0 < B) (a : ℕ) : ∑ phase : Fin B, (a + ↑phase) % B = ∑ phase : Fin B, ↑phase

theorem QuantumParallelRepetition.dSVDensityRationalPublicShiftedQuotient_sum {B : ℕ} (positive : 0 < B) (a : ℕ) : ∑ phase : Fin B, (a + ↑phase) / B = a

theorem QuantumParallelRepetition.dSVDensityRationalPublicShiftedQuotient_real_sum {B : ℕ} (positive : 0 < B) (a : ℕ) : ∑ phase : Fin B, ↑((a + ↑phase) / B) = ↑a

theorem QuantumParallelRepetition.dSVDensityRationalPublicShiftedBucketMismatch_sum_le {B : ℕ} (positive : 0 < B) (a b : ℕ) : (∑ phase : Fin B, if (a + ↑phase) / B = (b + ↑phase) / B then 0 else 1) ≤ |↑a - ↑b|

theorem QuantumParallelRepetition.dSVDensityRationalPublicShiftedBucketMismatch_average_le {B : ℕ} (positive : 0 < B) (a b : ℕ) : (∑ phase : Fin B, 1 / ↑B * if (a + ↑phase) / B = (b + ↑phase) / B then 0 else 1) ≤ |↑a - ↑b| / ↑B

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

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

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

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_rank_ratio_lt {N B Q : ℕ} (positive_Q : 0 < Q) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) : ↑↑r / ↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) < Real.exp ((↑B + 1) / ↑Q)

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

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

theorem QuantumParallelRepetition.exists_proofDSVDensityRationalHeterogeneousCommonStopSpectralGaugeContinuity_sq {d N B : ℕ} (grid : 0 < N) (dimension : 0 < d) (phases : 0 < B) {Q : ℕ} (fine : 0 < Q) (ε : ℝ) (precision : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∃ (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ {S L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L), ‖dSVDensityRationalPublicBucketPhysicalCoherentLocalReset Q (width (schedule k)) ξ ζ A C (dSVDensityRationalPublicBucketPhysicalCoherentMixedState (width (schedule k)) n ξ ζ) - dSVDensityRationalPublicBucketPhysicalCoherentTargetState (width (schedule k)) n ξ ζ‖ ^ 2 ≤ (10 + 8 * (↑Q / ↑B)) * dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ + (4 * ε ^ 2 + 16 * (Real.exp ((↑B + 1) / ↑Q) - 1) + 8 / ↑B) * dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

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

The DSV density rational heterogeneous common stop gauge stage error construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalDiagonalSurvival_budget {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ∑ k : Fin L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑k * dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ 1

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

The state vector representing DSV density rational heterogeneous stopped common prefix failure.

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureVector_apply {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (q : Fin ↑j → DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d) : (dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureVector width schedule ξ ζ j).ofLp q = ∏ i : Fin ↑j, (dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j ⟨↑i, ⋯⟩).ofLp (q i)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureVector_norm_sq {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : ‖dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureVector width schedule ξ ζ j‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j

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

The DSV density rational heterogeneous stopped common prefix hazard construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exists_proofDSVDensityRationalHeterogeneousStoppedCommonPrefixHazardBound {d N B : ℕ} (grid : 0 < N) (dimension : 0 < d) (phases : 0 < B) {Q : ℕ} (fine : 0 < Q) (ε : ℝ) (precision : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∃ (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ {S L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d), dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q n width schedule ξ ζ A C ≤ (10 + 8 * (↑Q / ↑B)) * dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ + (4 * ε ^ 2 + 16 * (Real.exp ((↑B + 1) / ↑Q) - 1) + 8 / ↑B)

theorem QuantumParallelRepetition.unconditionalPublicBucket_exp_sub_one_le {u : ℝ} (nonnegative : 0 ≤ u) (bounded : u ≤ 1) : Real.exp u - 1 ≤ (Real.exp 1 - 1) * u

theorem QuantumParallelRepetition.exists_proofUnconditionalStoppedCommonPrefixBalancedHazard {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (t : ℝ) (positive : 0 < t) (bounded : t ≤ 1) (precision : ℝ) (precision_positive : 0 < precision) : ∃ (B : ℕ) (Q : ℕ) (n : ℕ), 0 < B ∧ 0 < Q ∧ 0 < n ∧ ∃ (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ {S L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d), dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q n width schedule ξ ζ A C ≤ 34 / t * dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ + 4 * precision ^ 2 + (16 * (Real.exp 1 - 1) + 4) * t

noncomputable def QuantumParallelRepetition.unconditionalPrefactorBucketCoefficient : ℝ

The unconditional prefactor bucket coefficient construction used in the quantum parallel- repetition argument.

Equations

• QuantumParallelRepetition.unconditionalPrefactorBucketCoefficient = 16 * (Real.exp 1 - 1) + 4

theorem QuantumParallelRepetition.unconditionalPrefactorBucketCoefficient_nonneg : 0 ≤ unconditionalPrefactorBucketCoefficient

theorem QuantumParallelRepetition.unconditionalPrefactor_fourthRoot_sq {a : ℝ} (nonnegative : 0 ≤ a) : (a ^ (1 / 4)) ^ 2 = √a

theorem QuantumParallelRepetition.unconditionalPrefactor_sixtyFour_fourthRoot_le : 64 ^ (1 / 4) ≤ 4

theorem QuantumParallelRepetition.unconditionalPrefactor_fourthRoot_async_le {eta alpha : ℝ} (eta_nonnegative : 0 ≤ eta) (alpha_nonnegative : 0 ≤ alpha) : (64 * √eta + alpha ^ (1 / 3)) ^ (1 / 4) ≤ 4 * eta ^ (1 / 8) + alpha ^ (1 / 12)

theorem QuantumParallelRepetition.unconditionalPrefactor_fourthRoot_async_le_twelfth {eta alpha : ℝ} (eta_nonnegative : 0 ≤ eta) (eta_bounded : eta ≤ 1) (alpha_nonnegative : 0 ≤ alpha) : (64 * √eta + alpha ^ (1 / 3)) ^ (1 / 4) ≤ 4 * eta ^ (1 / 12) + alpha ^ (1 / 12)

theorem QuantumParallelRepetition.unconditionalPrefactor_balancedHazard_sqrt_le {a rho : ℝ} (positive : 0 < a) (rho_nonnegative : 0 ≤ rho) : √(34 / √a * a + 4 * rho ^ 2 + unconditionalPrefactorBucketCoefficient * √a) ≤ √(34 + unconditionalPrefactorBucketCoefficient) * a ^ (1 / 4) + 2 * rho

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

theorem QuantumParallelRepetition.unconditionalPrefactor_largeVerifier_twelfthRoot_le {eta alpha : ℝ} (eta_nonnegative : 0 ≤ eta) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) (large : 1 < 64 * √eta + alpha ^ (1 / 3)) : 2 ≤ 128 * (eta ^ (1 / 12) + alpha ^ (1 / 12))

theorem QuantumParallelRepetition.unconditionalExactSourceScalarClipping (d : ℕ) (dimension : 0 < d) (alpha : ℝ) (alpha_positive : 0 < alpha) (alpha_bounded : alpha ≤ 1) : ∃ (w : ℝ) (N : ℕ), 1 ≤ w ∧ 0 < N ∧ 2 * (w + 1) * (↑d / ↑N) ≤ alpha ^ (1 / 3) ∧ 1 / w + ↑d * w / ↑N ≤ 3 * alpha ^ (1 / 3) / 2 ∧ (∀ (ξ : BipartiteUnitVector d), ‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 ≤ 3 * alpha ^ (1 / 3) / 2) ∧ ∀ (ξ ζ : BipartiteUnitVector d), dSVDensityRationalLeftProjectiveThresholdAtomMismatch w N ξ ζ / dSVDensityRationalLeftProjectiveDiagonalMass w N ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + alpha ^ (1 / 3)

noncomputable def QuantumParallelRepetition.exactLocallySampleableJARounded {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 : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

The exact locally sampleable ja rounded construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactLocallySampleableJBRounded {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 : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

The exact locally sampleable jb rounded construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactLocallySampleableJA_rounded_totalVariation_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) (base : ExactHistoryFlag X Y A B D) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) {gamma : ℝ} (approximation : ∀ (k : ExactLocalSamplerIndex X Y D), (Pinsker.finiteTotalVariation (exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) k) fun (r : ExactHistoryFlag X Y A B D) => ↑(numerator k r) / ↑denominator) < gamma) : Pinsker.finiteTotalVariation (exactLocallySampleableJA G n S D base) (exactLocallySampleableJARounded G n D denominator numerator) ≤ gamma

theorem QuantumParallelRepetition.exactLocallySampleableJB_rounded_totalVariation_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) (base : ExactHistoryFlag X Y A B D) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) {gamma : ℝ} (approximation : ∀ (k : ExactLocalSamplerIndex X Y D), (Pinsker.finiteTotalVariation (exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) k) fun (r : ExactHistoryFlag X Y A B D) => ↑(numerator k r) / ↑denominator) < gamma) : Pinsker.finiteTotalVariation (exactLocallySampleableJB G n S D base) (exactLocallySampleableJBRounded G n D denominator numerator) ≤ gamma

theorem QuantumParallelRepetition.exactLocallySampleableRounded_pair_totalVariation {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 : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) : Pinsker.finiteTotalVariation (exactLocallySampleableJARounded G n D denominator numerator) (exactLocallySampleableJBRounded G n D denominator numerator) = ∑ c : LocalQuestionContext X Y D, localQuestionWeight G n D c * Pinsker.finiteTotalVariation (fun (r : ExactHistoryFlag X Y A B D) => ↑(numerator (Sum.inl (c.1, c.2.1)) r) / ↑denominator) fun (r : ExactHistoryFlag X Y A B D) => ↑(numerator (Sum.inr (c.1, c.2.2)) r) / ↑denominator

noncomputable def QuantumParallelRepetition.exactLocallySampleablePermutationMismatch {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 : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) : ℝ

The exact locally sampleable permutation mismatch construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactLocallySampleablePermutationMismatch_le_two_tv {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 : Finset (Fin n)) (denominator : ℕ) (positive : 0 < denominator) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (normalized : ∀ (k : ExactLocalSamplerIndex X Y D), ∑ r : ExactHistoryFlag X Y A B D, numerator k r = denominator) (nonempty : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) : exactLocallySampleablePermutationMismatch G n D denominator numerator nonempty ≤ 2 * Pinsker.finiteTotalVariation (exactLocallySampleableJARounded G n D denominator numerator) (exactLocallySampleableJBRounded G n D denominator numerator)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactSourceSharedFlag (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (denominator : ℕ) : Type

The type used to represent exact source shared flag in the exact sampling construction.

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceSharedFlagWeight {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (denominator : ℕ) : ExactSourceSharedFlag X Y A B D denominator → ℝ

The probability weight for exact source shared flag.

Equations

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

theorem QuantumParallelRepetition.exactSourceSharedFlagWeight_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (denominator : ℕ) (j : ExactSourceSharedFlag X Y A B D denominator) : 0 ≤ exactSourceSharedFlagWeight D denominator j

theorem QuantumParallelRepetition.exactSourceSharedFlagWeight_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (denominator : ℕ) : ∑ j : ExactSourceSharedFlag X Y A B D denominator, exactSourceSharedFlagWeight D denominator j = 1

noncomputable def QuantumParallelRepetition.exactSourceAlicePermutationHistory {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 : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) (j : ExactSourceSharedFlag X Y A B D denominator) (x : X) : ExactHistoryFlag X Y A B D

The transcript representation for exact source alice permutation.

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceBobPermutationHistory {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 : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) (j : ExactSourceSharedFlag X Y A B D denominator) (y : Y) : ExactHistoryFlag X Y A B D

The transcript representation for exact source bob permutation.

Equations

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

noncomputable def QuantumParallelRepetition.exactSourcePermutationMatched {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 : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) (ω : ExactSourceSharedFlag X Y A B D denominator × X × Y) : Bool

The exact source permutation matched construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactSourcePermutationMatched_eq_true_iff {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 : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) (ω : ExactSourceSharedFlag X Y A B D denominator × X × Y) : exactSourcePermutationMatched D denominator numerator nonempty ω = true ↔ exactSourceAlicePermutationHistory D denominator numerator nonempty ω.1 ω.2.1 = exactSourceBobPermutationHistory D denominator numerator nonempty ω.1 ω.2.2

The Boolean shared-permutation test reflects equality of the two decoded histories.

theorem QuantumParallelRepetition.exactUniformPermutationProbability_eq_indicator_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (event : Equiv.Perm ι → Prop) : ClassicalSampling.uniformPermutationProbability event = (∑ permutation : Equiv.Perm ι, if event permutation then 1 else 0) / ↑(Fintype.card (Equiv.Perm ι))

theorem QuantumParallelRepetition.exactSourceSharedFlag_mismatch_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) : (∑ ω : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) ω * if exactSourcePermutationMatched D denominator numerator nonempty ω = true then 0 else 1) = exactLocallySampleablePermutationMismatch G n D denominator numerator nonempty

theorem QuantumParallelRepetition.exactSourceSharedFlag_mismatch_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (denominator : ℕ) (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ) (nonempty : ∀ (k : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator k)).Nonempty) {lam : ℝ} (mismatch : exactLocallySampleablePermutationMismatch G n D denominator numerator nonempty ≤ 4 * lam) : (∑ ω : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) ω * if exactSourcePermutationMatched D denominator numerator nonempty ω = true then 0 else 1) ≤ 4 * lam

theorem QuantumParallelRepetition.reweightedSeed_reverse_source_prefix_information_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] {K : Type u_5} {V : Type u_6} [Fintype K] [Fintype V] (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) (seedLaw : Finset (SourceRemainingCoordinate D) → FiniteEventLaw K) (Ω : Finset (SourceRemainingCoordinate D) → Type u_7) [(side : Finset (SourceRemainingCoordinate D)) → Fintype (Ω side)] (projection : (side : Finset (SourceRemainingCoordinate D)) → K × ExactOutcome X Y A B n → Ω side × (Fin side.card → V)) (default : V) : ∑ side : Finset (SourceRemainingCoordinate D), reversePartitionWeight side * ((∑ k : Fin side.card, reweightedSeedPrefixEntropyIncrement (seedLaw side) G n S D (projection side) default k) / ↑side.card) ≤ 2 * (postselectionLogCost G n S D + answerLogCost D) / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.exactIndependentCoordinateQuestion_marginal {M : Type u_5} {Ω : Type u_6} {V : Type u_7} [Fintype M] [DecidableEq M] [Fintype Ω] (outcome : Ω → ℝ) (question : Ω → M → V) (i : M) (v : V) : ClassicalInformation.groupedMass (fun (t : ExactForwardSeed M × Ω) => (t.1.coordinate, question t.2 t.1.coordinate)) (fun (t : ExactForwardSeed M × Ω) => exactSeedWeight t.1 * outcome t.2) (i, v) = 1 / ↑(Fintype.card M) * ClassicalInformation.groupedMass (fun (ω : Ω) => question ω i) outcome v

theorem QuantumParallelRepetition.strategyAliceQuestionPrior_marginal {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : Strategy G) (x : X) : ClassicalInformation.groupedMass (fun (ω : StrategyOutcome X Y A B) => ω.1) (strategyEventLaw G S).weight x = G.marginalX x

theorem QuantumParallelRepetition.strategyBobQuestionPrior_marginal {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : Strategy G) (y : Y) : ClassicalInformation.groupedMass (fun (ω : StrategyOutcome X Y A B) => ω.2.1) (strategyEventLaw G S).weight y = G.marginalY y

theorem QuantumParallelRepetition.exactGroupedMass_equiv {Ω : Type u_5} {K : Type u_6} {V : Type u_7} [Fintype Ω] [Fintype K] (equiv : Ω ≃ K) (projection : Ω → V) (mass : Ω → ℝ) (v : V) : ClassicalInformation.groupedMass (fun (k : K) => projection (equiv.symm k)) (fun (k : K) => mass (equiv.symm k)) v = ClassicalInformation.groupedMass projection mass v

theorem QuantumParallelRepetition.exactAliceInformationPosterior_firstMarginal_pushforward {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)) (i : SourceRemainingCoordinate D) (x : X) : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) = ClassicalInformation.groupedMass (fun (t : ExactLocallySampleableTuple X Y A B D) => (t.1, t.2.1)) (exactLocallySampleableLaw G n S D) (i, x)

theorem QuantumParallelRepetition.exactBobInformationPosterior_firstMarginal_pushforward {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)) (i : SourceRemainingCoordinate D) (y : Y) : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) = ClassicalInformation.groupedMass (fun (t : ExactLocallySampleableTuple X Y A B D) => (t.1, t.2.2.1)) (exactLocallySampleableLaw G n S D) (i, y)

theorem QuantumParallelRepetition.exactAliceInformationPosterior_firstMarginal {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)) (i : SourceRemainingCoordinate D) (x : X) : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) = 1 / ↑(Fintype.card (SourceRemainingCoordinate D)) * ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.1 ↑i) (repeatedConditionedOutcomeLaw G n S D) x

theorem QuantumParallelRepetition.exactBobInformationPosterior_firstMarginal {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)) (i : SourceRemainingCoordinate D) (y : Y) : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) = 1 / ↑(Fintype.card (SourceRemainingCoordinate D)) * ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.2.1 ↑i) (repeatedConditionedOutcomeLaw G n S D) y

theorem QuantumParallelRepetition.finiteUniformCoordinate_relativeEntropy {ι : Type u_5} {V : Type u_6} [Fintype ι] [Fintype V] (positive : 0 < Fintype.card ι) (posterior : ι → V → ℝ) (prior : V → ℝ) : (Pinsker.finiteRelativeEntropy (fun (t : ι × V) => 1 / ↑(Fintype.card ι) * posterior t.1 t.2) fun (t : ι × V) => 1 / ↑(Fintype.card ι) * prior t.2) = 1 / ↑(Fintype.card ι) * ∑ i : ι, Pinsker.finiteRelativeEntropy (posterior i) prior

theorem QuantumParallelRepetition.sourceRemaining_nonnegative_sum_le {n : ℕ} (D : Finset (Fin n)) (f : Fin n → ℝ) (nonnegative : ∀ (j : Fin n), 0 ≤ f j) : ∑ i : SourceRemainingCoordinate D, f ↑i ≤ ∑ j : Fin n, f j

theorem QuantumParallelRepetition.exactAliceSourceMarginalInformation_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) (base : ExactHistoryFlag X Y A B D) : exactAliceSourceMarginalInformation G n S D base ≤ postselectionLogCost G n S D / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.exactBobSourceMarginalInformation_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) (base : ExactHistoryFlag X Y A B D) : exactBobSourceMarginalInformation G n S D base ≤ postselectionLogCost G n S D / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.exact_source_equation_twenty_three_of_conditioned_reverse_prefix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {KA : Type u_5} {KB : Type u_6} [Fintype KA] [Fintype KB] (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) (seedLawA : Finset (SourceRemainingCoordinate D) → FiniteEventLaw KA) (seedLawB : Finset (SourceRemainingCoordinate D) → FiniteEventLaw KB) (ΩA : Finset (SourceRemainingCoordinate D) → Type u_7) (ΩB : Finset (SourceRemainingCoordinate D) → Type u_8) [(side : Finset (SourceRemainingCoordinate D)) → Fintype (ΩA side)] [(side : Finset (SourceRemainingCoordinate D)) → Fintype (ΩB side)] (projectionA : (side : Finset (SourceRemainingCoordinate D)) → KA × ExactOutcome X Y A B n → ΩA side × (Fin side.card → Y)) (projectionB : (side : Finset (SourceRemainingCoordinate D)) → KB × ExactOutcome X Y A B n → ΩB side × (Fin side.card → X)) (defaultY : Y) (defaultX : X) (aliceConditionedReverseIdentification : exactAliceSourceConditionalInformation G n S D base = ∑ side : Finset (SourceRemainingCoordinate D), reversePartitionWeight side * ((∑ k : Fin side.card, reweightedSeedPrefixEntropyIncrement (seedLawA side) G n S D (projectionA side) defaultY k) / ↑side.card)) (bobConditionedReverseIdentification : exactBobSourceConditionalInformation G n S D base = ∑ side : Finset (SourceRemainingCoordinate D), reversePartitionWeight side * ((∑ k : Fin side.card, reweightedSeedPrefixEntropyIncrement (seedLawB side) G n S D (projectionB side) defaultX k) / ↑side.card)) : ExactSourceClassicalInformationBound G n S D base

noncomputable def QuantumParallelRepetition.exactConditionedReverseAlicePrefixEntropyIncrement {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) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (k : Fin side.card) : ℝ

The information increment contributed by exact conditioned reverse alice prefix entropy.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseBobPrefixEntropyIncrement {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) (side : Finset (SourceRemainingCoordinate D)) (default : X) (k : Fin side.card) : ℝ

The information increment contributed by exact conditioned reverse bob prefix entropy.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseAlicePrefixInformation {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) (default : Y) : ℝ

The exact conditioned reverse alice prefix information construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseBobPrefixInformation {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) (default : X) : ℝ

The exact conditioned reverse bob prefix information construction used in the quantum parallel- repetition argument.

Equations

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

def QuantumParallelRepetition.ExactReverseAliceConditionalHistoryIdentification {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) (base : ExactHistoryFlag X Y A B D) (default : Y) : Prop

The exact reverse alice conditional history identification construction used in the quantum parallel-repetition argument.

Equations

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

def QuantumParallelRepetition.ExactReverseBobConditionalHistoryIdentification {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) (base : ExactHistoryFlag X Y A B D) (default : X) : Prop

The exact reverse bob conditional history identification construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exact_source_equation_twenty_three_of_actual_conditioned_reindex {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) (base : ExactHistoryFlag X Y A B D) (defaultY : Y) (defaultX : X) (alice : ExactReverseAliceConditionalHistoryIdentification G n S D remaining base defaultY) (bob : ExactReverseBobConditionalHistoryIdentification G n S D remaining base defaultX) : ExactSourceClassicalInformationBound G n S D base

theorem QuantumParallelRepetition.finiteRelativeEntropy_self {I : Type u_1} [Fintype I] (mass : I → ℝ) : Pinsker.finiteRelativeEntropy mass mass = 0

theorem QuantumParallelRepetition.finiteConditionalHistoryRelativeEntropy_eq {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype I] [Fintype R] [Fintype V] (p q : I × R × V → ℝ) (p_nonnegative : ∀ (point : I × R × V), 0 ≤ p point) (q_nonnegative : ∀ (point : I × R × V), 0 ≤ q point) (absolute_continuity : ∀ (point : I × R × V), q point = 0 → p point = 0) (reference : I → R → V → ℝ) (same_history : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) = ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional q i)) (next_reference : ∀ (i : I) (r : R), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r ≠ 0 → ClassicalInformation.jointConditional (ClassicalInformation.jointConditional q i) r = reference i r) : ∑ i : I, ClassicalInformation.jointFirstMarginal p i * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional p i) (ClassicalInformation.jointConditional q i) = ∑ i : I, ClassicalInformation.jointFirstMarginal p i * ∑ r : R, ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.jointConditional p i) r) (reference i r)

theorem QuantumParallelRepetition.finiteSupportedConditionalHistoryReferenceFirstMarginal_eq {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype R] [Fintype V] (p q : I × R × V → ℝ) (q_nonnegative : ∀ (point : I × R × V), 0 ≤ q point) (absolute_continuity : ∀ (point : I × R × V), q point = 0 → p point = 0) (reference : I → R → V → ℝ) (reference_normalized : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R), ∑ v : V, reference i r v = 1) (factor : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R) (v : V), q (i, r, v) = ClassicalInformation.jointFirstMarginal q i * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r * reference i r v) (i : I) (supported : ClassicalInformation.jointFirstMarginal p i ≠ 0) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional q i) = ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i)

theorem QuantumParallelRepetition.finiteSupportedConditionalHistoryReferenceConditional_eq {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype R] [Fintype V] (p q : I × R × V → ℝ) (q_nonnegative : ∀ (point : I × R × V), 0 ≤ q point) (absolute_continuity : ∀ (point : I × R × V), q point = 0 → p point = 0) (reference : I → R → V → ℝ) (reference_normalized : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R), ∑ v : V, reference i r v = 1) (factor : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R) (v : V), q (i, r, v) = ClassicalInformation.jointFirstMarginal q i * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r * reference i r v) (i : I) (r : R) (supported : ClassicalInformation.jointFirstMarginal p i ≠ 0) (history_supported : ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.jointConditional q i) r = reference i r

theorem QuantumParallelRepetition.finiteSupportedConditionalHistoryRelativeEntropy_eq_of_factor {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype I] [Fintype R] [Fintype V] (p q : I × R × V → ℝ) (p_nonnegative : ∀ (point : I × R × V), 0 ≤ p point) (q_nonnegative : ∀ (point : I × R × V), 0 ≤ q point) (absolute_continuity : ∀ (point : I × R × V), q point = 0 → p point = 0) (reference : I → R → V → ℝ) (reference_normalized : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R), ∑ v : V, reference i r v = 1) (factor : ∀ (i : I), ClassicalInformation.jointFirstMarginal p i ≠ 0 → ∀ (r : R) (v : V), q (i, r, v) = ClassicalInformation.jointFirstMarginal q i * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r * reference i r v) : ∑ i : I, ClassicalInformation.jointFirstMarginal p i * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional p i) (ClassicalInformation.jointConditional q i) = ∑ i : I, ClassicalInformation.jointFirstMarginal p i * ∑ r : R, ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional p i) r * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.jointConditional p i) r) (reference i r)

theorem QuantumParallelRepetition.exactAliceInformationPosterior_firstMarginal_eq_localMass {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)) (i : SourceRemainingCoordinate D) (x : X) : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) = exactAliceLocalMass D (exactLocallySampleableLaw G n S D) i x

theorem QuantumParallelRepetition.exactBobInformationPosterior_firstMarginal_eq_localMass {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)) (i : SourceRemainingCoordinate D) (y : Y) : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) = exactBobLocalMass D (exactLocallySampleableLaw G n S D) i y

theorem QuantumParallelRepetition.exactAliceSupportedQuestion_marginal_pos {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) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (x : X) (supported : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) ≠ 0) : 0 < G.marginalX x

theorem QuantumParallelRepetition.exactBobSupportedQuestion_marginal_pos {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) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (y : Y) (supported : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) ≠ 0) : 0 < G.marginalY y

theorem QuantumParallelRepetition.exactAliceInformationPosterior_historyMarginal {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)) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (x : X) (supported : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) ≠ 0) (r : ExactHistoryFlag X Y A B D) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactAliceInformationPosterior G n S D) (i, x)) r = exactAliceLocalConditional D base (exactLocallySampleableLaw G n S D) i x r

theorem QuantumParallelRepetition.exactBobInformationPosterior_historyMarginal {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)) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (y : Y) (supported : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) ≠ 0) (r : ExactHistoryFlag X Y A B D) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactBobInformationPosterior G n S D) (i, y)) r = exactBobLocalConditional D base (exactLocallySampleableLaw G n S D) i y r

theorem QuantumParallelRepetition.exactAliceInformationReference_supported_factor {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)) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (x : X) (supported : ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) (i, x) ≠ 0) (r : ExactHistoryFlag X Y A B D) (y : Y) : exactAliceInformationReference G n S D base ((i, x), r, y) = ClassicalInformation.jointFirstMarginal (exactAliceInformationReference G n S D base) (i, x) * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactAliceInformationPosterior G n S D) (i, x)) r * G.conditionalYGivenX x y

theorem QuantumParallelRepetition.exactBobInformationReference_supported_factor {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)) (base : ExactHistoryFlag X Y A B D) (i : SourceRemainingCoordinate D) (y : Y) (supported : ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) (i, y) ≠ 0) (r : ExactHistoryFlag X Y A B D) (x : X) : exactBobInformationReference G n S D base ((i, y), r, x) = ClassicalInformation.jointFirstMarginal (exactBobInformationReference G n S D base) (i, y) * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactBobInformationPosterior G n S D) (i, y)) r * G.conditionalXGivenY y x

theorem QuantumParallelRepetition.exactAliceSourceConditionalInformation_eq_question {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) (base : ExactHistoryFlag X Y A B D) : exactAliceSourceConditionalInformation G n S D base = ∑ ix : SourceRemainingCoordinate D × X, ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) ix * ∑ r : ExactHistoryFlag X Y A B D, ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactAliceInformationPosterior G n S D) ix) r * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.jointConditional (exactAliceInformationPosterior G n S D) ix) r) (G.conditionalYGivenX ix.2)

theorem QuantumParallelRepetition.exactBobSourceConditionalInformation_eq_question {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) (base : ExactHistoryFlag X Y A B D) : exactBobSourceConditionalInformation G n S D base = ∑ iy : SourceRemainingCoordinate D × Y, ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) iy * ∑ r : ExactHistoryFlag X Y A B D, ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional (exactBobInformationPosterior G n S D) iy) r * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.jointConditional (exactBobInformationPosterior G n S D) iy) r) (G.conditionalXGivenY iy.2)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactReverseAliceNextContext (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max (max (max u_8 u_7) u_6 u_5) u_6)

The type used to represent exact reverse alice next context in the exact sampling construction.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactReverseBobNextContext (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max (max (max u_8 u_7) u_6 u_5) u_5)

The type used to represent exact reverse bob next context in the exact sampling construction.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseAliceNextJoint {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) (side : Finset (SourceRemainingCoordinate D)) : ExactReverseAliceNextContext X Y A B D side → ℝ

The exact conditioned reverse alice next joint construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseAliceNextPrior {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) (side : Finset (SourceRemainingCoordinate D)) : ExactReverseAliceNextContext X Y A B D side → ℝ

The exact conditioned reverse alice next prior construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseBobNextJoint {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) (side : Finset (SourceRemainingCoordinate D)) : ExactReverseBobNextContext X Y A B D side → ℝ

The exact conditioned reverse bob next joint construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactConditionedReverseBobNextPrior {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) (side : Finset (SourceRemainingCoordinate D)) : ExactReverseBobNextContext X Y A B D side → ℝ

The exact conditioned reverse bob next prior construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.exactReverseAliceMaskedProjection_eq_of_history {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (default : Y) (q q' : ExactJointOutcome X Y A B D) (same_history : exactHistoryCode D q = exactHistoryCode D q') (same_question : q.2.1 ↑q.1.coordinate = q'.2.1 ↑q'.1.coordinate) : finitePrefixMask default ((exactReverseAliceContext q.1).sideRank ⟨q.1.coordinate, ⋯⟩).castSucc (exactReverseAliceSourceProjection D (exactReverseLeftSide q.1) q) = finitePrefixMask default ((exactReverseAliceContext q.1).sideRank ⟨q.1.coordinate, ⋯⟩).castSucc (exactReverseAliceSourceProjection D (exactReverseLeftSide q.1) q')

theorem QuantumParallelRepetition.exactReverseBobMaskedProjection_eq_of_history {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (default : X) (q q' : ExactJointOutcome X Y A B D) (same_history : exactHistoryCode D q = exactHistoryCode D q') (same_question : q.2.2.1 ↑q.1.coordinate = q'.2.2.1 ↑q'.1.coordinate) : finitePrefixMask default ((exactReverseBobContext q.1).sideRank ⟨q.1.coordinate, ⋯⟩).castSucc (exactReverseBobSourceProjection D (exactReverseRightSide q.1) q) = finitePrefixMask default ((exactReverseBobContext q.1).sideRank ⟨q.1.coordinate, ⋯⟩).castSucc (exactReverseBobSourceProjection D (exactReverseRightSide q.1) q')

theorem QuantumParallelRepetition.groupedMass_product_injective_seed {K : Type u_1} {Ω : Type u_2} {C : Type u_3} {T : Type u_4} [Fintype K] [Fintype Ω] [DecidableEq C] [DecidableEq T] (code : K → C) (injective : Function.Injective code) (projection : K → Ω → T) (seedWeight : K → ℝ) (outcomeWeight : Ω → ℝ) (seed : K) (target : T) : ClassicalInformation.groupedMass (fun (q : K × Ω) => (code q.1, projection q.1 q.2)) (fun (q : K × Ω) => seedWeight q.1 * outcomeWeight q.2) (code seed, target) = seedWeight seed * ClassicalInformation.groupedMass (projection seed) outcomeWeight target

theorem QuantumParallelRepetition.jointConditional_groupedMass_eq_of_fiber {Ω : Type u_1} {C : Type u_2} {D : Type u_3} {V : Type u_4} [Fintype Ω] [Fintype V] [DecidableEq (C × V)] [DecidableEq (D × V)] (mass : Ω → ℝ) (left : Ω → C) (right : Ω → D) (next : Ω → V) (leftTarget : C) (rightTarget : D) (same_fiber : ∀ (outcome : Ω), left outcome = leftTarget ↔ right outcome = rightTarget) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : Ω) => (left outcome, next outcome)) mass) leftTarget = ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : Ω) => (right outcome, next outcome)) mass) rightTarget

noncomputable def QuantumParallelRepetition.exactReverseAliceMarkedHistoryContext {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)) (default : Y) (seed : ExactRemainingSeed D) (outcome : ExactOutcome X Y A B n) : ExactReverseAliceNextContext X Y A B D (exactReverseLeftSide seed)

The data context recording exact reverse alice marked history.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobMarkedHistoryContext {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)) (default : X) (seed : ExactRemainingSeed D) (outcome : ExactOutcome X Y A B n) : ExactReverseBobNextContext X Y A B D (exactReverseRightSide seed)

The data context recording exact reverse bob marked history.

Equations

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

theorem QuantumParallelRepetition.exactConditionedAnswerFlag_eq_of_history {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)) (q q' : ExactJointOutcome X Y A B D) (same_history : exactHistoryCode D q = exactHistoryCode D q') : repeatedConditionedAnswerFlag G n S D q.2 = repeatedConditionedAnswerFlag G n S D q'.2

theorem QuantumParallelRepetition.exactReverseAliceMarkedHistoryContext_eq_of_history {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)) (default : Y) (seed : ExactRemainingSeed D) (outcome outcome' : ExactOutcome X Y A B n) (same_history : exactHistoryCode D (seed, outcome) = exactHistoryCode D (seed, outcome')) (same_question : outcome.1 ↑seed.coordinate = outcome'.1 ↑seed.coordinate) : exactReverseAliceMarkedHistoryContext G n S D default seed outcome = exactReverseAliceMarkedHistoryContext G n S D default seed outcome'

theorem QuantumParallelRepetition.exactReverseBobMarkedHistoryContext_eq_of_history {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)) (default : X) (seed : ExactRemainingSeed D) (outcome outcome' : ExactOutcome X Y A B n) (same_history : exactHistoryCode D (seed, outcome) = exactHistoryCode D (seed, outcome')) (same_question : outcome.2.1 ↑seed.coordinate = outcome'.2.1 ↑seed.coordinate) : exactReverseBobMarkedHistoryContext G n S D default seed outcome = exactReverseBobMarkedHistoryContext G n S D default seed outcome'

theorem QuantumParallelRepetition.exactReverseAlice_history_of_marked_context {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)) (default : Y) (seed : ExactRemainingSeed D) (outcome outcome' : ExactOutcome X Y A B n) (same_context : exactReverseAliceMarkedHistoryContext G n S D default seed outcome = exactReverseAliceMarkedHistoryContext G n S D default seed outcome') : outcome.1 ↑seed.coordinate = outcome'.1 ↑seed.coordinate ∧ exactHistoryCode D (seed, outcome) = exactHistoryCode D (seed, outcome')

theorem QuantumParallelRepetition.exactReverseBob_history_of_marked_context {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)) (default : X) (seed : ExactRemainingSeed D) (outcome outcome' : ExactOutcome X Y A B n) (same_context : exactReverseBobMarkedHistoryContext G n S D default seed outcome = exactReverseBobMarkedHistoryContext G n S D default seed outcome') : outcome.2.1 ↑seed.coordinate = outcome'.2.1 ↑seed.coordinate ∧ exactHistoryCode D (seed, outcome) = exactHistoryCode D (seed, outcome')

theorem QuantumParallelRepetition.exactReverseAliceMarkedHistoryContext_fiber_iff {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)) (default : Y) (seed : ExactRemainingSeed D) (outcome reference : ExactOutcome X Y A B n) : exactReverseAliceMarkedHistoryContext G n S D default seed outcome = exactReverseAliceMarkedHistoryContext G n S D default seed reference ↔ (outcome.1 ↑seed.coordinate, exactHistoryCode D (seed, outcome)) = (reference.1 ↑seed.coordinate, exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseBobMarkedHistoryContext_fiber_iff {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)) (default : X) (seed : ExactRemainingSeed D) (outcome reference : ExactOutcome X Y A B n) : exactReverseBobMarkedHistoryContext G n S D default seed outcome = exactReverseBobMarkedHistoryContext G n S D default seed reference ↔ (outcome.2.1 ↑seed.coordinate, exactHistoryCode D (seed, outcome)) = (reference.2.1 ↑seed.coordinate, exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseAliceMarkedPosteriorConditional_eq_sourceFiber {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)) (default : Y) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => (exactReverseAliceMarkedHistoryContext G n S D default seed outcome, outcome.2.1 ↑seed.coordinate)) (repeatedConditionedOutcomeLaw G n S D)) (exactReverseAliceMarkedHistoryContext G n S D default seed reference) = ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => ((outcome.1 ↑seed.coordinate, exactHistoryCode D (seed, outcome)), outcome.2.1 ↑seed.coordinate)) (repeatedConditionedOutcomeLaw G n S D)) (reference.1 ↑seed.coordinate, exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseBobMarkedPosteriorConditional_eq_sourceFiber {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)) (default : X) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => (exactReverseBobMarkedHistoryContext G n S D default seed outcome, outcome.1 ↑seed.coordinate)) (repeatedConditionedOutcomeLaw G n S D)) (exactReverseBobMarkedHistoryContext G n S D default seed reference) = ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => ((outcome.2.1 ↑seed.coordinate, exactHistoryCode D (seed, outcome)), outcome.1 ↑seed.coordinate)) (repeatedConditionedOutcomeLaw G n S D)) (reference.2.1 ↑seed.coordinate, exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.reweightedSeedPrefixPrior_as_flagged_pushforward {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} {Ω : Type u_6} {V : Type u_7} [Fintype K] {h : ℕ} (seedLaw : FiniteEventLaw K) (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V)) (t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V)) : reweightedSeedPrefixPrior seedLaw G n S D projection t = ClassicalInformation.groupedMass (fun (q : ConditionedAnswerFlag A B D × K × ExactOutcome X Y A B n) => (((projection q.2).1, q.1), (projection q.2).2)) (fun (q : ConditionedAnswerFlag A B D × K × ExactOutcome X Y A B n) => finiteUniformWeight (ConditionedAnswerFlag A B D) * (reweightedSeedPriorEventLaw seedLaw G n S).weight q.2) t

theorem QuantumParallelRepetition.reweightedSeedPrefixPrior_next_flagged_pushforward {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} {Ω : Type u_6} {V : Type u_7} [Fintype K] [Fintype Ω] [Fintype V] {h : ℕ} (seedLaw : FiniteEventLaw K) (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V)) (default : V) (k : Fin h) (target : ((Ω × ConditionedAnswerFlag A B D) × (Fin h → V)) × V) : ClassicalInformation.groupedMass (exactPrefixNextCode default k) (reweightedSeedPrefixPrior seedLaw G n S D projection) target = ClassicalInformation.groupedMass (fun (q : ConditionedAnswerFlag A B D × K × ExactOutcome X Y A B n) => exactPrefixNextCode default k (((projection q.2).1, q.1), (projection q.2).2)) (fun (q : ConditionedAnswerFlag A B D × K × ExactOutcome X Y A B n) => finiteUniformWeight (ConditionedAnswerFlag A B D) * (reweightedSeedPriorEventLaw seedLaw G n S).weight q.2) target

theorem QuantumParallelRepetition.finiteGroupedExpectation_eq_atom_sum {Ω : Type u_1} {C : Type u_2} [Fintype Ω] [Fintype C] [DecidableEq C] (code : Ω → C) (mass : Ω → ℝ) (value : C → ℝ) : ∑ target : C, ClassicalInformation.groupedMass code mass target * value target = ∑ outcome : Ω, mass outcome * value (code outcome)

theorem QuantumParallelRepetition.jointFirstMarginal_groupedContextNext {Ω : Type u_1} {C : Type u_2} {V : Type u_3} [Fintype Ω] [Fintype V] [DecidableEq C] [DecidableEq (C × V)] (context : Ω → C) (next : Ω → V) (mass : Ω → ℝ) (target : C) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (fun (outcome : Ω) => (context outcome, next outcome)) mass) target = ClassicalInformation.groupedMass context mass target

theorem QuantumParallelRepetition.finiteNextInformation_eq_atom_sum {Ω : Type u_1} {C : Type u_2} {V : Type u_3} [Fintype Ω] [Fintype C] [Fintype V] [DecidableEq (C × V)] (context : Ω → C) (next : Ω → V) (mass : Ω → ℝ) (reference : C → V → ℝ) : ∑ target : C, ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (fun (outcome : Ω) => (context outcome, next outcome)) mass) target * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : Ω) => (context outcome, next outcome)) mass) target) (reference target) = ∑ outcome : Ω, mass outcome * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (source : Ω) => (context source, next source)) mass) (context outcome)) (reference (context outcome))

theorem QuantumParallelRepetition.jointAtom_eq_zero_of_firstMarginal_zero {I : Type u_1} {V : Type u_2} [Fintype V] (mass : I × V → ℝ) (nonnegative : ∀ (point : I × V), 0 ≤ mass point) (index : I) (zero : ClassicalInformation.jointFirstMarginal mass index = 0) (value : V) : mass (index, value) = 0

theorem QuantumParallelRepetition.nestedFirstMarginal_mul_conditional {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype R] [Fintype V] (mass : I × R × V → ℝ) (nonnegative : ∀ (point : I × R × V), 0 ≤ mass point) (index : I) (history : R) : ClassicalInformation.jointFirstMarginal mass index * ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional mass index) history = ClassicalInformation.jointFirstMarginal (fun (point : (I × R) × V) => mass (point.1.1, point.1.2, point.2)) (index, history)

theorem QuantumParallelRepetition.nestedConditional_eq_flat {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype R] [Fintype V] (mass : I × R × V → ℝ) (nonnegative : ∀ (point : I × R × V), 0 ≤ mass point) (index : I) (history : R) : ClassicalInformation.jointConditional (ClassicalInformation.jointConditional mass index) history = ClassicalInformation.jointConditional (fun (point : (I × R) × V) => mass (point.1.1, point.1.2, point.2)) (index, history)

theorem QuantumParallelRepetition.finiteNestedNextInformation_eq_atom_sum {I : Type u_1} {R : Type u_2} {V : Type u_3} [Fintype I] [Fintype R] [Fintype V] (mass : I × R × V → ℝ) (nonnegative : ∀ (point : I × R × V), 0 ≤ mass point) (reference : I → V → ℝ) : ∑ index : I, ClassicalInformation.jointFirstMarginal mass index * ∑ history : R, ClassicalInformation.jointFirstMarginal (ClassicalInformation.jointConditional mass index) history * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.jointConditional mass index) history) (reference index) = ∑ point : I × R × V, mass point * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (fun (atom : (I × R) × V) => mass (atom.1.1, atom.1.2, atom.2)) (point.1, point.2.1)) (reference point.1)

theorem QuantumParallelRepetition.reweightedSeedPrefixJoint_as_actual_flagged_pushforward {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} {Ω : Type u_6} {V : Type u_7} [Fintype K] {h : ℕ} (seedLaw : FiniteEventLaw K) (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V)) (target : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V)) : reweightedSeedPrefixJoint seedLaw G n S D projection target = ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => (((projection point).1, repeatedConditionedAnswerFlag G n S D point.2), (projection point).2)) (reweightedSeedPosterior seedLaw G n S D) target

theorem QuantumParallelRepetition.exactAliceSourceConditionalInformation_eq_atom_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) : exactAliceSourceConditionalInformation G n S D base = ∑ point : (SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D × Y, exactAliceInformationPosterior G n S D point * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (fun (atom : ((SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D) × Y) => exactAliceInformationPosterior G n S D (atom.1.1, atom.1.2, atom.2)) (point.1, point.2.1)) (G.conditionalYGivenX point.1.2)

theorem QuantumParallelRepetition.exactBobSourceConditionalInformation_eq_atom_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) (base : ExactHistoryFlag X Y A B D) : exactBobSourceConditionalInformation G n S D base = ∑ point : (SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D × X, exactBobInformationPosterior G n S D point * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (fun (atom : ((SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D) × X) => exactBobInformationPosterior G n S D (atom.1.1, atom.1.2, atom.2)) (point.1, point.2.1)) (G.conditionalXGivenY point.1.2)