theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeightedCrossing_le_one {N B : ℕ} (positive : 0 < B) (Q : ℕ) (r s : Fin (N + 1)) : dSVDensityRationalPublicLogRankPhaseWeightedCrossing Q B r s ≤ 1

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeightedCrossing_alice_le {N B : ℕ} (positive : 0 < B) (Q : ℕ) (r s : Fin (N + 1)) : ↑↑r * dSVDensityRationalPublicLogRankPhaseWeightedCrossing Q B r s ≤ (↑Q / ↑B + 1) * |↑↑r - ↑↑s| + min ↑↑r ↑↑s / ↑B

theorem QuantumParallelRepetition.exists_proofDSVDensityRationalPublicBucketPhysicalQuantitativeMixedPrefixCleanup_sq {N B : ℕ} (grid : 0 < N) (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)) ℂ)), ∀ (r s : Fin (N + 1)), ∑ phase : Fin B, dSVDensityRationalPublicLogRankPhaseWeight B phase * ‖localUnitaryAction (A phase (dSVDensityRationalPublicLogRankBucket Q phase r)) (C phase (dSVDensityRationalPublicLogRankBucket Q phase s)) (dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (dSVCanonicalFailurePrefix (dSVDensityRationalPublicBucketPhysicalCommonRank r s))) - √↑↑r • embezzlementState (N * n)‖ ^ 2 ≤ 2 * |↑↑r - ↑↑s| + 4 * ↑↑r * ε ^ 2 + 16 * ↑↑r * (Real.exp ((↑B + 1) / ↑Q) - 1) + 8 * ((↑Q / ↑B + 1) * |↑↑r - ↑↑s| + min ↑↑r ↑↑s / ↑B)

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

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousCommonStopSpectralAtomWeight N ξ ζ i j = QuantumParallelRepetition.dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j / (↑d * ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousCommonStopSpectralAtomWeight_nonneg {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) : 0 ≤ dSVDensityRationalHeterogeneousCommonStopSpectralAtomWeight N ξ ζ i j

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousCommonStopSpectralRankGap_eq_hazard {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousCommonStopSpectralRankGap N w ξ ζ = dSVDensityRationalPhysicalProjectorCrossHazard N w ξ ζ

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousCommonStopSpectralAliceMass_eq_diagonalBorn {d N : ℕ} (grid : 0 < N) (dimension : 0 < d) (w : ℝ) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousCommonStopSpectralAliceMass N w ξ ζ = dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ

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

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousStoppedCommonStopGaugeError {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)) ℂ)) : ℝ

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

theorem QuantumParallelRepetition.exists_proofDSVDensityRationalHeterogeneousStoppedCommonStopGaugeErrorBound {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), dSVDensityRationalHeterogeneousStoppedCommonStopGaugeError Q n width schedule ξ ζ A C ≤ (10 + 8 * (↑Q / ↑B)) * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ + (4 * ε ^ 2 + 16 * (Real.exp ((↑B + 1) / ↑Q) - 1) + 8 / ↑B)

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

Equations

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

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)

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureCopy_eq_actual {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (i : Fin ↑j) : dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureCopy width schedule ξ ζ j i = dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j ⟨↑i, ⋯⟩

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

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard_eq_gaugeError {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)) ℂ)) : dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q n width schedule ξ ζ A C = dSVDensityRationalHeterogeneousStoppedCommonStopGaugeError Q n width schedule ξ ζ A C

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

noncomputable def QuantumParallelRepetition.unconditionalPublicBucketLoss (B Q : ℕ) (asynchronous precision : ℝ) : ℝ

Equations

• QuantumParallelRepetition.unconditionalPublicBucketLoss B Q asynchronous precision = (10 + 8 * (↑Q / ↑B)) * asynchronous + (4 * precision ^ 2 + 16 * (Real.exp ((↑B + 1) / ↑Q) - 1) + 8 / ↑B)

theorem QuantumParallelRepetition.exists_proofUnconditionalPublicBucketBalance (t : ℝ) (positive : 0 < t) (bounded : t ≤ 1) : ∃ (B : ℕ) (Q : ℕ), 0 < B ∧ 0 < Q ∧ 1 / ↑B ≤ t / 2 ∧ ↑Q / ↑B ≤ 3 / t ∧ (↑B + 1) / ↑Q ≤ t ∧ Real.exp ((↑B + 1) / ↑Q) - 1 ≤ (Real.exp 1 - 1) * t ∧ ∀ (asynchronous precision : ℝ), 0 ≤ asynchronous → unconditionalPublicBucketLoss B Q asynchronous precision ≤ 34 / t * asynchronous + 4 * precision ^ 2 + (16 * (Real.exp 1 - 1) + 4) * t

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

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)

def QuantumParallelRepetition.exactLocalQuestionHistoryEquiv {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)) : LocalQuestionContext X Y D × ExactHistoryFlag X Y A B D ≃ ExactLocallySampleableTuple X Y A B D

Equations

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

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

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

Equations

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

theorem QuantumParallelRepetition.exactLocallySampleableJA_weightedConditional {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) : exactLocallySampleableJA G n S D base ∘ ⇑(exactLocalQuestionHistoryEquiv D) = weightedConditionalJoint (localQuestionWeight G n D) fun (c : LocalQuestionContext X Y D) (r : ExactHistoryFlag X Y A B D) => exactAliceLocalConditional D base (exactLocallySampleableLaw G n S D) c.1 c.2.1 r

theorem QuantumParallelRepetition.exactLocallySampleableJB_weightedConditional {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) : exactLocallySampleableJB G n S D base ∘ ⇑(exactLocalQuestionHistoryEquiv D) = weightedConditionalJoint (localQuestionWeight G n D) fun (c : LocalQuestionContext X Y D) (r : ExactHistoryFlag X Y A B D) => exactBobLocalConditional D base (exactLocallySampleableLaw G n S D) c.1 c.2.2 r

theorem QuantumParallelRepetition.exactLocallySampleableJARounded_weightedConditional {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 → ℕ) : exactLocallySampleableJARounded G n D denominator numerator ∘ ⇑(exactLocalQuestionHistoryEquiv D) = weightedConditionalJoint (localQuestionWeight G n D) fun (c : LocalQuestionContext X Y D) (r : ExactHistoryFlag X Y A B D) => ↑(numerator (Sum.inl (c.1, c.2.1)) r) / ↑denominator

theorem QuantumParallelRepetition.exactLocallySampleableJBRounded_weightedConditional {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 → ℕ) : exactLocallySampleableJBRounded G n D denominator numerator ∘ ⇑(exactLocalQuestionHistoryEquiv D) = weightedConditionalJoint (localQuestionWeight G n D) fun (c : LocalQuestionContext X Y D) (r : ExactHistoryFlag X Y A B D) => ↑(numerator (Sum.inr (c.1, c.2.2)) r) / ↑denominator

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

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

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 → ℝ

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

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

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

Equations

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

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

def QuantumParallelRepetition.finiteIndependentProductWeight {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (q : ι → V → ℝ) (x : ι → V) : ℝ

Equations

• QuantumParallelRepetition.finiteIndependentProductWeight q x = ∏ i : ι, q i (x i)

noncomputable def QuantumParallelRepetition.finiteCoordinateMarginal {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (i : ι) : V → ℝ

Equations

• QuantumParallelRepetition.finiteCoordinateMarginal p i = QuantumParallelRepetition.ClassicalInformation.groupedMass (fun (x : ι → V) => x i) p

theorem QuantumParallelRepetition.finiteIndependentProductWeight_nonneg {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (q : ι → V → ℝ) (hq : ∀ (i : ι) (v : V), 0 ≤ q i v) (x : ι → V) : 0 ≤ finiteIndependentProductWeight q x

theorem QuantumParallelRepetition.finiteIndependentProductWeight_sum {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (q : ι → V → ℝ) (hq : ∀ (i : ι), ∑ v : V, q i v = 1) : ∑ x : ι → V, finiteIndependentProductWeight q x = 1

theorem QuantumParallelRepetition.finiteCoordinateMarginal_nonneg {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (hp : ∀ (x : ι → V), 0 ≤ p x) (i : ι) (v : V) : 0 ≤ finiteCoordinateMarginal p i v

theorem QuantumParallelRepetition.finiteCoordinateMarginal_sum {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (i : ι) : ∑ v : V, finiteCoordinateMarginal p i v = ∑ x : ι → V, p x

theorem QuantumParallelRepetition.finiteJoint_le_coordinateMarginal {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (hp : ∀ (x : ι → V), 0 ≤ p x) (x : ι → V) (i : ι) : p x ≤ finiteCoordinateMarginal p i (x i)

theorem QuantumParallelRepetition.finiteCoordinateMarginal_absolute_continuity {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (q : ι → V → ℝ) (hac : ∀ (x : ι → V), finiteIndependentProductWeight q x = 0 → p x = 0) (i : ι) (v : V) : q i v = 0 → finiteCoordinateMarginal p i v = 0

theorem QuantumParallelRepetition.finiteJoint_absolute_continuous_product_marginals {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (hp : ∀ (x : ι → V), 0 ≤ p x) (x : ι → V) : finiteIndependentProductWeight (finiteCoordinateMarginal p) x = 0 → p x = 0

theorem QuantumParallelRepetition.finiteCoordinateMarginal_sum_mul {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (i : ι) (f : V → ℝ) : ∑ x : ι → V, p x * f (x i) = ∑ v : V, finiteCoordinateMarginal p i v * f v

theorem QuantumParallelRepetition.finiteProductMarginal_relativeEntropy_le {ι : Type u_1} {V : Type u_2} [Fintype ι] [Fintype V] (p : (ι → V) → ℝ) (q : ι → V → ℝ) (hp : ∀ (x : ι → V), 0 ≤ p x) (hp_normalized : ∑ x : ι → V, p x = 1) (hq : ∀ (i : ι) (v : V), 0 ≤ q i v) (hq_normalized : ∀ (i : ι), ∑ v : V, q i v = 1) (absolute_continuity : ∀ (x : ι → V), finiteIndependentProductWeight q x = 0 → p x = 0) : ∑ i : ι, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal p i) (q i) ≤ Pinsker.finiteRelativeEntropy p (finiteIndependentProductWeight q)

theorem QuantumParallelRepetition.exactIndependentCoordinateQuestion_marginal {M : Type u_5} {Ω : Type u_6} {V : Type u_7} [Fintype M] [DecidableEq M] [Fintype Ω] [Fintype V] (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.repeatedAliceQuestionPrior_product {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)) (xs : Fin n → X) : ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.1) (strategyEventLaw (G.repeat n) S).weight xs = finiteIndependentProductWeight (fun (x : Fin n) => G.marginalX) xs

theorem QuantumParallelRepetition.repeatedBobQuestionPrior_product {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)) (ys : Fin n → Y) : ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.2.1) (strategyEventLaw (G.repeat n) S).weight ys = finiteIndependentProductWeight (fun (x : Fin n) => G.marginalY) ys

noncomputable def QuantumParallelRepetition.repeatedAlicePostselectedQuestionLaw {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)) : (Fin n → X) → ℝ

Equations

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

noncomputable def QuantumParallelRepetition.repeatedBobPostselectedQuestionLaw {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)) : (Fin n → Y) → ℝ

Equations

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

theorem QuantumParallelRepetition.exactGroupedMass_equiv {Ω : Type u_5} {K : Type u_6} {V : Type u_7} [Fintype Ω] [Fintype K] [Fintype V] (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.finiteProductMarginal_projection_relativeEntropy_le {Ω : Type u_5} {ι : Type u_6} {V : Type u_7} [Fintype Ω] [Fintype ι] [Fintype V] (posterior prior : Ω → ℝ) (projection : Ω → ι → V) (q : ι → V → ℝ) (budget : ℝ) (posterior_nonnegative : ∀ (ω : Ω), 0 ≤ posterior ω) (posterior_normalized : ∑ ω : Ω, posterior ω = 1) (prior_nonnegative : ∀ (ω : Ω), 0 ≤ prior ω) (absolute_continuity : ∀ (ω : Ω), prior ω = 0 → posterior ω = 0) (coordinate_nonnegative : ∀ (i : ι) (v : V), 0 ≤ q i v) (coordinate_normalized : ∀ (i : ι), ∑ v : V, q i v = 1) (actual_prior : ClassicalInformation.groupedMass projection prior = finiteIndependentProductWeight q) (actual_budget : Pinsker.finiteRelativeEntropy posterior prior ≤ budget) : ∑ i : ι, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal (ClassicalInformation.groupedMass projection posterior) i) (q i) ≤ budget

theorem QuantumParallelRepetition.repeatedAliceCoordinateInformation_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) : ∑ j : Fin n, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal (repeatedAlicePostselectedQuestionLaw G n S D) j) G.marginalX ≤ postselectionLogCost G n S D

theorem QuantumParallelRepetition.repeatedBobCoordinateInformation_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) : ∑ j : Fin n, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal (repeatedBobPostselectedQuestionLaw G n S D) j) G.marginalY ≤ postselectionLogCost G n S D

theorem QuantumParallelRepetition.finiteCoordinateMarginal_groupedMass {Ω : Type u_5} {ι : Type u_6} {V : Type u_7} [Fintype Ω] [Fintype ι] [Fintype V] (projection : Ω → ι → V) (mass : Ω → ℝ) (i : ι) (v : V) : finiteCoordinateMarginal (ClassicalInformation.groupedMass projection mass) i v = ClassicalInformation.groupedMass (fun (ω : Ω) => projection ω i) mass v

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.repeatedAlicePostselectedQuestionLaw_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (xs : Fin n → X) : 0 ≤ repeatedAlicePostselectedQuestionLaw G n S D xs

theorem QuantumParallelRepetition.repeatedBobPostselectedQuestionLaw_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (ys : Fin n → Y) : 0 ≤ repeatedBobPostselectedQuestionLaw G n S D ys

theorem QuantumParallelRepetition.repeatedAlicePostselectedCoordinateMarginal {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)) (j : Fin n) (x : X) : finiteCoordinateMarginal (repeatedAlicePostselectedQuestionLaw G n S D) j x = ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.1 j) (repeatedConditionedOutcomeLaw G n S D) x

theorem QuantumParallelRepetition.repeatedBobPostselectedCoordinateMarginal {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)) (j : Fin n) (y : Y) : finiteCoordinateMarginal (repeatedBobPostselectedQuestionLaw G n S D) j y = ClassicalInformation.groupedMass (fun (ω : ExactOutcome X Y A B n) => ω.2.1 j) (repeatedConditionedOutcomeLaw G n S D) y

theorem QuantumParallelRepetition.exactAliceSourceMarginalInformation_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (base : ExactHistoryFlag X Y A B D) : exactAliceSourceMarginalInformation G n S D base = 1 / ↑(Fintype.card (SourceRemainingCoordinate D)) * ∑ i : SourceRemainingCoordinate D, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal (repeatedAlicePostselectedQuestionLaw G n S D) ↑i) G.marginalX

theorem QuantumParallelRepetition.exactBobSourceMarginalInformation_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (base : ExactHistoryFlag X Y A B D) : exactBobSourceMarginalInformation G n S D base = 1 / ↑(Fintype.card (SourceRemainingCoordinate D)) * ∑ i : SourceRemainingCoordinate D, Pinsker.finiteRelativeEntropy (finiteCoordinateMarginal (repeatedBobPostselectedQuestionLaw G n S D) ↑i) G.marginalY

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

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

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

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

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

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

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 I] [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 I] [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) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max (max (max u_8 u_7) u_6 u_5) u_6)

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) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max (max (max u_8 u_7) u_6 u_5) u_5)

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 → ℝ

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 → ℝ

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 → ℝ

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 → ℝ

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 Ω] [Fintype C] [Fintype T] [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 C] [Fintype D] [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)

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)

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] [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)) (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 C] [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] [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 I] [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 I] [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 I] [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] [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)) (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)

theorem QuantumParallelRepetition.exactPermutationOutputUniformPushforward {R : Type u_1} [Fintype R] [DecidableEq R] (denominator : ℕ) (numerator : R → ℕ) (normalized : ∑ r : R, numerator r = denominator) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (letter : R) : ClassicalInformation.groupedMass (ClassicalInformation.rationalPermutationOutput denominator numerator nonempty) (fun (x : Equiv.Perm (R × Fin denominator)) => 1 / ↑(Fintype.card (Equiv.Perm (R × Fin denominator)))) letter = ↑(numerator letter) / ↑denominator

theorem QuantumParallelRepetition.exactPermutationOutputUniformExpectation {R : Type u_1} [Fintype R] [DecidableEq R] (denominator : ℕ) (numerator : R → ℕ) (normalized : ∑ r : R, numerator r = denominator) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (value : R → ℝ) : ∑ permutation : Equiv.Perm (R × Fin denominator), 1 / ↑(Fintype.card (Equiv.Perm (R × Fin denominator))) * value (ClassicalInformation.rationalPermutationOutput denominator numerator nonempty permutation) = ∑ letter : R, ↑(numerator letter) / ↑denominator * value letter

noncomputable def QuantumParallelRepetition.exactSourceAliceSampleTuple {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) (outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y) : ExactLocallySampleableTuple X Y A B D

Equations

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

theorem QuantumParallelRepetition.exactSourceAliceSampleTuple_expectation {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 → ℕ) (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) (value : ExactLocallySampleableTuple X Y A B D → ℝ) : ∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * value (exactSourceAliceSampleTuple D denominator numerator nonempty outcome) = ∑ history : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableJARounded G n D denominator numerator history * value history

theorem QuantumParallelRepetition.exactSourceAliceSampleTuple_groupedMass {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 → ℕ) (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) (history : ExactLocallySampleableTuple X Y A B D) : ClassicalInformation.groupedMass (exactSourceAliceSampleTuple D denominator numerator nonempty) (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) history = exactLocallySampleableJARounded G n D denominator numerator history

noncomputable def QuantumParallelRepetition.exactFiniteFiberLift {Ω : Type u_1} {T : Type u_2} [Fintype Ω] [DecidableEq T] (projection : Ω → T) (original : Ω → ℝ) (target : T → ℝ) (outcome : Ω) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactFiniteFiberLift_groupedMass {Ω : Type u_1} {T : Type u_2} [Fintype Ω] [DecidableEq T] (projection : Ω → T) (original : Ω → ℝ) (target : T → ℝ) (supported : ∀ (point : T), ClassicalInformation.groupedMass projection original point = 0 → target point = 0) (point : T) : ClassicalInformation.groupedMass projection (exactFiniteFiberLift projection original target) point = target point

theorem QuantumParallelRepetition.exactFiniteFiberLift_expectation {Ω : Type u_1} {T : Type u_2} [Fintype Ω] [Fintype T] [DecidableEq T] (projection : Ω → T) (original : Ω → ℝ) (target : T → ℝ) (supported : ∀ (point : T), ClassicalInformation.groupedMass projection original point = 0 → target point = 0) (value : T → ℝ) : ∑ outcome : Ω, exactFiniteFiberLift projection original target outcome * value (projection outcome) = ∑ point : T, target point * value point

theorem QuantumParallelRepetition.exactFiniteFiberLift_absolute_groupedMass {Ω : Type u_1} {T : Type u_2} [Fintype Ω] [DecidableEq T] (projection : Ω → T) (original : Ω → ℝ) (target : T → ℝ) (original_nonnegative : ∀ (outcome : Ω), 0 ≤ original outcome) (supported : ∀ (point : T), ClassicalInformation.groupedMass projection original point = 0 → target point = 0) (point : T) : ClassicalInformation.groupedMass projection (fun (outcome : Ω) => |original outcome - exactFiniteFiberLift projection original target outcome|) point = |ClassicalInformation.groupedMass projection original point - target point|

theorem QuantumParallelRepetition.exactFiniteFiberLift_totalVariation {Ω : Type u_1} {T : Type u_2} [Fintype Ω] [Fintype T] [DecidableEq T] (projection : Ω → T) (original : Ω → ℝ) (target : T → ℝ) (original_nonnegative : ∀ (outcome : Ω), 0 ≤ original outcome) (supported : ∀ (point : T), ClassicalInformation.groupedMass projection original point = 0 → target point = 0) : Pinsker.finiteTotalVariation original (exactFiniteFiberLift projection original target) = Pinsker.finiteTotalVariation (ClassicalInformation.groupedMass projection original) target

theorem QuantumParallelRepetition.existsCommonSupportPreservingRationalApproximations {I : Type u_1} {K : Type u_2} [Fintype I] [DecidableEq I] [Fintype K] (base : I) (probability : K → I → ℝ) (nonnegative : ∀ (index : K) (letter : I), 0 ≤ probability index letter) (normalized : ∀ (index : K), ∑ letter : I, probability index letter = 1) {gamma : ℝ} (gamma_positive : 0 < gamma) : ∃ (denominator : ℕ), 0 < denominator ∧ ∃ (numerator : K → I → ℕ), (∀ (index : K), ∑ letter : I, numerator index letter = denominator) ∧ (∀ (index : K), (Pinsker.finiteTotalVariation (probability index) fun (letter : I) => ↑(numerator index letter) / ↑denominator) < gamma) ∧ ∀ (index : K) (letter : I), 0 < probability index letter → 0 < numerator index letter

theorem QuantumParallelRepetition.exactLocallySampleableLaw_absolute_continuous_roundedJA {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 → ℕ) (preserves : ∀ (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) (history : ExactLocallySampleableTuple X Y A B D) : exactLocallySampleableJARounded G n D denominator numerator history = 0 → exactLocallySampleableLaw G n S D history = 0

theorem QuantumParallelRepetition.exact_exists_support_preserving_local_shared_permutation {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) (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), (Pinsker.finiteTotalVariation (exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index) fun (history : ExactHistoryFlag X Y A B D) => ↑(numerator index history) / ↑denominator) < gamma) ∧ (∀ (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), (∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D), (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ExactHistoryFlag X Y A B D × Fin denominator)) => ClassicalInformation.rationalPermutationOutput denominator (numerator index) ⋯ permutation = history) = ↑(numerator index history) / ↑denominator) ∧ ∀ (left right : ExactLocalSamplerIndex X Y D), (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ExactHistoryFlag X Y A B D × Fin denominator)) => ClassicalInformation.rationalPermutationOutput denominator (numerator left) ⋯ permutation ≠ ClassicalInformation.rationalPermutationOutput denominator (numerator right) ⋯ permutation) ≤ 2 * Pinsker.finiteTotalVariation (fun (history : ExactHistoryFlag X Y A B D) => ↑(numerator left history) / ↑denominator) fun (history : ExactHistoryFlag X Y A B D) => ↑(numerator right history) / ↑denominator

noncomputable def QuantumParallelRepetition.exactSourceAliceRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) : POVM A (ExactAliceLocalIndex G n S D r)

Equations

• QuantumParallelRepetition.exactSourceAliceRefinedPOVM G n S D r a₀ x = QuantumParallelRepetition.purificationAlicePOVM (QuantumParallelRepetition.exactAliceRefinedPOVM G n S D r a₀ x)

noncomputable def QuantumParallelRepetition.exactSourceBobRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) : POVM B (ExactBobLocalIndex G n S D r)

Equations

• QuantumParallelRepetition.exactSourceBobRefinedPOVM G n S D r b₀ y = QuantumParallelRepetition.exactBobRefinedPOVM G n S D r b₀ y

noncomputable def QuantumParallelRepetition.exactSourceJointEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (a : A) (b : B) : Matrix (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) ℂ

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceWinningEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) : Matrix (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) ℂ

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceWinningEffectCLM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) →L[ℂ] EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

Equations

• QuantumParallelRepetition.exactSourceWinningEffectCLM G n S D r a₀ b₀ x y = Matrix.toEuclideanCLM (QuantumParallelRepetition.exactSourceWinningEffect G n S D r a₀ b₀ x y)

theorem QuantumParallelRepetition.exactSourceJointEffect_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (a : A) (b : B) : quadraticExpectation (Matrix.toEuclideanCLM (exactSourceJointEffect G n S D r a₀ b₀ x y a b)) (exactUnnormalizedPsi G n S D r x y) = ((bornTracePairing S.state.matrix) (exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a)) (exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b)

theorem QuantumParallelRepetition.exactSourceWinningEffect_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) : quadraticExpectation (exactSourceWinningEffectCLM G n S D r a₀ b₀ x y) (exactUnnormalizedPsi G n S D r x y) = ∑ a : A, ∑ b : B, if G.predicate x y a b = true then ((bornTracePairing S.state.matrix) (exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a)) (exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b) else 0

theorem QuantumParallelRepetition.exactSourceWinningEffect_quadratic_eq_conditional {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (supported : exactFiberQuestionMass G n D r.seed r.history x y ≠ 0) : quadraticExpectation (exactSourceWinningEffectCLM G n S D r a₀ b₀ x y) (exactUnnormalizedPsi G n S D r x y) = exactJointConditionalWinningMass G n S D r.seed r.history r.aliceAnswer r.bobAnswer x y

theorem QuantumParallelRepetition.exactSourceNormalizedWinningEffect_eq_conditional {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (supported : exactFiberQuestionMass G n D r.seed r.history x y ≠ 0) : quadraticExpectation (exactSourceWinningEffectCLM G n S D r a₀ b₀ x y) (normalizedPureVector (exactUnnormalizedPsi G n S D r x y)) = exactJointConditionalWinningMass G n S D r.seed r.history r.aliceAnswer r.bobAnswer x y / ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x)) (exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)

noncomputable def QuantumParallelRepetition.exactSourceAcceptedCoordinateMass {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)) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactSourceAcceptedCoordinateMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (t : ExactLocallySampleableTuple X Y A B D) : 0 ≤ exactSourceAcceptedCoordinateMass G n S D t

theorem QuantumParallelRepetition.exactSourceAcceptedCoordinateMass_le_law {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)) (positive : 0 < repeatedPostselectionMass G n S D) (t : ExactLocallySampleableTuple X Y A B D) : exactSourceAcceptedCoordinateMass G n S D t ≤ exactLocallySampleableLaw G n S D t

noncomputable def QuantumParallelRepetition.exactSourceConditionalWinningProbability {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)) (t : ExactLocallySampleableTuple X Y A B D) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_bounds {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)) (positive : 0 < repeatedPostselectionMass G n S D) (t : ExactLocallySampleableTuple X Y A B D) : 0 ≤ exactSourceConditionalWinningProbability G n S D t ∧ exactSourceConditionalWinningProbability G n S D t ≤ 1

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_mul_law {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)) (positive : 0 < repeatedPostselectionMass G n S D) (t : ExactLocallySampleableTuple X Y A B D) : exactLocallySampleableLaw G n S D t * exactSourceConditionalWinningProbability G n S D t = exactSourceAcceptedCoordinateMass G n S D t

theorem QuantumParallelRepetition.exactSourceAcceptedCoordinateMass_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)) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactSourceAcceptedCoordinateMass G n S D t = ∑ q : ExactJointOutcome X Y A B D, if repeatedCoordinateWin G n (↑q.1.coordinate) q.2 = true then exactPostselectedJointLaw G n S D q else 0

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_expectation {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)) (positive : 0 < repeatedPostselectionMass G n S D) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t * exactSourceConditionalWinningProbability G n S D t = ∑ q : ExactJointOutcome X Y A B D, if repeatedCoordinateWin G n (↑q.1.coordinate) q.2 = true then exactPostselectedJointLaw G n S D q else 0

theorem QuantumParallelRepetition.exactRepeatedConditionedCoordinateWin {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 : Fin n) : (∑ outcome : ExactOutcome X Y A B n, if repeatedCoordinateWin G n i outcome = true then repeatedConditionedOutcomeLaw G n S D outcome else 0) = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert i D)) / repeatedPostselectionMass G n S D

theorem QuantumParallelRepetition.exactSourceAcceptedCoordinateMass_sum_eq_remaining_average {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)) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactSourceAcceptedCoordinateMass G n S D t = 1 / ↑(Fintype.card (SourceRemainingCoordinate D)) * ∑ i : SourceRemainingCoordinate D, (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert (↑i) D)) / repeatedPostselectionMass G n S D

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_eq_accepted_average {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)) (positive : 0 < repeatedPostselectionMass G n S D) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t * exactSourceConditionalWinningProbability G n S D t = sourceHistoryAcceptedMass G n S D / repeatedPostselectionMass G n S D

theorem QuantumParallelRepetition.exactSource_failure_sum_lt_of_uniform {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) {δ : ℝ} (failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < δ) : ∑ i ∈ Finset.univ \ D, (strategyEventLaw (G.repeat n) S).failureMass (repeatedCoordinateWin G n) D i < ↑(Finset.univ \ D).card * (δ * repeatedPostselectionMass G n S D)

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_gt_of_uniform_failure {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) {δ : ℝ} (failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < δ) : 1 - δ < ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t * exactSourceConditionalWinningProbability G n S D t

noncomputable def QuantumParallelRepetition.exactSourceAliceFlagCoupling {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 × Y → ℝ

Equations

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

theorem QuantumParallelRepetition.exactSourceAliceFlagCoupling_supported {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 → ℕ) (normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (preserves : ∀ (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) (history : ExactLocallySampleableTuple X Y A B D) : ClassicalInformation.groupedMass (exactSourceAliceSampleTuple D denominator numerator nonempty) (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator)) history = 0 → exactLocallySampleableLaw G n S D history = 0

theorem QuantumParallelRepetition.exactSourceAliceFlagCoupling_expectation {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 → ℕ) (normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (preserves : ∀ (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) (value : ExactLocallySampleableTuple X Y A B D → ℝ) : ∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, exactSourceAliceFlagCoupling G n S D denominator numerator nonempty outcome * value (exactSourceAliceSampleTuple D denominator numerator nonempty outcome) = ∑ history : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D history * value history

theorem QuantumParallelRepetition.exactSourceAliceFlagCoupling_sum {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 → ℕ) (normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (preserves : ∀ (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) : ∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y, exactSourceAliceFlagCoupling G n S D denominator numerator nonempty outcome = 1

theorem QuantumParallelRepetition.exactSourceAliceFlagCoupling_totalVariation {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 → ℕ) (normalized : ∀ (index : ExactLocalSamplerIndex X Y D), ∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) (preserves : ∀ (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) = Pinsker.finiteTotalVariation (exactLocallySampleableJARounded G n D denominator numerator) (exactLocallySampleableLaw G n S D)

noncomputable def QuantumParallelRepetition.exactFairWinningOutcomeBornMass {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)) (history : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactSourceAcceptedCoordinateMass_eq_seeded_fair_born {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)) (positive : 0 < repeatedPostselectionMass G n S D) (history : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : exactSourceAcceptedCoordinateMass G n S D (history.seed.coordinate, x, y, history) = if exactHistoryAccepted G n D history then exactSeedWeight history.seed * exactFairWinningOutcomeBornMass G n S D history x y / repeatedPostselectionMass G n S D else 0

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_eq_fine_born_ratio {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)) (positive : 0 < repeatedPostselectionMass G n S D) (history : ExactHistoryFlag X Y A B D) (accepted : exactHistoryAccepted G n D history) (x : X) (y : Y) : exactSourceConditionalWinningProbability G n S D (history.seed.coordinate, x, y, history) = exactFairWinningOutcomeBornMass G n S D history x y / exactFairFullOutcomeBornMass G n S D history x y

theorem QuantumParallelRepetition.exactFineCoordinateWinningBorn_collapse {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)) (aliceAnswer : ↥D → A) (bobAnswer : ↥D → B) (xs : Fin n → X) (ys : Fin n → Y) (coordinate : Fin n) (x : X) (y : Y) : (∑ a : A, ∑ b : B, if G.predicate x y a b = true then ((bornTracePairing S.state.matrix) (conditionedAliceCoordinateEffect G n S D aliceAnswer xs coordinate a)) (conditionedBobCoordinateEffect G n S D bobAnswer ys coordinate b) else 0) = ∑ aa : Fin n → A, ∑ bb : Fin n → B, if (∀ (j : Fin n) (member : j ∈ D), aa j = aliceAnswer ⟨j, member⟩) ∧ (∀ (j : Fin n) (member : j ∈ D), bb j = bobAnswer ⟨j, member⟩) ∧ G.predicate x y (aa coordinate) (bb coordinate) = true then S.outcomeProbability xs ys aa bb else 0

noncomputable def QuantumParallelRepetition.exactFairCoordinateRefinedWinningBornMass {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)) (history : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactFairWinningOutcomeBornMass_eq_refined {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)) (history : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : exactFairWinningOutcomeBornMass G n S D history x y = exactFairCoordinateRefinedWinningBornMass G n S D history x y

theorem QuantumParallelRepetition.exactFairWinningOutcomeBornMass_eq_fiber_conditional {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)) (history : ExactHistoryFlag X Y A B D) (x : X) (y : Y) (supported : exactFiberQuestionMass G n D history.seed history.history x y ≠ 0) : exactFairWinningOutcomeBornMass G n S D history x y = exactFiberQuestionMass G n D history.seed history.history x y * exactJointConditionalWinningMass G n S D history.seed history.history history.aliceAnswer history.bobAnswer x y

theorem QuantumParallelRepetition.exactSourceConditionalWinningProbability_eq_normalized_verifier {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [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)) (positive : 0 < repeatedPostselectionMass G n S D) (history : ExactHistoryFlag X Y A B D) (accepted : exactHistoryAccepted G n D history) (a₀ : A) (b₀ : B) (x : X) (y : Y) (supported : exactFiberQuestionMass G n D history.seed history.history x y ≠ 0) : exactSourceConditionalWinningProbability G n S D (history.seed.coordinate, x, y, history) = quadraticExpectation (exactSourceWinningEffectCLM G n S D history a₀ b₀ x y) (normalizedPureVector (exactUnnormalizedPsi G n S D history x y))

theorem QuantumParallelRepetition.exactLocallySampleableLaw_coordinate_eq_of_ne_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (t : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D t ≠ 0) : t.1 = t.2.2.2.seed.coordinate

theorem QuantumParallelRepetition.exactLocallySampleableLaw_accepted_of_ne_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (t : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D t ≠ 0) : exactHistoryAccepted G n D t.2.2.2

theorem QuantumParallelRepetition.exactLocallySampleableLaw_fiber_ne_zero_of_ne_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (t : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D t ≠ 0) : exactFiberQuestionMass G n D t.2.2.2.seed t.2.2.2.history t.2.1 t.2.2.1 ≠ 0

theorem QuantumParallelRepetition.exactLocallySampleableLaw_psi_ne_zero_of_ne_zero {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (t : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D t ≠ 0) : exactUnnormalizedPsi G n S D t.2.2.2 t.2.1 t.2.2.1 ≠ 0

def QuantumParallelRepetition.dependentBlockPOVM {R : Type u_1} {C : Type u_2} [Fintype R] [DecidableEq R] [Fintype C] {ι : R → Type u_3} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] (P : (r : R) → POVM C (ι r)) : POVM C ((r : R) × ι r)

Equations

• QuantumParallelRepetition.dependentBlockPOVM P = { effect := fun (c : C) => Matrix.blockDiagonal' fun (r : R) => (P r).effect c, positive := ⋯, complete := ⋯ }

def QuantumParallelRepetition.reindexedPOVM {C : Type u_1} {d : Type u_2} {e : Type u_3} [Fintype C] [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (basis : d ≃ e) (P : POVM C d) : POVM C e

Equations

• QuantumParallelRepetition.reindexedPOVM basis P = { effect := fun (c : C) => (P.effect c).submatrix ⇑basis.symm ⇑basis.symm, positive := ⋯, complete := ⋯ }

def QuantumParallelRepetition.twoBlockPOVM {C d e : Type} [Fintype C] [DecidableEq C] [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM C d) (Q : POVM C e) : POVM C (d ⊕ e)

Equations

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

def QuantumParallelRepetition.deterministicOutcomePOVM {C : Type u_1} {d : Type u_2} [Fintype C] [DecidableEq C] [Fintype d] [DecidableEq d] (default : C) : POVM C d

Equations

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

def QuantumParallelRepetition.pOVMChangeDecidableEq {C : Type u_1} {d : Type u_2} [Fintype C] [Fintype d] (source target : DecidableEq d) (P : POVM C d) : POVM C d

Equations

• QuantumParallelRepetition.pOVMChangeDecidableEq source target P = { effect := fun (c : C) => P.effect c, positive := ⋯, complete := ⋯ }

noncomputable def QuantumParallelRepetition.exactSourceAlicePaddedPOVM {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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) : POVM A (ExactPaddedLocalIndex G n S D r)

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceBobPaddedPOVM {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)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) : POVM B (ExactPaddedLocalIndex G n S D r)

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceGlobalAlicePOVM {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)) (a₀ : A) (x : X) : POVM A (ExactGlobalHistoryLocalIndex G n S D)

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceGlobalBobPOVM {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)) (b₀ : B) (y : Y) : POVM B (ExactGlobalHistoryLocalIndex G n S D)

Equations

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

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

Equations

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

noncomputable def QuantumParallelRepetition.exactSourceGlobalCatalystBobPOVM {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)) (e : ℕ) (b₀ : B) (y : Y) : POVM B (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e))

Equations

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

@[simp]

theorem QuantumParallelRepetition.twoBlockPOVM_effect_inl {C d e : Type} [Fintype C] [DecidableEq C] [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM C d) (Q : POVM C e) (c : C) (i j : d) : (twoBlockPOVM P Q).effect c (Sum.inl i) (Sum.inl j) = P.effect c i j

@[simp]

theorem QuantumParallelRepetition.twoBlockPOVM_effect_inr {C d e : Type} [Fintype C] [DecidableEq C] [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM C d) (Q : POVM C e) (c : C) (i j : e) : (twoBlockPOVM P Q).effect c (Sum.inr i) (Sum.inr j) = Q.effect c i j

@[simp]

theorem QuantumParallelRepetition.dependentBlockPOVM_effect_same {R : Type u_1} {C : Type u_2} [Fintype R] [DecidableEq R] [Fintype C] {ι : R → Type u_3} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] (P : (r : R) → POVM C (ι r)) (r : R) (c : C) (i j : ι r) : (dependentBlockPOVM P).effect c ⟨r, i⟩ ⟨r, j⟩ = (P r).effect c i j

@[simp]

theorem QuantumParallelRepetition.exactSourceGlobalAlicePOVM_effect {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)) (r : ExactHistoryFlag X Y A B D) (a₀ a : A) (x : X) (i j : ExactAliceLocalIndex G n S D r) : (exactSourceGlobalAlicePOVM G n S D a₀ x).effect a (Sum.inr ⟨r, Sum.inr (Sum.inl i)⟩) (Sum.inr ⟨r, Sum.inr (Sum.inl j)⟩) = (exactSourceAliceRefinedPOVM G n S D r a₀ x).effect a i j

@[simp]

theorem QuantumParallelRepetition.exactSourceGlobalBobPOVM_effect {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)) (r : ExactHistoryFlag X Y A B D) (b₀ b : B) (y : Y) (i j : ExactBobLocalIndex G n S D r) : (exactSourceGlobalBobPOVM G n S D b₀ y).effect b (Sum.inr ⟨r, Sum.inr (Sum.inr i)⟩) (Sum.inr ⟨r, Sum.inr (Sum.inr j)⟩) = (exactSourceBobRefinedPOVM G n S D r b₀ y).effect b i j

theorem QuantumParallelRepetition.matrixQuadraticExpectation_expand {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) (z : EuclideanSpace ℂ d) : quadraticExpectation (Matrix.toEuclideanCLM M) z = (∑ i : d, (∑ j : d, M i j * z.ofLp j) * star (z.ofLp i)).re

theorem QuantumParallelRepetition.finiteSum_injective_support {d : Type u_1} {e : Type u_2} {K : Type u_3} [Fintype d] [Fintype e] [AddCommMonoid K] (f : d → e) (injective : Function.Injective f) (g : e → K) (supported : ∀ (j : e), (∀ (i : d), f i ≠ j) → g j = 0) : ∑ j : e, g j = ∑ i : d, g (f i)

theorem QuantumParallelRepetition.matrixQuadraticExpectation_injective {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (f : d → e) (injective : Function.Injective f) (M : Matrix e e ℂ) (N : Matrix d d ℂ) (v : EuclideanSpace ℂ e) (z : EuclideanSpace ℂ d) (included : ∀ (i : d), v.ofLp (f i) = z.ofLp i) (supported : ∀ (j : e), (∀ (i : d), f i ≠ j) → v.ofLp j = 0) (compressed : ∀ (i j : d), M (f i) (f j) = N i j) : quadraticExpectation (Matrix.toEuclideanCLM M) v = quadraticExpectation (Matrix.toEuclideanCLM N) z

def QuantumParallelRepetition.exactSourceGlobalJointBasis {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r → ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D

Equations

• QuantumParallelRepetition.exactSourceGlobalJointBasis G n S D r (i, j) = (Sum.inr ⟨r, Sum.inr (Sum.inl i)⟩, Sum.inr ⟨r, Sum.inr (Sum.inr j)⟩)

theorem QuantumParallelRepetition.exactSourceGlobalJointBasis_injective {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Function.Injective (exactSourceGlobalJointBasis G n S D r)

theorem QuantumParallelRepetition.exactSourceGlobalJointBasis_vector {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) (i : ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) : (exactGlobalHistoryVector G n S D r (exactPaddedVector G n S D r z)).ofLp (exactSourceGlobalJointBasis G n S D r i) = z.ofLp i

theorem QuantumParallelRepetition.exactSourceGlobalJointBasis_support {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) (j : ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) (outside : ∀ (i : ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r), exactSourceGlobalJointBasis G n S D r i ≠ j) : (exactGlobalHistoryVector G n S D r (exactPaddedVector G n S D r z)).ofLp j = 0

noncomputable def QuantumParallelRepetition.exactSourceGlobalWinningEffect {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)) (a₀ : A) (b₀ : B) (x : X) (y : Y) : Matrix (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) ℂ

Equations

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

theorem QuantumParallelRepetition.exactSourceGlobalWinningEffect_compression {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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (i j : ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r) : exactSourceGlobalWinningEffect G n S D a₀ b₀ x y (exactSourceGlobalJointBasis G n S D r i) (exactSourceGlobalJointBasis G n S D r j) = exactSourceWinningEffect G n S D r a₀ b₀ x y i j

theorem QuantumParallelRepetition.exactSourceGlobalWinningEffect_quadratic {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)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : quadraticExpectation (Matrix.toEuclideanCLM (exactSourceGlobalWinningEffect G n S D a₀ b₀ x y)) (exactGlobalHistoryVector G n S D r (exactPaddedVector G n S D r z)) = quadraticExpectation (exactSourceWinningEffectCLM G n S D r a₀ b₀ x y) z

@[simp]

theorem QuantumParallelRepetition.reindexedCatalystPOVM_effect {C : Type u_1} {d : Type u_2} [Fintype C] [Fintype d] [DecidableEq d] (P : POVM C d) (e : ℕ) (c : C) (i j : d) (k l : Fin e) : (reindexedPOVM finProdFinEquiv (purificationAlicePOVM (reindexedPOVM (Fintype.equivFin d) P))).effect c (finProdFinEquiv ((Fintype.equivFin d) i, k)) (finProdFinEquiv ((Fintype.equivFin d) j, l)) = P.effect c i j * if k = l then 1 else 0

@[simp]

theorem QuantumParallelRepetition.exactSourceGlobalCatalystBobPOVM_effect {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)) (e : ℕ) (b₀ b : B) (y : Y) (i j : ExactGlobalHistoryLocalIndex G n S D) (k l : Fin e) : (exactSourceGlobalCatalystBobPOVM G n S D e b₀ y).effect b (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) i, k)) (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) j, l)) = (exactSourceGlobalBobPOVM G n S D b₀ y).effect b i j * if k = l then 1 else 0

theorem QuantumParallelRepetition.reweightedSeedPrefixEntropyIncrement_eq_actual_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] {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)) (positive : 0 < repeatedPostselectionMass G n S D) (projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V)) (default : V) (k : Fin h) : reweightedSeedPrefixEntropyIncrement seedLaw G n S D projection default k = ∑ point : K × ExactOutcome X Y A B n, reweightedSeedPosterior seedLaw G n S D point * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default k) (reweightedSeedPrefixJoint seedLaw G n S D projection)) (finitePrefixMask default k.castSucc (((projection point).1, repeatedConditionedAnswerFlag G n S D point.2), (projection point).2))) (ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default k) (reweightedSeedPrefixPrior seedLaw G n S D projection)) (finitePrefixMask default k.castSucc (((projection point).1, repeatedConditionedAnswerFlag G n S D point.2), (projection point).2)))

theorem QuantumParallelRepetition.exactStrategyQuestionCodeGroupedMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {C : Type u_5} [Fintype C] [DecidableEq C] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (code : (Fin n → X) → (Fin n → Y) → C) (target : C) : ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => code outcome.1 outcome.2.1) (strategyEventLaw (G.repeat n) S).weight target = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, if code xs ys = target then (G.repeat n).questionWeight xs ys else 0

theorem QuantumParallelRepetition.exactRepeatedQuestionWeight_splitAt_bob {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 : ℕ) (i : Fin n) (xs : Fin n → X) (y : Y) (tail : { j : Fin n // j ≠ i } → Y) : (G.repeat n).questionWeight xs ((Equiv.funSplitAt i Y).symm (y, tail)) = G.questionWeight (xs i) y * ∏ j ∈ Finset.univ.erase i, G.questionWeight (xs j) ((Equiv.funSplitAt i Y).symm (y, tail) j)

theorem QuantumParallelRepetition.exactRepeatedQuestionTail_splitAt_bob {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 : ℕ) (i : Fin n) (xs : Fin n → X) (y y' : Y) (tail : { j : Fin n // j ≠ i } → Y) : ∏ j ∈ Finset.univ.erase i, G.questionWeight (xs j) ((Equiv.funSplitAt i Y).symm (y, tail) j) = ∏ j ∈ Finset.univ.erase i, G.questionWeight (xs j) ((Equiv.funSplitAt i Y).symm (y', tail) j)