Quantum parallel repetition, part 08

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

The product encoding of exact source alice sample.

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

Reweight each projection fiber to its target mass while retaining its relative weights.

Equations

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

theorem QuantumParallelRepetition.existsCommonSupportPreservingRationalApproximations {I : Type u_1} {K : Type u_2} [Fintype I] [Finite 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)

Alice's local source measurement obtained by purifying the coordinate refinement.

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)

Bob's local source measurement obtained by purifying the coordinate refinement.

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

The tensor product of the two refined local source effects.

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

The sum of refined joint effects over answers accepted by the game predicate.

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)

The continuous linear map implementing exact source winning effect.

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

The postselected mass of outcomes with the specified code that win the selected coordinate.

Equations

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

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

The probability of exact source conditional winning.

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

The exact source alice flag coupling construction used in the quantum parallel-repetition argument.

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)

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

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)

The positive operator-valued measurement implementing dependent block.

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

The positive operator-valued measurement implementing reindexed.

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] [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (P : POVM C d) (Q : POVM C e) : POVM C (d ⊕ e)

Combine two measurements as a direct-sum measurement on their local spaces.

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

The positive operator-valued measurement implementing deterministic outcome.

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

Transport a POVM between equality decisions while retaining every effect matrix.

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)

Pad Alice's refined measurement with deterministic outcomes on the unused blocks.

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)

Pad Bob's refined measurement with deterministic outcomes on the unused blocks.

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)

The positive operator-valued measurement implementing exact source global alice.

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)

The positive operator-valued measurement implementing exact source global bob.

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

The positive operator-valued measurement implementing exact source global catalyst alice.

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

The positive operator-valued measurement implementing exact source global catalyst bob.

Equations

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

@[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

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

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

The measurement effect for exact source global winning.

Equations

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

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

theorem QuantumParallelRepetition.exactStrategyStableBobQuestionCode_joint_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] {C : Type u_5} [DecidableEq C] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (coordinate : Fin n) (code : (Fin n → X) → (Fin n → Y) → C) (target : C) (question : X) (next : Y) (stable : ∀ (xs : Fin n → X) (tail : { j : Fin n // j ≠ coordinate } → Y) (y y' : Y), code xs ((Equiv.funSplitAt coordinate Y).symm (y, tail)) = code xs ((Equiv.funSplitAt coordinate Y).symm (y', tail))) (determines : ∀ (xs : Fin n → X) (ys : Fin n → Y), code xs ys = target → xs coordinate = question) : ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => (code outcome.1 outcome.2.1, outcome.2.1 coordinate)) (strategyEventLaw (G.repeat n) S).weight (target, next) = G.conditionalYGivenX question next * ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => code outcome.1 outcome.2.1) (strategyEventLaw (G.repeat n) S).weight target

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

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

theorem QuantumParallelRepetition.exactStrategyStableAliceQuestionCode_joint_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] {C : Type u_5} [DecidableEq C] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (coordinate : Fin n) (code : (Fin n → X) → (Fin n → Y) → C) (target : C) (question : Y) (next : X) (stable : ∀ (ys : Fin n → Y) (tail : { j : Fin n // j ≠ coordinate } → X) (x x' : X), code ((Equiv.funSplitAt coordinate X).symm (x, tail)) ys = code ((Equiv.funSplitAt coordinate X).symm (x', tail)) ys) (determines : ∀ (xs : Fin n → X) (ys : Fin n → Y), code xs ys = target → ys coordinate = question) : ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => (code outcome.1 outcome.2.1, outcome.1 coordinate)) (strategyEventLaw (G.repeat n) S).weight (target, next) = G.conditionalXGivenY question next * ClassicalInformation.groupedMass (fun (outcome : ExactOutcome X Y A B n) => code outcome.1 outcome.2.1) (strategyEventLaw (G.repeat n) S).weight target

theorem QuantumParallelRepetition.exactAliceSourceConditionalInformation_eq_joint_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 : ExactJointOutcome X Y A B D, exactPostselectedJointLaw 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.coordinate, point.2.1 ↑point.1.coordinate), exactHistoryCode D point)) (G.conditionalYGivenX (point.2.1 ↑point.1.coordinate))

theorem QuantumParallelRepetition.exactBobSourceConditionalInformation_eq_joint_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 : ExactJointOutcome X Y A B D, exactPostselectedJointLaw 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.coordinate, point.2.2.1 ↑point.1.coordinate), exactHistoryCode D point)) (G.conditionalXGivenY (point.2.2.1 ↑point.1.coordinate))

theorem QuantumParallelRepetition.exactSeedWeight_pos_of_seed {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : 0 < exactSeedWeight seed

theorem QuantumParallelRepetition.jointConditional_product_context_seed {K : Type u_1} {Ω : Type u_2} {C : Type u_3} {V : Type u_4} [Fintype K] [Fintype Ω] [Fintype V] (context : K → Ω → C) (next : K → Ω → V) (seedWeight : K → ℝ) (outcomeWeight : Ω → ℝ) (seed : K) (target : C) (nonzero : seedWeight seed ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (q : K × Ω) => ((q.1, context q.1 q.2), next q.1 q.2)) fun (q : K × Ω) => seedWeight q.1 * outcomeWeight q.2) (seed, target) = ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : Ω) => (context seed outcome, next seed outcome)) outcomeWeight) target

theorem QuantumParallelRepetition.exactAliceSourceContextNextPosterior_eq_groupedMass {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)) : (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)) = ClassicalInformation.groupedMass (fun (point : ExactJointOutcome X Y A B D) => (((point.1.coordinate, point.2.1 ↑point.1.coordinate), exactHistoryCode D point), point.2.2.1 ↑point.1.coordinate)) (exactPostselectedJointLaw G n S D)

theorem QuantumParallelRepetition.exactBobSourceContextNextPosterior_eq_groupedMass {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)) : (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)) = ClassicalInformation.groupedMass (fun (point : ExactJointOutcome X Y A B D) => (((point.1.coordinate, point.2.2.1 ↑point.1.coordinate), exactHistoryCode D point), point.2.1 ↑point.1.coordinate)) (exactPostselectedJointLaw G n S D)

theorem QuantumParallelRepetition.exactAliceSourcePosteriorConditional_eq_fixedSeedFiber {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)) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : 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)) ((seed.coordinate, reference.1 ↑seed.coordinate), exactHistoryCode D (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.exactBobSourcePosteriorConditional_eq_fixedSeedFiber {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)) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : 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)) ((seed.coordinate, reference.2.1 ↑seed.coordinate), exactHistoryCode D (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.exactReverseAliceMarkedPosteriorConditional_eq_sourcePosterior {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 (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)) ((seed.coordinate, reference.1 ↑seed.coordinate), exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseBobMarkedPosteriorConditional_eq_sourcePosterior {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 (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)) ((seed.coordinate, reference.2.1 ↑seed.coordinate), exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseAliceSideWeightedPrefix_sum {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (score : (side : Finset M) → ExactForwardSeed M → Fin side.card → ℝ) : ∑ side : Finset M, reversePartitionWeight side * ((∑ marker : Fin side.card, ∑ seed : ExactForwardSeed M, (exactReverseAliceConditionalSeedLaw nonempty side).weight seed * score side seed marker) / ↑side.card) = ∑ seed : ExactForwardSeed M, exactSeedWeight seed * ((∑ marker : Fin (exactReverseLeftSide seed).card, score (exactReverseLeftSide seed) seed marker) / ↑(exactReverseLeftSide seed).card)

theorem QuantumParallelRepetition.exactReverseBobSideWeightedPrefix_sum {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (score : (side : Finset M) → ExactForwardSeed M → Fin side.card → ℝ) : ∑ side : Finset M, reversePartitionWeight side * ((∑ marker : Fin side.card, ∑ seed : ExactForwardSeed M, (exactReverseBobConditionalSeedLaw nonempty side).weight seed * score side seed marker) / ↑side.card) = ∑ seed : ExactForwardSeed M, exactSeedWeight seed * ((∑ marker : Fin (exactReverseRightSide seed).card, score (exactReverseRightSide seed) seed marker) / ↑(exactReverseRightSide seed).card)

theorem QuantumParallelRepetition.groupedMass_product_stable_context_fiber {K : Type u_1} {Ω : Type u_2} {I : Type u_3} {C : Type u_4} {V : Type u_5} [Fintype K] [Fintype Ω] (index : K → I) (context : I → Ω → C) (next : I → Ω → V) (extract : C → I) (extract_context : ∀ (i : I) (outcome : Ω), extract (context i outcome) = i) (seedWeight : K → ℝ) (outcomeWeight : Ω → ℝ) (target : C) (value : V) : ClassicalInformation.groupedMass (fun (point : K × Ω) => (context (index point.1) point.2, next (index point.1) point.2)) (fun (point : K × Ω) => seedWeight point.1 * outcomeWeight point.2) (target, value) = ClassicalInformation.groupedMass index seedWeight (extract target) * ClassicalInformation.groupedMass (fun (outcome : Ω) => (context (extract target) outcome, next (extract target) outcome)) outcomeWeight (target, value)

theorem QuantumParallelRepetition.jointConditional_product_stable_context_seed {K : Type u_1} {Ω : Type u_2} {I : Type u_3} {C : Type u_4} {V : Type u_5} [Fintype K] [Fintype Ω] [Fintype V] (index : K → I) (context : I → Ω → C) (next : I → Ω → V) (extract : C → I) (extract_context : ∀ (i : I) (outcome : Ω), extract (context i outcome) = i) (seedWeight : K → ℝ) (outcomeWeight : Ω → ℝ) (seed : K) (target : C) (target_index : extract target = index seed) (nonzero : ClassicalInformation.groupedMass index seedWeight (index seed) ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (point : K × Ω) => (context (index point.1) point.2, next (index point.1) point.2)) fun (point : K × Ω) => seedWeight point.1 * outcomeWeight point.2) target = ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (fun (outcome : Ω) => (context (index seed) outcome, next (index seed) outcome)) outcomeWeight) target

theorem QuantumParallelRepetition.groupedMass_pos_of_supported_atom {K : Type u_1} {I : Type u_2} [Fintype K] [DecidableEq I] (code : K → I) (weight : K → ℝ) (nonnegative : ∀ (seed : K), 0 ≤ weight seed) (seed : K) (positive : 0 < weight seed) : 0 < ClassicalInformation.groupedMass code weight (code seed)

theorem QuantumParallelRepetition.reweightedSeedPrefixNextJoint_as_actual_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) (marker : Fin h) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (reweightedSeedPrefixJoint seedLaw G n S D projection) = ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => exactPrefixNextCode default marker (((projection point).1, repeatedConditionedAnswerFlag G n S D point.2), (projection point).2)) (reweightedSeedPosterior seedLaw G n S D)

theorem QuantumParallelRepetition.groupedMass_productCode_weighted_sum {K : Type u_1} {Ω : Type u_2} {C : Type u_3} [Fintype K] [Fintype Ω] [DecidableEq C] (code : K → Ω → C) (weight : K → ℝ) (mass : Ω → ℝ) (target : C) : ClassicalInformation.groupedMass (fun (point : K × Ω) => code point.1 point.2) (fun (point : K × Ω) => weight point.1 * mass point.2) target = ∑ index : K, weight index * ClassicalInformation.groupedMass (code index) mass target

theorem QuantumParallelRepetition.groupedMass_flagSeedOutcome_reassoc {F : Type u_1} {K : Type u_2} {Ω : Type u_3} {C : Type u_4} [Fintype F] [Fintype K] [Fintype Ω] [DecidableEq C] (code : F → K → Ω → C) (flagWeight : F → ℝ) (seedWeight : K → ℝ) (outcomeWeight : Ω → ℝ) (target : C) : ClassicalInformation.groupedMass (fun (point : F × K × Ω) => code point.1 point.2.1 point.2.2) (fun (point : F × K × Ω) => flagWeight point.1 * (seedWeight point.2.1 * outcomeWeight point.2.2)) target = ClassicalInformation.groupedMass (fun (point : (F × K) × Ω) => code point.1.1 point.1.2 point.2) (fun (point : (F × K) × Ω) => flagWeight point.1.1 * seedWeight point.1.2 * outcomeWeight point.2) target

theorem QuantumParallelRepetition.mixedStableBobQuestionCode_joint_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] {K : Type u_5} {C : Type u_6} [Fintype K] [DecidableEq C] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (weight : K → ℝ) (coordinate : K → Fin n) (code : K → (Fin n → X) → (Fin n → Y) → C) (target : C) (question : X) (next : Y) (stable : ∀ (index : K) (xs : Fin n → X) (tail : { j : Fin n // j ≠ coordinate index } → Y) (y y' : Y), code index xs ((Equiv.funSplitAt (coordinate index) Y).symm (y, tail)) = code index xs ((Equiv.funSplitAt (coordinate index) Y).symm (y', tail))) (determines : ∀ (index : K) (xs : Fin n → X) (ys : Fin n → Y), code index xs ys = target → xs (coordinate index) = question) : ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => (code point.1 point.2.1 point.2.2.1, point.2.2.1 (coordinate point.1))) (fun (point : K × ExactOutcome X Y A B n) => weight point.1 * (strategyEventLaw (G.repeat n) S).weight point.2) (target, next) = G.conditionalYGivenX question next * ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => code point.1 point.2.1 point.2.2.1) (fun (point : K × ExactOutcome X Y A B n) => weight point.1 * (strategyEventLaw (G.repeat n) S).weight point.2) target

theorem QuantumParallelRepetition.mixedStableAliceQuestionCode_joint_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] {K : Type u_5} {C : Type u_6} [Fintype K] [DecidableEq C] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (weight : K → ℝ) (coordinate : K → Fin n) (code : K → (Fin n → X) → (Fin n → Y) → C) (target : C) (question : Y) (next : X) (stable : ∀ (index : K) (ys : Fin n → Y) (tail : { j : Fin n // j ≠ coordinate index } → X) (x x' : X), code index ((Equiv.funSplitAt (coordinate index) X).symm (x, tail)) ys = code index ((Equiv.funSplitAt (coordinate index) X).symm (x', tail)) ys) (determines : ∀ (index : K) (xs : Fin n → X) (ys : Fin n → Y), code index xs ys = target → ys (coordinate index) = question) : ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => (code point.1 point.2.1 point.2.2.1, point.2.1 (coordinate point.1))) (fun (point : K × ExactOutcome X Y A B n) => weight point.1 * (strategyEventLaw (G.repeat n) S).weight point.2) (target, next) = G.conditionalXGivenY question next * ClassicalInformation.groupedMass (fun (point : K × ExactOutcome X Y A B n) => code point.1 point.2.1 point.2.2.1) (fun (point : K × ExactOutcome X Y A B n) => weight point.1 * (strategyEventLaw (G.repeat n) S).weight point.2) target

theorem QuantumParallelRepetition.exactConditionedReverseAliceNextPrior_marked_joint_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)) (remaining : 0 < (Finset.univ \ D).card) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (target : ExactReverseAliceNextContext X Y A B D side) (next : Y) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextPrior G n S D remaining side) (target, next) = G.conditionalYGivenX (target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker)) next * ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextPrior G n S D remaining side)) target

theorem QuantumParallelRepetition.exactConditionedReverseAliceNextPrior_marked_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)) (remaining : 0 < (Finset.univ \ D).card) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (target : ExactReverseAliceNextContext X Y A B D side) (supported : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextPrior G n S D remaining side)) target ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextPrior G n S D remaining side)) target = G.conditionalYGivenX (target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker))

theorem QuantumParallelRepetition.exactReverseAliceMarkedPriorConditional_eq_game {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) (supported : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseAliceNextPrior G n S D remaining (exactReverseLeftSide seed))) (exactReverseAliceMarkedHistoryContext G n S D default seed reference) ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseAliceNextPrior G n S D remaining (exactReverseLeftSide seed))) (exactReverseAliceMarkedHistoryContext G n S D default seed reference) = G.conditionalYGivenX (reference.1 ↑seed.coordinate)

theorem QuantumParallelRepetition.exactReverseAliceActualConditionalSeedWeight_pos {n : ℕ} (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (seed : ExactRemainingSeed D) : 0 < (exactReverseAliceConditionalSeedLaw ⋯ (exactReverseLeftSide seed)).weight seed

theorem QuantumParallelRepetition.exactReverseAliceSideMarkedPosteriorConditional_eq_fixedSeedFiber {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseAliceNextJoint G n S D remaining (exactReverseLeftSide seed))) (exactReverseAliceMarkedHistoryContext G n S D default seed reference) = 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)

theorem QuantumParallelRepetition.exactReverseAliceSideMarkedPosteriorConditional_eq_sourcePosterior {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseAliceNextJoint G n S D remaining (exactReverseLeftSide seed))) (exactReverseAliceMarkedHistoryContext G n S D default seed reference) = 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)) ((seed.coordinate, reference.1 ↑seed.coordinate), exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.reweightedSeedPrefixPriorMarginal_ne_zero_of_positive_atom {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 : ℕ} (law : 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) (marker : Fin h) (point : K × ExactOutcome X Y A B n) (atom_positive : 0 < reweightedSeedPosterior law G n S D point) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (reweightedSeedPrefixPrior law G n S D projection)) (finitePrefixMask default marker.castSucc (((projection point).1, repeatedConditionedAnswerFlag G n S D point.2), (projection point).2)) ≠ 0

theorem QuantumParallelRepetition.repeatedConditionedOutcomeLaw_pos_of_ne_zero {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (outcome : ExactOutcome X Y A B n) (nonzero : repeatedConditionedOutcomeLaw G n S D outcome ≠ 0) : 0 < repeatedConditionedOutcomeLaw G n S D outcome

theorem QuantumParallelRepetition.exactReverseAliceMarkedPriorMarginal_ne_zero_of_outcome {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) (default : Y) (seed : ExactRemainingSeed D) (outcome : ExactOutcome X Y A B n) (outcome_nonzero : repeatedConditionedOutcomeLaw G n S D outcome ≠ 0) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseAliceNextPrior G n S D remaining (exactReverseLeftSide seed))) (exactReverseAliceMarkedHistoryContext G n S D default seed outcome) ≠ 0

theorem QuantumParallelRepetition.exactReverseAliceConditionalHistoryIdentification_proved {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) (default : Y) : ExactReverseAliceConditionalHistoryIdentification G n S D remaining base default

theorem QuantumParallelRepetition.exactConditionedReverseBobNextPrior_marked_joint_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)) (remaining : 0 < (Finset.univ \ D).card) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (target : ExactReverseBobNextContext X Y A B D side) (next : X) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextPrior G n S D remaining side) (target, next) = G.conditionalXGivenY (target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker)) next * ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextPrior G n S D remaining side)) target

theorem QuantumParallelRepetition.exactConditionedReverseBobNextPrior_marked_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)) (remaining : 0 < (Finset.univ \ D).card) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (target : ExactReverseBobNextContext X Y A B D side) (supported : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextPrior G n S D remaining side)) target ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextPrior G n S D remaining side)) target = G.conditionalXGivenY (target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker))

theorem QuantumParallelRepetition.exactReverseBobMarkedPriorConditional_eq_game {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) (supported : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseBobNextPrior G n S D remaining (exactReverseRightSide seed))) (exactReverseBobMarkedHistoryContext G n S D default seed reference) ≠ 0) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseBobNextPrior G n S D remaining (exactReverseRightSide seed))) (exactReverseBobMarkedHistoryContext G n S D default seed reference) = G.conditionalXGivenY (reference.2.1 ↑seed.coordinate)

theorem QuantumParallelRepetition.exactReverseBobConditionalSeedLaw_actual_pos {M : Type u_5} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (seed : ExactForwardSeed M) : 0 < (exactReverseBobConditionalSeedLaw nonempty (exactReverseRightSide seed)).weight seed

theorem QuantumParallelRepetition.exactConditionedReverseBobNextJoint_marked_conditional_eq_fixedOutcome {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseBobNextJoint G n S D remaining (exactReverseRightSide seed))) (exactReverseBobMarkedHistoryContext G n S D default seed reference) = 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)

theorem QuantumParallelRepetition.exactConditionedReverseBobNextJoint_marked_conditional_eq_sourcePosterior {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) (seed : ExactRemainingSeed D) (reference : ExactOutcome X Y A B n) : ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseBobNextJoint G n S D remaining (exactReverseRightSide seed))) (exactReverseBobMarkedHistoryContext G n S D default seed reference) = 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)) ((seed.coordinate, reference.2.1 ↑seed.coordinate), exactHistoryCode D (seed, reference))

theorem QuantumParallelRepetition.exactReverseBobMarkedPriorMarginal_ne_zero_of_outcome {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) (default : X) (seed : ExactRemainingSeed D) (outcome : ExactOutcome X Y A B n) (supported : repeatedConditionedOutcomeLaw G n S D outcome ≠ 0) : ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)) (exactConditionedReverseBobNextPrior G n S D remaining (exactReverseRightSide seed))) (exactReverseBobMarkedHistoryContext G n S D default seed outcome) ≠ 0

theorem QuantumParallelRepetition.exactReverseBobConditionalHistoryIdentification_proved {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) (default : X) : ExactReverseBobConditionalHistoryIdentification G n S D remaining base default

theorem QuantumParallelRepetition.exact_source_equation_twenty_three_unconditional {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) : ExactSourceClassicalInformationBound G n S D base

def QuantumParallelRepetition.ExactSourceSupportPreservingClassicalSampler {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)) (base : ExactHistoryFlag X Y A B D) (kappa gamma : ℝ) : Prop

The exact source support preserving classical sampler construction used in the quantum parallel- repetition argument.

Equations

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

theorem QuantumParallelRepetition.exact_source_equation_twenty_seven_support_preserving {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) {kappa gamma : ℝ} (gamma_positive : 0 < gamma) (alice : Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) ≤ kappa) (bob : Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) ≤ kappa) : ExactSourceSupportPreservingClassicalSampler G n S D base kappa gamma

theorem QuantumParallelRepetition.exact_source_equation_twenty_seven_support_preserving_of_information {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) (information : ExactSourceClassicalInformationBound G n S D base) {gamma : ℝ} (gamma_positive : 0 < gamma) : ExactSourceSupportPreservingClassicalSampler G n S D base (exactSourcePinskerRate G n S D) gamma