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} [Fintype C] [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} [Fintype C] [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

def QuantumParallelRepetition.exactAliceSourceAtomCode {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)) : ExactJointOutcome X Y A B D → (SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D × Y

Equations

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

def QuantumParallelRepetition.exactBobSourceAtomCode {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)) : ExactJointOutcome X Y A B D → (SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D × X

Equations

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

theorem QuantumParallelRepetition.exactAliceInformationPosterior_eq_jointPushforward {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)) : exactAliceInformationPosterior G n S D = ClassicalInformation.groupedMass (exactAliceSourceAtomCode D) (exactPostselectedJointLaw G n S D)

theorem QuantumParallelRepetition.exactBobInformationPosterior_eq_jointPushforward {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)) : exactBobInformationPosterior G n S D = ClassicalInformation.groupedMass (exactBobSourceAtomCode D) (exactPostselectedJointLaw G n S D)

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 C] [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 Ω] [Fintype I] [Fintype C] [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 : Ω → ℝ) (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 I] [Fintype C] [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] [Fintype I] [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)

def QuantumParallelRepetition.exactReverseAliceContextOutcomeProjection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : ExactReverseAliceFixedInformation X Y D side × (Fin side.card → Y)

Equations

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

def QuantumParallelRepetition.exactReverseBobContextOutcomeProjection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : ExactReverseBobFixedInformation X Y D side × (Fin side.card → X)

Equations

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

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

noncomputable def QuantumParallelRepetition.exactReverseAliceMaskedQuestionRegister {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)) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (xs : Fin n → X) (ys : Fin n → Y) : ExactReverseAliceNextContext X Y A B D side

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobMaskedQuestionRegister {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)) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (xs : Fin n → X) (ys : Fin n → Y) : ExactReverseBobNextContext X Y A B D side

Equations

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

theorem QuantumParallelRepetition.exactReverseAliceMaskedQuestionRegister_stable {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)) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (xs : Fin n → X) (tail : { j : Fin n // j ≠ ↑↑((exactReverseAliceContextAt side seed).sideRank.symm marker) } → Y) (y y' : Y) : exactReverseAliceMaskedQuestionRegister D side default marker flag seed xs ((Equiv.funSplitAt (↑↑((exactReverseAliceContextAt side seed).sideRank.symm marker)) Y).symm (y, tail)) = exactReverseAliceMaskedQuestionRegister D side default marker flag seed xs ((Equiv.funSplitAt (↑↑((exactReverseAliceContextAt side seed).sideRank.symm marker)) Y).symm (y', tail))

theorem QuantumParallelRepetition.exactConditionedReverseAliceNextPrior_flagged_mixture {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) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextPrior G n S D remaining side) = ClassicalInformation.groupedMass (fun (point : (ConditionedAnswerFlag A B D × ExactRemainingSeed D) × ExactOutcome X Y A B n) => (exactReverseAliceMaskedQuestionRegister D side default marker point.1.1 point.1.2 point.2.1 point.2.2.1, point.2.2.1 ↑↑((exactReverseAliceContextAt side point.1.2).sideRank.symm marker))) fun (point : (ConditionedAnswerFlag A B D × ExactRemainingSeed D) × ExactOutcome X Y A B n) => finiteUniformWeight (ConditionedAnswerFlag A B D) * (exactReverseAliceConditionalSeedLaw ⋯ side).weight point.1.2 * (strategyEventLaw (G.repeat n) S).weight point.2

theorem QuantumParallelRepetition.exactReverseAliceMaskedQuestionRegister_determines {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)) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (xs : Fin n → X) (ys : Fin n → Y) (target : ExactReverseAliceNextContext X Y A B D side) (same : exactReverseAliceMaskedQuestionRegister D side default marker flag seed xs ys = target) : xs ↑↑((exactReverseAliceContextAt side seed).sideRank.symm marker) = target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker)

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)

def QuantumParallelRepetition.exactReverseAliceMaskedOutcomeContext {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)) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : ExactReverseAliceNextContext X Y A B D side

Equations

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

theorem QuantumParallelRepetition.exactReverseAliceMaskedOutcomeContext_extract {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)) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : (exactReverseAliceMaskedOutcomeContext G n S D side default marker context outcome).1.1.fst = context

theorem QuantumParallelRepetition.exactConditionedReverseAliceNextJoint_marked_mixture {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) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseAliceNextJoint G n S D remaining side) = ClassicalInformation.groupedMass (fun (point : ExactJointOutcome X Y A B D) => (exactReverseAliceMaskedOutcomeContext G n S D side default marker (exactReverseAliceContextAt side point.1) point.2, point.2.2.1 ↑↑((exactReverseAliceContextAt side point.1).sideRank.symm marker))) fun (point : ExactJointOutcome X Y A B D) => (exactReverseAliceConditionalSeedLaw ⋯ side).weight point.1 * repeatedConditionedOutcomeLaw G n S D point.2

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.exactReverseAliceMaskedOutcomeContext_actual {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) : exactReverseAliceMaskedOutcomeContext G n S D (exactReverseLeftSide seed) default ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩) (exactReverseAliceContextAt (exactReverseLeftSide seed) seed) outcome = exactReverseAliceMarkedHistoryContext G n S D default seed outcome

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

noncomputable def QuantumParallelRepetition.exactReverseAliceContextMarkerInformation {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) (side : Finset (SourceRemainingCoordinate D)) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (marker : Fin side.card) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactReverseAlicePrefixIncrement_eq_contextMarkerInformation {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) (side : Finset (SourceRemainingCoordinate D)) (default : Y) (marker : Fin side.card) : exactConditionedReverseAlicePrefixEntropyIncrement G n S D remaining side default marker = ∑ seed : ExactRemainingSeed D, (exactReverseAliceConditionalSeedLaw ⋯ side).weight seed * exactReverseAliceContextMarkerInformation G n S D remaining default side (exactReverseAliceContextAt side seed) marker

theorem QuantumParallelRepetition.exactReverseAlicePrefixInformation_eq_seedMarkerAverage {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) : exactConditionedReverseAlicePrefixInformation G n S D remaining default = ∑ seed : ExactRemainingSeed D, exactSeedWeight seed * ((∑ marker : Fin (exactReverseLeftSide seed).card, exactReverseAliceContextMarkerInformation G n S D remaining default (exactReverseLeftSide seed) (exactReverseAliceContextAt (exactReverseLeftSide seed) seed) marker) / ↑(exactReverseLeftSide seed).card)

theorem QuantumParallelRepetition.exactReverseAlicePrefixInformation_eq_markedSeedAverage {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) : exactConditionedReverseAlicePrefixInformation G n S D remaining default = ∑ seed : ExactRemainingSeed D, exactSeedWeight seed * exactReverseAliceContextMarkerInformation G n S D remaining default (exactReverseLeftSide seed) (exactReverseAliceContext seed) ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)

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

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

Equations

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

theorem QuantumParallelRepetition.exactReverseAliceMarkedContextInformation_eq_source {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) : exactReverseAliceContextMarkerInformation G n S D remaining default (exactReverseLeftSide seed) (exactReverseAliceContext seed) ((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = exactAliceSourceSeedBornInformation G n S D seed

theorem QuantumParallelRepetition.exactAliceSourceConditionalInformation_eq_seedBornAverage {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 = ∑ seed : ExactRemainingSeed D, exactSeedWeight seed * exactAliceSourceSeedBornInformation G n S D seed

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.exactReverseBobMaskedQuestionRegister_stable {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)) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (ys : Fin n → Y) (tail : { j : Fin n // j ≠ ↑↑((exactReverseBobContextAt side seed).sideRank.symm marker) } → X) (x x' : X) : exactReverseBobMaskedQuestionRegister D side default marker flag seed ((Equiv.funSplitAt (↑↑((exactReverseBobContextAt side seed).sideRank.symm marker)) X).symm (x, tail)) ys = exactReverseBobMaskedQuestionRegister D side default marker flag seed ((Equiv.funSplitAt (↑↑((exactReverseBobContextAt side seed).sideRank.symm marker)) X).symm (x', tail)) ys

theorem QuantumParallelRepetition.exactConditionedReverseBobNextPrior_flagged_mixture {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) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextPrior G n S D remaining side) = ClassicalInformation.groupedMass (fun (point : (ConditionedAnswerFlag A B D × ExactRemainingSeed D) × ExactOutcome X Y A B n) => (exactReverseBobMaskedQuestionRegister D side default marker point.1.1 point.1.2 point.2.1 point.2.2.1, point.2.1 ↑↑((exactReverseBobContextAt side point.1.2).sideRank.symm marker))) fun (point : (ConditionedAnswerFlag A B D × ExactRemainingSeed D) × ExactOutcome X Y A B n) => finiteUniformWeight (ConditionedAnswerFlag A B D) * (exactReverseBobConditionalSeedLaw ⋯ side).weight point.1.2 * (strategyEventLaw (G.repeat n) S).weight point.2

theorem QuantumParallelRepetition.exactReverseBobMaskedQuestionRegister_determines {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)) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (flag : ConditionedAnswerFlag A B D) (seed : ExactRemainingSeed D) (xs : Fin n → X) (ys : Fin n → Y) (target : ExactReverseBobNextContext X Y A B D side) (same : exactReverseBobMaskedQuestionRegister D side default marker flag seed xs ys = target) : ys ↑↑((exactReverseBobContextAt side seed).sideRank.symm marker) = target.1.1.snd.2.2.1 (target.1.1.fst.sideRank.symm marker)

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)

def QuantumParallelRepetition.exactReverseBobMaskedOutcomeContext {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)) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : ExactReverseBobNextContext X Y A B D side

Equations

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

theorem QuantumParallelRepetition.exactReverseBobMaskedOutcomeContext_extract {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)) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (outcome : ExactOutcome X Y A B n) : (exactReverseBobMaskedOutcomeContext G n S D side default marker context outcome).1.1.fst = context

theorem QuantumParallelRepetition.exactConditionedReverseBobNextJoint_marked_mixture {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) : ClassicalInformation.groupedMass (exactPrefixNextCode default marker) (exactConditionedReverseBobNextJoint G n S D remaining side) = ClassicalInformation.groupedMass (fun (point : ExactJointOutcome X Y A B D) => (exactReverseBobMaskedOutcomeContext G n S D side default marker (exactReverseBobContextAt side point.1) point.2, point.2.1 ↑↑((exactReverseBobContextAt side point.1).sideRank.symm marker))) fun (point : ExactJointOutcome X Y A B D) => (exactReverseBobConditionalSeedLaw ⋯ side).weight point.1 * repeatedConditionedOutcomeLaw G n S D point.2

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.exactReverseBobMaskedOutcomeContext_actual {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) : exactReverseBobMaskedOutcomeContext G n S D (exactReverseRightSide seed) default ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) (exactReverseBobContextAt (exactReverseRightSide seed) seed) outcome = exactReverseBobMarkedHistoryContext G n S D default seed outcome

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

noncomputable def QuantumParallelRepetition.exactReverseBobContextMarkedEntropyScore {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) (side : Finset (SourceRemainingCoordinate D)) (context : ExactReverseSideContext (SourceRemainingCoordinate D) side) (marker : Fin side.card) (outcome : ExactOutcome X Y A B n) : ℝ

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobActualMarkedEntropyScore {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) (side : Finset (SourceRemainingCoordinate D)) (seed : ExactRemainingSeed D) (marker : Fin side.card) (outcome : ExactOutcome X Y A B n) : ℝ

Equations

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

theorem QuantumParallelRepetition.exactReverseBobActualMarkedEntropyScore_eq_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)) (remaining : 0 < (Finset.univ \ D).card) (default : X) (side : Finset (SourceRemainingCoordinate D)) (seed : ExactRemainingSeed D) (marker : Fin side.card) (outcome : ExactOutcome X Y A B n) : exactReverseBobActualMarkedEntropyScore G n S D remaining default side seed marker outcome = exactReverseBobContextMarkedEntropyScore G n S D remaining default side (exactReverseBobContextAt side seed) marker outcome

theorem QuantumParallelRepetition.exactConditionedReverseBobPrefixEntropyIncrement_eq_markedOutcomeScore {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) (side : Finset (SourceRemainingCoordinate D)) (default : X) (marker : Fin side.card) : exactConditionedReverseBobPrefixEntropyIncrement G n S D remaining side default marker = ∑ seed : ExactRemainingSeed D, (exactReverseBobConditionalSeedLaw ⋯ side).weight seed * ∑ outcome : ExactOutcome X Y A B n, repeatedConditionedOutcomeLaw G n S D outcome * exactReverseBobActualMarkedEntropyScore G n S D remaining default side seed marker outcome

theorem QuantumParallelRepetition.exactConditionedReverseBobPrefixInformation_eq_sourceMarkerAverage {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) : exactConditionedReverseBobPrefixInformation G n S D remaining default = ∑ seed : ExactRemainingSeed D, exactSeedWeight seed * ((∑ marker : Fin (exactReverseRightSide seed).card, ∑ outcome : ExactOutcome X Y A B n, repeatedConditionedOutcomeLaw G n S D outcome * exactReverseBobActualMarkedEntropyScore G n S D remaining default (exactReverseRightSide seed) seed marker outcome) / ↑(exactReverseRightSide seed).card)

theorem QuantumParallelRepetition.exactConditionedReverseBobPrefixInformation_eq_sourceMarkedOutcomeScore {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) : exactConditionedReverseBobPrefixInformation G n S D remaining default = ∑ seed : ExactRemainingSeed D, exactSeedWeight seed * ∑ outcome : ExactOutcome X Y A B n, repeatedConditionedOutcomeLaw G n S D outcome * exactReverseBobContextMarkedEntropyScore G n S D remaining default (exactReverseRightSide seed) (exactReverseBobContext seed) ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) outcome

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.exactReverseBobActualMarkedEntropy_eq_source {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) : exactReverseBobContextMarkedEntropyScore G n S D remaining default (exactReverseRightSide seed) (exactReverseBobContext seed) ((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) outcome = 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)) ((seed.coordinate, outcome.2.1 ↑seed.coordinate), exactHistoryCode D (seed, outcome))) (G.conditionalXGivenY (outcome.2.1 ↑seed.coordinate))

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

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

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

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

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

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

def QuantumParallelRepetition.ExactSourceOneGameRounding {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Prop

Equations

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

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

theorem QuantumParallelRepetition.exact_standardQuantumParallelRepetition_of_source_rounding {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (rounding : ExactSourceOneGameRounding G) : StandardQuantumParallelRepetition G

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

Equations

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

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

noncomputable def QuantumParallelRepetition.exactSourceGlobalCatalystWinningEffect {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)) (e : ℕ) (a₀ : A) (b₀ : B) (x : X) (y : Y) : Matrix (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e) × Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e)) (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e) × 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.exactSourceGlobalCatalystBasisEquiv {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)) (e : ℕ) : (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) × Fin e × Fin e ≃ Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e) × 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.exactSourceGlobalCatalystAlicePOVM_effect_global {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (e : ℕ) (a₀ a : A) (x : X) (i j : ExactGlobalHistoryLocalIndex G n S D) (k l : Fin e) : (exactSourceGlobalCatalystAlicePOVM G n S D e a₀ x).effect a (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) i, k)) (finProdFinEquiv ((Fintype.equivFin (ExactGlobalHistoryLocalIndex G n S D)) j, l)) = (exactSourceGlobalAlicePOVM G n S D a₀ x).effect a i j * if k = l then 1 else 0

theorem QuantumParallelRepetition.exactSourceGlobalCatalystWinningEffect_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)) (e : ℕ) (a₀ : A) (b₀ : B) (x : X) (y : Y) (i j : (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) × Fin e × Fin e) : exactSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y ((exactSourceGlobalCatalystBasisEquiv G n S D e) i) ((exactSourceGlobalCatalystBasisEquiv G n S D e) j) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (exactSourceGlobalWinningEffect G n S D a₀ b₀ x y) 1 i j

theorem QuantumParallelRepetition.exactSourceGlobalCatalystWinningEffect_tensor_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) (e : ℕ) (residual_positive : 0 < e) (a₀ : A) (b₀ : B) (x : X) (y : Y) : quadraticExpectation (Matrix.toEuclideanCLM (exactSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y)) (tensorEmbezzlementTarget (exactGlobalHistoryFinPsi G n S D r x y)) = quadraticExpectation (Matrix.toEuclideanCLM (exactSourceGlobalWinningEffect G n S D a₀ b₀ x y)) (exactGlobalHistoryVector G n S D r (exactPsi G n S D r x y))

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

theorem QuantumParallelRepetition.exactSourceGlobalCatalystWinningEffect_law_supported_verifier {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)) (positive : 0 < repeatedPostselectionMass G n S D) (e : ℕ) (residual_positive : 0 < e) (a₀ : A) (b₀ : B) (t : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D t ≠ 0) : exactSourceConditionalWinningProbability G n S D t = quadraticExpectation (Matrix.toEuclideanCLM (exactSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ t.2.1 t.2.2.1)) (tensorEmbezzlementTarget (exactGlobalHistoryFinPsi G n S D t.2.2.2 t.2.1 t.2.2.1))

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

Equations

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

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

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

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

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

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

theorem QuantumParallelRepetition.unconditionalMatchedVerifierEffect_tensor_norm_le_one {s : Type u_1} {t : Type u_2} [Fintype s] [Fintype t] [DecidableEq s] [DecidableEq t] (effect : Matrix s s ℂ) (positive : effect.PosSemidef) (complement : (1 - effect).PosSemidef) : ‖Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) effect 1)‖ ≤ 1

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

@[reducible, inline]

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

Equations

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

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

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSelectedCopyIdealStage {d N B m : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m)

Equations

• QuantumParallelRepetition.unconditionalSelectedCopyIdealStage w ξ ζ = QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentTargetState w m ξ ζ

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

Equations

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

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

Equations

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

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

Equations

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

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

theorem QuantumParallelRepetition.unconditionalSelectedCopyRetainedWork_norm_sq {S N d L : ℕ} {τ : Type u_1} [Fintype τ] (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (rest : EuclideanSpace ℂ τ) : ‖unconditionalSelectedCopyRetainedWork width schedule ξ ζ j rest‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * ‖rest‖ ^ 2

theorem QuantumParallelRepetition.unconditionalSelectedCopyMatchedBranch_deviation_sq {S N d L B m : ℕ} {τ : Type u_1} [Fintype τ] (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (rest : EuclideanSpace ℂ τ) (rest_unit : ‖rest‖ = 1) : ‖unconditionalSelectedCopyCleanedMatchedBranch Q width schedule ξ ζ A C j rest - unconditionalSelectedCopyIdealMatchedBranch width schedule ξ ζ j rest‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousCommonStopGaugeStageError Q (width (schedule j)) m ξ ζ A C

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

theorem QuantumParallelRepetition.unconditionalConjugatePOVM_jointEffect {A : Type u_1} {B : Type u_2} {ι : Type u_3} {κ : Type u_4} [Fintype A] [Fintype B] [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (P : POVM A ι) (Q : POVM B κ) (a : A) (b : B) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((unconditionalConjugatePOVM P).effect a) ((unconditionalConjugatePOVM Q).effect b) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.effect a) (Q.effect b)).transpose

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

Equations

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

theorem QuantumParallelRepetition.unconditionalConjugateSourceGlobalCatalystWinningEffect_eq_transpose {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)) (e : ℕ) (a₀ : A) (b₀ : B) (x : X) (y : Y) : unconditionalConjugateSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y = (exactSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y).transpose

theorem QuantumParallelRepetition.unconditionalConjugateSourceGlobalCatalystWinningEffect_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)) (e : ℕ) (a₀ : A) (b₀ : B) (x : X) (y : Y) (z : EuclideanSpace ℂ (Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e) × Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D) * e))) : quadraticExpectation (Matrix.toEuclideanCLM (unconditionalConjugateSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y)) (unconditionalConjugatePureVector z) = quadraticExpectation (Matrix.toEuclideanCLM (exactSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ x y)) z

theorem QuantumParallelRepetition.unconditionalConjugateSourceGlobalCatalystWinningEffect_law_supported {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)) (positive : 0 < repeatedPostselectionMass G n S D) (e : ℕ) (residual_positive : 0 < e) (a₀ : A) (b₀ : B) (u : ExactLocallySampleableTuple X Y A B D) (supported : exactLocallySampleableLaw G n S D u ≠ 0) : quadraticExpectation (Matrix.toEuclideanCLM (unconditionalConjugateSourceGlobalCatalystWinningEffect G n S D e a₀ b₀ u.2.1 u.2.2.1)) (unconditionalConjugatePureVector (tensorEmbezzlementTarget (exactGlobalHistoryFinPsi G n S D u.2.2.2 u.2.1 u.2.2.1))) = exactSourceConditionalWinningProbability G n S D u

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

theorem QuantumParallelRepetition.unconditionalMixedConjugateSigmaLocalAction_apply {d m : ℕ} (B : ℕ) (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (z : EuclideanSpace ℂ (((_ : Fin B × Fin d) × Fin m) × (_ : Fin B × Fin d) × Fin m)) (φ ψ : Fin B) (i j : Fin d) (a b : Fin m) : (unconditionalMixedConjugateSigmaLocalAction B U V z).ofLp (⟨(φ, i), a⟩, ⟨(ψ, j), b⟩) = ∑ k : Fin d, ∑ l : Fin d, ↑U i k * ↑V j l * z.ofLp (⟨(φ, k), a⟩, ⟨(ψ, l), b⟩)

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

Equations

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

theorem QuantumParallelRepetition.unconditionalMixedConjugateTargetCovariance {d N B n : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (dimension : 0 < d) (ξ ζ : BipartiteUnitVector d) : √(w * ↑d) • unconditionalMixedConjugateSigmaLocalAction B (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis ξ)) (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis ζ)) (dSVDensityRationalPublicBucketPhysicalCoherentTargetState w n ξ ζ) = unconditionalMixedConjugateAcceptedPhaseHarmonicTarget w n ξ

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

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

theorem QuantumParallelRepetition.unconditionalSelectedCopy_conjugateAcceptedTarget_norm_sq {d N B m : ℕ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (w : ℝ) (ξ : BipartiteUnitVector d) : ‖unconditionalMixedConjugateAcceptedPhaseHarmonicTarget w m ξ‖ ^ 2 = ‖dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2

theorem QuantumParallelRepetition.unconditionalSelectedCopy_mixedConjugateLocalAction_norm {d B m : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin d) ℂ)) (z : EuclideanSpace ℂ (((_ : Fin B × Fin d) × Fin m) × (_ : Fin B × Fin d) × Fin m)) : ‖unconditionalMixedConjugateSigmaLocalAction B U V z‖ = ‖z‖

theorem QuantumParallelRepetition.unconditionalSelectedCopyIdealStage_norm_sq {d N B m : ℕ} {w : ℝ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : 0 < w) (ξ ζ : BipartiteUnitVector d) : ‖unconditionalSelectedCopyIdealStage w ξ ζ‖ ^ 2 = dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension w ξ

theorem QuantumParallelRepetition.unconditionalSelectedCopyCleanedStage_norm_sq {d N B m : ℕ} {w : ℝ} (phases : 0 < B) (grid : 0 < N) (harmonic : 0 < m) (width : 0 < w) (ξ ζ : BipartiteUnitVector d) (Q : ℕ) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) : ‖unconditionalSelectedCopyCleanedStage Q w ξ ζ A C‖ ^ 2 = ‖dSVDensityRationalCompleteProjectiveOutcome w N ξ ζ true true‖ ^ 2

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

theorem QuantumParallelRepetition.unconditionalSelectedCopyIdealMatchedBranch_norm_sq {S N d L B m : ℕ} {τ : Type u_1} [Fintype τ] (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) (width : Fin S → ℝ) (width_positive : ∀ (s : Fin S), 0 < width s) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (rest : EuclideanSpace ℂ τ) (rest_unit : ‖rest‖ = 1) : ‖unconditionalSelectedCopyIdealMatchedBranch width schedule ξ ζ j rest‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule j)) ξ

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

Equations

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

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

Equations

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

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

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

theorem QuantumParallelRepetition.unconditionalMixedConjugateSelectedBranchCovariance {S N d L B m : ℕ} {τ : Type u_1} [Fintype τ] [DecidableEq τ] (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (positive : 0 < width (schedule j)) (rest : EuclideanSpace ℂ τ) : √(width (schedule j) * ↑d) • unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis ξ))) (unconditionalMixedConjugateSigmaAtomLift B (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis ζ))) (unconditionalSelectedCopyIdealMatchedBranch width schedule ξ ζ j rest) = unconditionalMatchedVerifierTensor (unconditionalMixedConjugateAcceptedPhaseHarmonicTarget (width (schedule j)) m ξ) (unconditionalSelectedCopyRetainedWork width schedule ξ ζ j rest)

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

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

theorem QuantumParallelRepetition.actualStoppingGlobalWinningEffect_same {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype R] [DecidableEq R] {ι κ : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (r s : R) (x : X) (y : Y) (i i' : ι r) (j j' : κ s) : actualStoppingGlobalWinningEffect G PA PB x y (⟨r, i⟩, ⟨s, j⟩) (⟨r, i'⟩, ⟨s, j'⟩) = actualStoppingBranchWinningEffect G PA PB r s x y (i, j) (i', j')

theorem QuantumParallelRepetition.actualStoppingGlobalWinningEffect_cross_eq_zero {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype R] [DecidableEq R] {ι κ : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] [(r : R) → Fintype (κ r)] [(r : R) → DecidableEq (κ r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (s : R) → Y → POVM B (κ s)) (r s r' s' : R) (x : X) (y : Y) (i : ι r) (j : κ s) (i' : ι r') (j' : κ s') (different : r ≠ r' ∨ s ≠ s') : actualStoppingGlobalWinningEffect G PA PB x y (⟨r, i⟩, ⟨s, j⟩) (⟨r', i'⟩, ⟨s', j'⟩) = 0

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

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

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

Equations

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

theorem QuantumParallelRepetition.actualStoppingQuestionLocalWinningEffect_quadratic {X Y A B R : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype R] [DecidableEq R] {ι : R → Type} [(r : R) → Fintype (ι r)] [(r : R) → DecidableEq (ι r)] (G : Game X Y A B) (PA : (r : R) → X → POVM A (ι r)) (PB : (r : R) → Y → POVM B (ι r)) (U : X → ↥(Matrix.unitaryGroup ((r : R) × ι r) ℂ)) (V : Y → ↥(Matrix.unitaryGroup ((r : R) × ι r) ℂ)) (z : EuclideanSpace ℂ (((r : R) × ι r) × (r : R) × ι r)) (normalized : ‖z‖ = 1) (x : X) (y : Y) : quadraticExpectation (Matrix.toEuclideanCLM (pureVerifierEffect G z normalized (fun (x : X) => unitaryConjugatePOVM (U x) (dependentBlockPOVM fun (r : R) => PA r x)) (fun (y : Y) => unitaryConjugatePOVM (V y) (dependentBlockPOVM fun (r : R) => PB r y)) x y)) z = quadraticExpectation (Matrix.toEuclideanCLM (actualStoppingGlobalWinningEffect G PA PB x y)) (actualStoppingQuestionLocalAction (U x) (V y) z)

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

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

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

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseHistoryFamily (B N d L : ℕ) : Type

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseStoppedState (B N d L m : ℕ) (S T : DSVDensityRationalPublicLogPhaseHistoryFamily B N d L) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m) × Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m))

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicMultiscaleOriginalSigmaTargetFirstEquiv (S B N d L m : ℕ) : (_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) × Fin m ≃ Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalAliceHistoryFamily (S B N d L : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) : DSVDensityRationalPublicLogPhaseHistoryFamily (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B)) N d L

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalBobHistoryFamily (S B N d L : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) : DSVDensityRationalPublicLogPhaseHistoryFamily (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B)) N d L

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalStoppedState (S B N d L m : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalSameStopStateEquiv (S B N d L m : ℕ) : EuclideanSpace ℂ (((_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) × Fin m) × (_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) × Fin m) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))

Equations

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

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalSameStopSigmaSource (S B N d L m : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))

Equations

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

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalSameStopSigmaSource_apply (S B N d L m : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (φ ψ : DSVDensityRationalPublicMultiscalePhaseIndex S B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) (i j : Fin m) : (dSVDensityRationalHeterogeneousOriginalSameStopSigmaSource S B N d L m width schedule ξ ζ).ofLp ((dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m) ((φ, a), i), (dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m) ((ψ, b), j)) = (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B))).ofLp (φ, ψ) * (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (a, b) * (embezzlementState m).ofLp (i, j)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalSameStopSigmaSource_eq_stopped (S B N d L m : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousOriginalSameStopSigmaSource S B N d L m width schedule ξ ζ = dSVDensityRationalHeterogeneousOriginalStoppedState S B N d L m width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousOriginalStoppedState_apply (S B N d L m : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (φ ψ : DSVDensityRationalPublicMultiscalePhaseIndex S B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) (i j : Fin m) : (dSVDensityRationalHeterogeneousOriginalStoppedState S B N d L m width schedule ξ ζ).ofLp ((dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m) ((φ, a), i), (dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m) ((ψ, b), j)) = (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B))).ofLp (φ, ψ) * (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (a, b) * (embezzlementState m).ofLp (i, j)

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

Equations

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

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

Equations

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

@[simp]

theorem QuantumParallelRepetition.directDSVSelectedCopyLocalHistoryEquiv_hit {L : ℕ} {β : Type u_1} (j : Fin L) (selected : β) (before : Fin ↑j → β) (after : Fin (L - ↑j) → β) : (directDSVSelectedCopyLocalHistoryEquiv j) (selected, before, after) j.castSucc = selected

@[simp]

theorem QuantumParallelRepetition.directDSVSelectedCopyLocalHistoryEquiv_before {L : ℕ} {β : Type u_1} (j : Fin L) (selected : β) (before : Fin ↑j → β) (after : Fin (L - ↑j) → β) (i : Fin ↑j) : (directDSVSelectedCopyLocalHistoryEquiv j) (selected, before, after) ⟨↑i, ⋯⟩ = before i

@[simp]

theorem QuantumParallelRepetition.directDSVSelectedCopyLocalHistoryEquiv_after {L : ℕ} {β : Type u_1} (j : Fin L) (selected : β) (before : Fin ↑j → β) (after : Fin (L - ↑j) → β) (i : Fin (L - ↑j)) : (directDSVSelectedCopyLocalHistoryEquiv j) (selected, before, after) ⟨↑j + 1 + ↑i, ⋯⟩ = after i

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

theorem QuantumParallelRepetition.directDSVActualStoppingSelectedHistory_sourceProduct {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) (selectedA selectedB : DSVUniformDensityThresholdLocalIndex N d) (beforeA beforeB : Fin ↑j → DSVUniformDensityThresholdLocalIndex N d) (afterA afterB : Fin (L - ↑j) → DSVUniformDensityThresholdLocalIndex N d) : (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (⟨j.succ, (directDSVSelectedCopyLocalHistoryEquiv j) (selectedA, beforeA, afterA)⟩, ⟨j.succ, (directDSVSelectedCopyLocalHistoryEquiv j) (selectedB, beforeB, afterB)⟩) = ((dSVDensityRationalCompleteProjectiveOutcome (width (schedule j)) N ξ ζ true true).ofLp (selectedA, selectedB) * (dSVDensityRationalHeterogeneousStoppedCommonPrefixFailureVector width schedule ξ ζ j).ofLp fun (i : Fin ↑j) => (beforeA i, beforeB i)) * (dSVUniformDensityIndependentSharedState (L - ↑j) N d).ofLp (afterA, afterB)

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalSourcePhysicalStoppingTargetFirstStateEquiv (S B N d L m : ℕ) : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (((_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m) × (_ : Fin (L + 1)) × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m)

Equations

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

theorem QuantumParallelRepetition.unconditionalSourcePhysicalStoppingTargetFirst_branch_apply {S B N d L m : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (r s : Fin (L + 1)) (φ ψ : DSVDensityRationalPublicMultiscalePhaseIndex S B) (a b : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d) (i k : Fin m) : (actualStoppingBranchVector ((unconditionalSourcePhysicalStoppingTargetFirstStateEquiv S B N d L m) (dSVDensityRationalHeterogeneousOriginalStoppedState S B N d L m width schedule ξ ζ)) r s).ofLp (⟨(φ, a), i⟩, ⟨(ψ, b), k⟩) = (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B))).ofLp (φ, ψ) * (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (⟨r, a⟩, ⟨s, b⟩) * (embezzlementState m).ofLp (i, k)

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

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

Equations

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

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

Equations

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

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

theorem QuantumParallelRepetition.unconditionalSelectedMultiscalePhase_EPR_apply {S B : ℕ} (scale : Fin (S + 1)) (p q : Fin B) (r t : Fin (Fintype.card (Fin S → Fin B))) : (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase (S + 1) B))).ofLp ((unconditionalSelectedMultiscalePhaseIndexEquiv scale) (p, r), (unconditionalSelectedMultiscalePhaseIndexEquiv scale) (q, t)) = (ePRState B).ofLp (p, q) * (ePRState (Fintype.card (Fin S → Fin B))).ofLp (r, t)

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

Equations

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

theorem QuantumParallelRepetition.unconditionalActualMultiscalePhase_EPR_apply {S B : ℕ} (scale : Fin S) (p q : Fin B) (r t : Fin (Fintype.card (Fin (S - 1) → Fin B))) : (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B))).ofLp ((unconditionalActualMultiscalePhaseIndexEquiv scale) (p, r), (unconditionalActualMultiscalePhaseIndexEquiv scale) (q, t)) = (ePRState B).ofLp (p, q) * (ePRState (Fintype.card (Fin (S - 1) → Fin B))).ofLp (r, t)

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

Equations

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

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

Equations

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

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

Equations

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

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

theorem QuantumParallelRepetition.unconditionalSourcePhysicalCleanedStoppingLocalAction_reindex {S B N d L m : ℕ} (U V : ↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)) ℂ)) (z : EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))) : actualStoppingQuestionLocalAction (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m U) (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m V) ((unconditionalSourcePhysicalStoppingTargetFirstStateEquiv S B N d L m) z) = (unconditionalSourcePhysicalStoppingTargetFirstStateEquiv S B N d L m) (localUnitaryAction U V z)

theorem QuantumParallelRepetition.unconditionalSourcePhysicalCleanedStoppingFixedSource_physicalAction {S B N d L m : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : actualStoppingQuestionLocalAction (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralAlice S B N d L m width schedule ξ)) (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralBob S B N d L m width schedule ζ)) (unconditionalSourcePhysicalCleanedStoppingFixedSource S B N d L m) = (unconditionalSourcePhysicalStoppingTargetFirstStateEquiv S B N d L m) (dSVDensityRationalHeterogeneousOriginalStoppedState S B N d L m width schedule ξ ζ)

theorem QuantumParallelRepetition.unconditionalSourcePhysicalCleanedStoppingFixedSource_branch_apply {S B N d L m : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (r s : Fin (L + 1)) (φ ψ : DSVDensityRationalPublicMultiscalePhaseIndex S B) (a b : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d) (i k : Fin m) : (actualStoppingBranchVector (actualStoppingQuestionLocalAction (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralAlice S B N d L m width schedule ξ)) (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralBob S B N d L m width schedule ζ)) (unconditionalSourcePhysicalCleanedStoppingFixedSource S B N d L m)) r s).ofLp (⟨(φ, a), i⟩, ⟨(ψ, b), k⟩) = (ePRState (Fintype.card (DSVDensityRationalPublicMultiscalePhase S B))).ofLp (φ, ψ) * (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (⟨r, a⟩, ⟨s, b⟩) * (embezzlementState m).ofLp (i, k)

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

Equations

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

@[simp]

theorem QuantumParallelRepetition.unconditionalSourcePhysicalCleanedSelectedHistoryEquiv_hit {L : ℕ} (j : Fin L) (β : Type u_1) (f : Fin (L + 1) → β) : ((unconditionalSourcePhysicalCleanedSelectedHistoryEquiv j β) f).1 = f j.castSucc

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

• QuantumParallelRepetition.unconditionalActualCleanedSelectedStageBucketUnitary Q w ξ A = QuantumParallelRepetition.unconditionalSourcePhysicalCleanedSelectedStageUnitary Q w ξ A

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

theorem QuantumParallelRepetition.unconditionalActualCleanedSelectedMatchedStoppingBranch {S B N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex S B ≃ Fin B × R) (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) : actualStoppingBranchVector (dSVUniformDensityPhysicalAsyncSigmaContinuation (unconditionalActualCleanedSelectedFiniteStageDecoder phaseSplit Q width schedule ξ (dSVUniformDensityAliceHistorySpectralCopy ξ) A) (unconditionalActualCleanedSelectedFiniteStageDecoder phaseSplit Q width schedule ζ (dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ C) (actualStoppingQuestionLocalAction (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralAlice S B N d L m width schedule ξ)) (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralBob S B N d L m width schedule ζ)) (unconditionalSourcePhysicalCleanedStoppingFixedSource S B N d L m))) j.succ j.succ = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑(unconditionalActualCleanedSelectedFullStageUnitary phaseSplit Q width schedule ξ (dSVUniformDensityAliceHistorySpectralCopy ξ) A j) ↑(unconditionalActualCleanedSelectedFullStageUnitary phaseSplit Q width schedule ζ (dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ C j)).mulVec (actualStoppingBranchVector ((unconditionalSourcePhysicalStoppingTargetFirstStateEquiv S B N d L m) (dSVDensityRationalHeterogeneousOriginalStoppedState S B N d L m width schedule ξ ζ)) j.succ j.succ).ofLp)

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualPhysicalMixedAcceptedRawStage {B N d m : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m)

Equations

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

theorem QuantumParallelRepetition.unconditionalActualPhysicalMixedAcceptedSpectralGauge_apply {B N d m : ℕ} (U : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)) (φ ψ : Fin B) (i j : Fin d) (k l : Fin N) (a b : Fin m) : ↑(unconditionalActualCleanedSelectedStageSpectralUnitary U) ⟨(φ, i), finProdFinEquiv (k, a)⟩ ⟨(ψ, j), finProdFinEquiv (l, b)⟩ = if φ = ψ then ↑U ⟨k, i⟩ ⟨l, j⟩ * if a = b then 1 else 0 else 0

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

theorem QuantumParallelRepetition.unconditionalActualPhysicalMixedAcceptedSpectralGauge_stage {B N d m : ℕ} {w : ℝ} (width : 0 < w) (grid : 0 < N) (ξ ζ : BipartiteUnitVector d) : WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑(unconditionalActualCleanedSelectedStageSpectralUnitary (dSVUniformDensityAliceHistorySpectralCopy ξ)) ↑(unconditionalActualCleanedSelectedStageSpectralUnitary (dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹)).mulVec (unconditionalActualPhysicalMixedAcceptedRawStage w ξ ζ).ofLp) = dSVDensityRationalPublicBucketPhysicalCoherentMixedState w m ξ ζ

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

noncomputable def QuantumParallelRepetition.unconditionalActualCanonicalRawSelectedPhysicalStage {B N d m : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m)

Equations

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

theorem QuantumParallelRepetition.unconditionalActualCanonicalCleanedHistorySymm_eq_direct {L : ℕ} (j : Fin L) (β : Type u_1) (selected : β) (before : Fin ↑j → β) (later : Fin (L - ↑j) → β) : (unconditionalSourcePhysicalCleanedSelectedHistoryEquiv j β).symm (selected, before, later) = (directDSVSelectedCopyLocalHistoryEquiv j) (selected, before, later)

theorem QuantumParallelRepetition.unconditionalActualCanonicalFullSource_eq_rawSelectedStage {S B N d L m : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (j : Fin L) : (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualMultiscalePhaseIndexEquiv (schedule j)).symm j) (unconditionalActualCanonicalFixedSourceMatchedBranch width schedule ξ ζ j) = unconditionalMatchedVerifierTensor (unconditionalActualCanonicalRawSelectedPhysicalStage (width (schedule j)) ξ ζ) (unconditionalSelectedCopyRetainedWork width schedule ξ ζ j (unconditionalActualCanonicalRetainedPhaseTail j))

theorem QuantumParallelRepetition.unconditionalActualCanonicalRawSelectedPhysicalStage_eq {B N d m : ℕ} (w : ℝ) (ξ ζ : BipartiteUnitVector d) : unconditionalActualCanonicalRawSelectedPhysicalStage w ξ ζ = unconditionalActualPhysicalMixedAcceptedRawStage w ξ ζ

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

Equations

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

@[simp]

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

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

Equations

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

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

Equations

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

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

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

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

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

def QuantumParallelRepetition.unconditionalSelectedRetainedBilateralRegroup (ι τ : Type) : (ι × τ) × ι × τ ≃ (ι × ι) × τ × τ

Equations

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

theorem QuantumParallelRepetition.unconditionalRegroupedSelectedRetainedReindexAction {κ ι τ δ : Type} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] [Fintype τ] [DecidableEq τ] [Fintype δ] [DecidableEq δ] (e : κ ≃ ι × τ) (workEquiv : τ × τ ≃ δ) (U V : ↥(Matrix.unitaryGroup ι ℂ)) (z : EuclideanSpace ℂ (κ × κ)) : have regroup := (unconditionalSelectedRetainedBilateralRegroup ι τ).trans ((Equiv.refl (ι × ι)).prodCongr workEquiv); have sigma := (Equiv.prodComm ι τ).trans (Equiv.sigmaEquivProd τ ι).symm; have localEquiv := e.trans sigma; have A := unconditionalSourceFixedPureStoppedSigmaReindexedUnitary localEquiv.symm (coherentSharedRandomControlledUnitary fun (x : τ) => U); have B := unconditionalSourceFixedPureStoppedSigmaReindexedUnitary localEquiv.symm (coherentSharedRandomControlledUnitary fun (x : τ) => V); have state := LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((e.prodCongr e).trans regroup); state (WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑A ↑B).mulVec z.ofLp)) = unconditionalMixedConjugateSelectedBranchLocalAction U V (state z)

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

Equations

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

theorem QuantumParallelRepetition.unconditionalActualFixedSourceFullBilateralRegroup_eq {B N d L m : ℕ} {R : Type} (j : Fin L) : unconditionalSourcePhysicalCleanedFullBilateralRegroup j = (unconditionalSelectedRetainedBilateralRegroup (UnconditionalSelectedCopyLocalIndex B d N m) (UnconditionalActualCleanedSelectedRetainedIndex j R)).trans ((Equiv.refl (UnconditionalSelectedCopyLocalIndex B d N m × UnconditionalSelectedCopyLocalIndex B d N m)).prodCongr (unconditionalActualFixedSourceRetainedHistoryPairEquiv j))

theorem QuantumParallelRepetition.unconditionalActualFixedSourceFullPhysicalBilateralStageTransport {S B N d L m : ℕ} {R : Type} [Fintype R] [DecidableEq R] (phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex S B ≃ Fin B × R) (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (spectralA spectralB : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdLocalIndex N d) ℂ)) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (z : EuclideanSpace ℂ (UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m × UnconditionalSourcePhysicalStoppingPhaseFiber S B N d L m)) : (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry phaseSplit j) (WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑(unconditionalActualCleanedSelectedFullStageUnitary phaseSplit Q width schedule ξ spectralA A j) ↑(unconditionalActualCleanedSelectedFullStageUnitary phaseSplit Q width schedule ζ spectralB C j)).mulVec z.ofLp)) = unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalActualCleanedSelectedStageBucketUnitary Q (width (schedule j)) ξ A * unconditionalActualCleanedSelectedStageSpectralUnitary spectralA) (unconditionalActualCleanedSelectedStageBucketUnitary Q (width (schedule j)) ζ C * unconditionalActualCleanedSelectedStageSpectralUnitary spectralB) ((unconditionalSourcePhysicalCleanedFullBilateralStateIsometry phaseSplit j) z)

theorem QuantumParallelRepetition.unconditionalActualFixedSourceDecodedMatchedBranch {S B N d L m : ℕ} (Q : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (j : Fin L) (positive : 0 < width (schedule j)) (grid : 0 < N) : (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualMultiscalePhaseIndexEquiv (schedule j)).symm j) (actualStoppingBranchVector (dSVUniformDensityPhysicalAsyncSigmaContinuation (unconditionalActualCleanedSelectedFiniteStageDecoder (unconditionalActualMultiscalePhaseIndexEquiv (schedule j)).symm Q width schedule ξ (dSVUniformDensityAliceHistorySpectralCopy ξ) A) (unconditionalActualCleanedSelectedFiniteStageDecoder (unconditionalActualMultiscalePhaseIndexEquiv (schedule j)).symm Q width schedule ζ (dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ C) (actualStoppingQuestionLocalAction (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralAlice S B N d L m width schedule ξ)) (unconditionalSourcePhysicalCleanedTargetFirstUnitary S B N d L m (dSVDensityRationalHeterogeneousTargetFirstSpectralBob S B N d L m width schedule ζ)) (unconditionalSourcePhysicalCleanedStoppingFixedSource S B N d L m))) j.succ j.succ) = unconditionalSelectedCopyCleanedMatchedBranch Q width schedule ξ ζ A C j (unconditionalActualCanonicalRetainedPhaseTail j)