Quantum parallel repetition, part 06 #
theorem
QuantumParallelRepetition.exactAliceQuestionConditionalWeight_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
:
(∑ q : ExactFullQuestion X Y n,
if exactRevealCode D seed q = history ∧ q.1 ↑seed.coordinate = x then
exactPriorQuestionWeight G n q / exactAliceQuestionMass G n D seed history x
else 0) = if exactAliceQuestionMass G n D seed history x = 0 then 0 else 1
theorem
QuantumParallelRepetition.exactBobQuestionConditionalWeight_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(y : Y)
:
(∑ q : ExactFullQuestion X Y n,
if exactRevealCode D seed q = history ∧ q.2 ↑seed.coordinate = y then
exactPriorQuestionWeight G n q / exactBobQuestionMass G n D seed history y
else 0) = if exactBobQuestionMass G n D seed history y = 0 then 0 else 1
theorem
QuantumParallelRepetition.exactAliceQuestionFilter_complement_posSemidef
{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)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → A)
(x : X)
:
(1 - exactAliceQuestionFilter G n S D seed history answer x).PosSemidef
theorem
QuantumParallelRepetition.exactBobQuestionFilter_complement_posSemidef
{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)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → B)
(y : Y)
:
(1 - exactBobQuestionFilter G n S D seed history answer y).PosSemidef
theorem
QuantumParallelRepetition.exactAliceMeanFilter_complement_posSemidef
{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)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → A)
(y : Y)
:
(1 - exactAliceMeanFilter G n S D seed history answer y).PosSemidef
theorem
QuantumParallelRepetition.exactBobMeanFilter_complement_posSemidef
{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)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → B)
(x : X)
:
(1 - exactBobMeanFilter G n S D seed history answer x).PosSemidef
theorem
QuantumParallelRepetition.exactFairAliceMean_spectral_entropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(y : Y)
:
-((bornTracePairing S.state.matrix)
(cfc (fun (z : ℝ) => z * Real.log z) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y)))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y) ≤ (((bornTracePairing S.state.matrix) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)).negMulLog
theorem
QuantumParallelRepetition.exactFairBobMean_spectral_entropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(x : X)
:
-((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(cfc (fun (z : ℝ) => z * Real.log z) (exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x)) ≤ (((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x)).negMulLog
theorem
QuantumParallelRepetition.exactFairAliceHistoryHighOperatorPotential_nonpos
{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))
(r : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactFairBobHistoryHighOperatorPotential_nonpos
{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))
(r : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactFairAliceHistoryLowOperatorPotential_neg_le_entropy
{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))
(r : ExactHistoryFlag X Y A B D)
:
-exactFairAliceHistoryLowOperatorPotential G n S D r ≤ ∑ y : Y,
G.marginalY y * (((bornTracePairing S.state.matrix) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)).negMulLog
theorem
QuantumParallelRepetition.exactFairBobHistoryLowOperatorPotential_neg_le_entropy
{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))
(r : ExactHistoryFlag X Y A B D)
:
-exactFairBobHistoryLowOperatorPotential G n S D r ≤ ∑ x : X,
G.marginalX x * (((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x)).negMulLog
theorem
QuantumParallelRepetition.exactReverseAliceFilterHighOperatorPotential_nonpos
{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))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
theorem
QuantumParallelRepetition.exactReverseBobFilterHighOperatorPotential_nonpos
{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))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
theorem
QuantumParallelRepetition.groupedMass_expectation
{Ω : Type u_5}
{T : Type u_6}
[Fintype Ω]
[Fintype T]
[DecidableEq T]
(code : Ω → T)
(weight : Ω → ℝ)
(f : T → ℝ)
:
∑ t : T, ClassicalInformation.groupedMass code weight t * f t = ∑ outcome : Ω, weight outcome * f (code outcome)
theorem
QuantumParallelRepetition.exactJointQuestionMass_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
:
exactJointQuestionMass G n D seed history x y = ClassicalInformation.groupedMass
(fun (q : ExactFullQuestion X Y n) => (exactRevealCode D seed q, q.1 ↑seed.coordinate, q.2 ↑seed.coordinate))
(exactPriorQuestionWeight G n) (history, x, y)
theorem
QuantumParallelRepetition.exactFairJointQuestionExpectation_reindex
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(f : ExactRevealHistory X Y D seed → X → Y → ℝ)
:
∑ history : ExactRevealHistory X Y D seed,
∑ x : X, ∑ y : Y, exactRevealMass G n D seed history * G.questionWeight x y * f history x y = ∑ q : ExactFullQuestion X Y n,
exactPriorQuestionWeight G n q * f (exactRevealCode D seed q) (q.1 ↑seed.coordinate) (q.2 ↑seed.coordinate)
theorem
QuantumParallelRepetition.exactFairAliceHistoryHighOperatorPotential_eq_joint
{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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairAliceHistoryHighOperatorPotential G n S D r = ∑ x : X,
∑ y : Y,
G.questionWeight x y * ((bornTracePairing S.state.matrix)
(cfc (fun (z : ℝ) => z * Real.log z) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x)))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)
theorem
QuantumParallelRepetition.exactFairBobHistoryHighOperatorPotential_eq_joint
{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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairBobHistoryHighOperatorPotential G n S D r = ∑ x : X,
∑ y : Y,
G.questionWeight x y * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(cfc (fun (z : ℝ) => z * Real.log z) (exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y))
theorem
QuantumParallelRepetition.exactFairAliceHistoryLowOperatorPotential_eq_joint
{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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairAliceHistoryLowOperatorPotential G n S D r = ∑ x : X,
∑ y : Y,
G.questionWeight x y * ((bornTracePairing S.state.matrix)
(cfc (fun (z : ℝ) => z * Real.log z) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y)))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)
theorem
QuantumParallelRepetition.exactFairBobHistoryLowOperatorPotential_eq_joint
{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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairBobHistoryLowOperatorPotential G n S D r = ∑ x : X,
∑ y : Y,
G.questionWeight x y * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(cfc (fun (z : ℝ) => z * Real.log z) (exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x))
theorem
QuantumParallelRepetition.exactFairAcceptedJointStatistic_reindex
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
:
∀ (x : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D)
(f : ExactRevealHistory X Y D seed → (↥D → A) → (↥D → B) → X → Y → ℝ),
(∑ history : ExactRevealHistory X Y D seed,
∑ aliceAnswer : ↥D → A,
∑ bobAnswer : ↥D → B,
if exactHistoryAccepted G n D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } then
exactRevealMass G n D seed history * ∑ x : X, ∑ y : Y, G.questionWeight x y * f history aliceAnswer bobAnswer x y
else 0) = ∑ q : ExactFullQuestion X Y n,
exactPriorQuestionWeight G n q * ∑ aliceAnswer : ↥D → A,
∑ bobAnswer : ↥D → B,
if exactHistoryAccepted G n D
{ seed := seed, history := exactRevealCode D seed q, aliceAnswer := aliceAnswer,
bobAnswer := bobAnswer } then
f (exactRevealCode D seed q) aliceAnswer bobAnswer (q.1 ↑seed.coordinate) (q.2 ↑seed.coordinate)
else 0
theorem
QuantumParallelRepetition.exactPriorQuestion_coordinate_weight_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 : ℕ)
(q : ExactFullQuestion X Y n)
(supported : exactPriorQuestionWeight G n q ≠ 0)
(j : Fin n)
:
theorem
QuantumParallelRepetition.exactRevealCode_update_distinguished_alice
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(q : ExactFullQuestion X Y n)
(x : X)
:
theorem
QuantumParallelRepetition.exactRevealCode_update_distinguished_bob
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(q : ExactFullQuestion X Y n)
(y : Y)
:
theorem
QuantumParallelRepetition.exactReverseBobMarker_induction
{n : ℕ}
(D : Finset (Fin n))
(P :
(side : Finset (SourceRemainingCoordinate D)) →
ExactReverseSideContext (SourceRemainingCoordinate D) side → Fin side.card → Prop)
(allSeeds :
∀ (seed : ExactRemainingSeed D),
P (exactReverseRightSide seed) (exactReverseBobContext seed)
((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
P side context marker
theorem
QuantumParallelRepetition.exactReverseAliceMarker_induction
{n : ℕ}
(D : Finset (Fin n))
(P :
(side : Finset (SourceRemainingCoordinate D)) →
ExactReverseSideContext (SourceRemainingCoordinate D) side → Fin side.card → Prop)
(allSeeds :
∀ (seed : ExactRemainingSeed D),
P (exactReverseLeftSide seed) (exactReverseAliceContext seed)
((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
P side context marker
theorem
QuantumParallelRepetition.exactFairFullOutcomeBornMass_accepted_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))
(seed : ExactRemainingSeed D)
:
(∑ history : ExactRevealHistory X Y D seed,
∑ aliceAnswer : ↥D → A,
∑ bobAnswer : ↥D → B,
if exactHistoryAccepted G n D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } then
∑ x : X,
∑ y : Y,
exactFairFullOutcomeBornMass G n S D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } x y
else 0) = repeatedPostselectionMass G n S D
theorem
QuantumParallelRepetition.exactFairFullOutcomeBornMass_eq_reveal_question_born
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(x : X)
(y : Y)
:
exactFairFullOutcomeBornMass G n S D r x y = exactRevealMass G n D r.seed r.history * G.questionWeight x y * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)
theorem
QuantumParallelRepetition.exactFairAliceMeanBorn_eq_conditional
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(y : Y)
:
((bornTracePairing S.state.matrix) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y) = ∑ x : X,
G.conditionalXGivenY y x * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)
theorem
QuantumParallelRepetition.exactFairBobMeanBorn_eq_conditional
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(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)
:
((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x) = ∑ y : Y,
G.conditionalYGivenX x y * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)
theorem
QuantumParallelRepetition.exactFairAliceMeanBornMass_eq_fullOutcome_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))
(r : ExactHistoryFlag X Y A B D)
:
exactRevealMass G n D r.seed r.history * ∑ y : Y,
G.marginalY y * ((bornTracePairing S.state.matrix) (exactAliceMeanFilter G n S D r.seed r.history r.aliceAnswer y))
(exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y) = ∑ x : X, ∑ y : Y, exactFairFullOutcomeBornMass G n S D r x y
theorem
QuantumParallelRepetition.exactFairBobMeanBornMass_eq_fullOutcome_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))
(r : ExactHistoryFlag X Y A B D)
:
exactRevealMass G n D r.seed r.history * ∑ x : X,
G.marginalX x * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x))
(exactBobMeanFilter G n S D r.seed r.history r.bobAnswer x) = ∑ x : X, ∑ y : Y, exactFairFullOutcomeBornMass G n S D r x y
theorem
QuantumParallelRepetition.exactFairAliceMeanAcceptedBornMass_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))
(seed : ExactRemainingSeed D)
:
(∑ history : ExactRevealHistory X Y D seed,
∑ aliceAnswer : ↥D → A,
∑ bobAnswer : ↥D → B,
if exactHistoryAccepted G n D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } then
exactRevealMass G n D seed history * ∑ y : Y,
G.marginalY y * ((bornTracePairing S.state.matrix) (exactAliceMeanFilter G n S D seed history aliceAnswer y))
(exactBobQuestionFilter G n S D seed history bobAnswer y)
else 0) = repeatedPostselectionMass G n S D
theorem
QuantumParallelRepetition.exactFairBobMeanAcceptedBornMass_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))
(seed : ExactRemainingSeed D)
:
(∑ history : ExactRevealHistory X Y D seed,
∑ aliceAnswer : ↥D → A,
∑ bobAnswer : ↥D → B,
if exactHistoryAccepted G n D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } then
exactRevealMass G n D seed history * ∑ x : X,
G.marginalX x * ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D seed history aliceAnswer x))
(exactBobMeanFilter G n S D seed history bobAnswer x)
else 0) = repeatedPostselectionMass G n S D
theorem
QuantumParallelRepetition.fullHistoryAnswerCount_pos_of_postselection
{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 L : Finset (Fin n))
(hL : L ⊆ Finset.univ \ D)
(hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))
:
theorem
QuantumParallelRepetition.arbitrarily_large_purified_divisor_greedy_conditioning_with_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)
(hwitness : HasSubexponentialWitness (repeatedEntangledValue G))
{η K δ : ℝ}
(hη : 0 < η)
(hη_one : η ≤ 1)
(hK : 0 ≤ K)
(hδ : 0 < δ)
:
∃ (q : ℕ),
2 ≤ q ∧ ∀ (N₀ : ℕ),
∃ (n : ℕ),
N₀ < n ∧ ∃ (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
Real.exp (-(η / (4 * ↑q)) * ↑n) < (purifiedStrategy S).winProbability ∧ D.card < n / q ∧ (purifiedStrategy S).winProbability ≤ (strategyEventLaw (G.repeat n) (purifiedStrategy S)).eventMass
(FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) ∧ ∑ i ∈ Finset.univ \ D,
(strategyEventLaw (G.repeat n) (purifiedStrategy S)).failureMass (repeatedCoordinateWin G n) D
i < ↑(Finset.univ \ D).card * (η * (strategyEventLaw (G.repeat n) (purifiedStrategy S)).eventMass
(FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) ∧ 8 * K * Real.log
(fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) (purifiedStrategy S)).eventMass
(FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) / ↑(Finset.univ \ D).card ≤ δ ^ 2
theorem
QuantumParallelRepetition.answerLogCost_nonneg_of_postselection
{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)
:
theorem
QuantumParallelRepetition.exactSourceClassicalInformationRate_le_three_martingaleRate
{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)
:
theorem
QuantumParallelRepetition.exactSourcePinskerRate_le_half_of_martingaleRate
{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)
{rateTolerance : ℝ}
(rate_nonnegative : 0 ≤ rateTolerance)
(rate_bound : martingaleRate G n S D ≤ rateTolerance ^ 2 / 8)
:
theorem
QuantumParallelRepetition.exact_arbitrarily_large_conditioning_of_subexponentialWitness
{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)
(witness : HasSubexponentialWitness (repeatedEntangledValue G))
{failureTolerance rateTolerance : ℝ}
(failure_positive : 0 < failureTolerance)
(failure_at_most_one : failureTolerance ≤ 1)
(rate_positive : 0 < rateTolerance)
(lower : ℕ)
:
∃ (n : ℕ),
lower < n ∧ ∃ (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
0 < S.winProbability ∧ 0 < repeatedPostselectionMass G n S D ∧ 0 < (Finset.univ \ D).card ∧ uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < failureTolerance ∧ martingaleRate G n S D ≤ rateTolerance ^ 2 / 8 ∧ exactSourcePinskerRate G n S D ≤ rateTolerance / 2
theorem
QuantumParallelRepetition.exactReverseBobSeedInverseCard_le
{M : Type u_5}
[Fintype M]
[DecidableEq M]
:
∑ seed : ExactForwardSeed M, exactSeedWeight seed / ↑(exactReverseRightSide seed).card ≤ 2 / ↑(Fintype.card M)
theorem
QuantumParallelRepetition.exactReverseAliceSeedInverseCard_le
{M : Type u_5}
[Fintype M]
[DecidableEq M]
:
∑ seed : ExactForwardSeed M, exactSeedWeight seed / ↑(exactReverseLeftSide seed).card ≤ 2 / ↑(Fintype.card M)
theorem
QuantumParallelRepetition.exactFairSourceScalarCost_nonneg
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
:
0 ≤ repeatedPostselectionMass G n S D * Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D)
theorem
QuantumParallelRepetition.exactFairAcceptedAliceEntropy_le_sourceRate
{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)
:
exactFairAcceptedAliceEntropy G n S D ≤ 2 * (repeatedPostselectionMass G n S D * martingaleRate G n S D)
theorem
QuantumParallelRepetition.exactFairAcceptedBobEntropy_le_sourceRate
{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)
:
exactFairAcceptedBobEntropy G n S D ≤ 2 * (repeatedPostselectionMass G n S D * martingaleRate G n S D)
theorem
QuantumParallelRepetition.exactFairOperatorEntropyBound_of_positive
{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)
:
ExactFairOperatorEntropyBound G n S D (martingaleRate G n S D)
theorem
QuantumParallelRepetition.exactSourceStateDistanceBound_of_positive
{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)
:
ExactSourceStateDistanceBound G n S D (martingaleRate G n S D)
theorem
QuantumParallelRepetition.unconditionalLiterature_weightedAsynchronous_le
{ι : Type u_1}
[Fintype ι]
(weight value asynchronous : ι → ℝ)
(weight_nonnegative : ∀ (i : ι), 0 ≤ weight i)
(weight_normalized : ∑ i : ι, weight i = 1)
(value_nonnegative : ∀ (i : ι), 0 ≤ value i)
(η δ : ℝ)
(source_energy : ∑ i : ι, weight i * value i ^ 2 ≤ 32 * η)
(physical : ∀ (i : ι), asynchronous i ≤ 8 * √2 * value i + δ)
:
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicMultiscaleFirstHitPhysicalFlagMismatchMass
{A : Type u_1}
{C : Type u_2}
[Fintype A]
[Fintype C]
{L : ℕ}
(alice : A → Fin (L + 1))
(bob : C → Fin (L + 1))
(z : EuclideanSpace ℂ (A × C))
:
The total probability mass of DSV density rational public multiscale first hit physical flag mismatch.
Equations
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState_apply
(N : ℕ)
{S d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)
:
(dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (a, b) = ∑ x : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L,
∑ y : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L,
↑(dSVDensityRationalHeterogeneousActualAliceUnitary N width schedule ξ) a x * ↑(dSVDensityRationalHeterogeneousActualBobUnitary N width schedule ζ) b y * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (x, y)
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState_apply_zeroFlag
(N : ℕ)
{S d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)
:
(dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (a, b) = ∑ x : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d,
∑ y : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d,
↑(dSVDensityRationalHeterogeneousActualAliceUnitary N width schedule ξ) a ⟨0, x⟩ * ↑(dSVDensityRationalHeterogeneousActualBobUnitary N width schedule ζ) b ⟨0, y⟩ * (dSVUniformDensityIndependentSharedState (L + 1) N d).ofLp (x, y)
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualSpectralStopping_apply
{β : Type u_1}
[Fintype β]
[DecidableEq β]
{L : ℕ}
(accepted : Fin L → β → Prop)
(U : ↥(Matrix.unitaryGroup β ℂ))
(flag : Fin (L + 1))
(history input : Fin (L + 1) → β)
:
↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted * dSVDensityRationalFirstAcceptActualTensorBasis U)
⟨flag, history⟩ ⟨0, input⟩ = if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then
∏ i : Fin (L + 1), ↑U (history i) (input i)
else 0
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalLocalUnitary_apply
{β : Type u_1}
[Fintype β]
[DecidableEq β]
{L : ℕ}
(accepted : Fin L → β → Prop)
(U : ↥(Matrix.unitaryGroup β ℂ))
(flag : Fin (L + 1))
(output input : Fin (L + 1) → β)
:
↑(dSVDensityRationalHeterogeneousActualPhysicalLocalUnitary accepted U) ⟨flag, output⟩ ⟨0, input⟩ = ∑ history : Fin (L + 1) → β,
(∏ i : Fin (L + 1), star (↑U (history i) (output i))) * if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then
∏ i : Fin (L + 1), ↑U (history i) (input i)
else 0
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalLocalUnitary_sourceProduct
{β : Type u_1}
[Fintype β]
[DecidableEq β]
{L : ℕ}
(accepted : Fin L → β → Prop)
(U : ↥(Matrix.unitaryGroup β ℂ))
(flag : Fin (L + 1))
(output input : Fin (L + 1) → β)
:
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass
(N : ℕ)
{S d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(flagAlice flagBob : Fin (L + 1))
:
The total probability mass of DSV density rational heterogeneous actual physical flag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAsynchronousFlagMass
(N : ℕ)
{S d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
The total probability mass of DSV density rational heterogeneous actual asynchronous flag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAsynchronousFlagMass_nonneg
(N : ℕ)
{S d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
theorem
QuantumParallelRepetition.dSVDensityRationalFirstAcceptActualPredicateMask_eq_spectralMask
{d : ℕ}
(w : ℝ)
(N : ℕ)
(ξ : BipartiteUnitVector d)
(outcome : Bool)
:
(Matrix.diagonal fun (q : DSVUniformDensityThresholdLocalIndex N d) =>
if dSVDensityRationalProjectiveThresholdBin w N q.fst (⋯.eigenvalues q.snd) = outcome then 1 else 0) = dSVDensityRationalFirstAcceptLocalSpectralMask w N ξ outcome
theorem
QuantumParallelRepetition.dSVDensityRationalFirstAcceptActualOptionalOutcome_apply
{d : ℕ}
(w : ℝ)
(N : ℕ)
(ξ ζ : BipartiteUnitVector d)
(a b : Option Bool)
(alice bob : DSVUniformDensityThresholdLocalIndex N d)
:
(dSVDensityRationalCompleteStoppedOptionalOutcome w N ξ ζ a b).ofLp (alice, bob) = ∑ x : DSVUniformDensityThresholdLocalIndex N d,
∑ y : DSVUniformDensityThresholdLocalIndex N d,
dSVDensityRationalCompleteStoppedOptionalLocalEffect w N ξ a alice x * (dSVDensityRationalCompleteStoppedOptionalLocalEffect w N ζ b).transpose bob y * (dSVUniformDensityThresholdSharedState N d).ofLp (x, y)
def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth
{S L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(i : Fin (L + 1))
:
The DSV density rational heterogeneous actual physical flag born copy width construction used in the quantum parallel-repetition argument.
Equations
- QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i = if active : ↑i < L then width (schedule ⟨↑i, active⟩) else 0
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyConditionMask
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ : BipartiteUnitVector d)
(flag i : Fin (L + 1))
:
(Matrix.diagonal fun (q : DSVUniformDensityThresholdLocalIndex N d) =>
if dSVDensityRationalHeterogeneousActualCopyCondition
(dSVDensityRationalHeterogeneousActualCopyAccepted width schedule ξ) flag i q then
1
else 0) = match dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i with
| none => 1
| some outcome =>
dSVDensityRationalFirstAcceptLocalSpectralMask
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ outcome
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornAlice_sourceProduct
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ : BipartiteUnitVector d)
(flag : Fin (L + 1))
(output input : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d)
:
↑(dSVDensityRationalHeterogeneousActualAliceUnitary N width schedule ξ) ⟨flag, output⟩ ⟨0, input⟩ = ∏ i : Fin (L + 1),
dSVDensityRationalCompleteStoppedOptionalLocalEffect
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i) (output i) (input i)
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornBob_sourceProduct
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ζ : BipartiteUnitVector d)
(flag : Fin (L + 1))
(output input : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d)
:
↑(dSVDensityRationalHeterogeneousActualBobUnitary N width schedule ζ) ⟨flag, output⟩ ⟨0, input⟩ = ∏ i : Fin (L + 1),
(dSVDensityRationalCompleteStoppedOptionalLocalEffect
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i)).transpose
(output i) (input i)
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornState_allFlags
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(flagAlice flagBob : Fin (L + 1))
(alice bob : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d)
:
(dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (⟨flagAlice, alice⟩, ⟨flagBob, bob⟩) = ∏ i : Fin (L + 1),
(dSVDensityRationalCompleteStoppedOptionalOutcome
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagAlice i)
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagBob i)).ofLp
(alice i, bob i)
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalAlignedLocalAction_apply
(B N d L m : ℕ)
(U V : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ))
(φ ψ : Fin B)
(a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)
(i j : Fin m)
:
(localUnitaryAction
(dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift B N d L m
(dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary B U))
(dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift B N d L m
(dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary B V))
(dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource B N d L m)).ofLp
((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((φ, a), i), (dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((ψ, b), j)) = ((if φ = ψ then ↑(√↑B)⁻¹ else 0) * ∑ x : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L,
∑ y : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L,
↑U a x * ↑V b y * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (x, y)) * (embezzlementState m).ofLp (i, j)
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousTargetFirstSpectralAlice
(S B N d L m : ℕ)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ : BipartiteUnitVector d)
:
↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)) ℂ)
The DSV density rational heterogeneous target first spectral alice construction used in the quantum parallel-repetition argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousTargetFirstSpectralBob
(S B N d L m : ℕ)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ζ : BipartiteUnitVector d)
:
↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)) ℂ)
The DSV density rational heterogeneous target first spectral bob construction used in the quantum parallel-repetition argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousTargetFirstSpectralPhysicalSource
(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))
The source object for DSV density rational heterogeneous target first spectral physical.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousTargetFirstSpectralPhysicalSource_apply
(S B N d L m : ℕ)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(φ ψ : DSVDensityRationalPublicMultiscalePhase S B)
(a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)
(i j : Fin m)
:
(dSVDensityRationalHeterogeneousTargetFirstSpectralPhysicalSource S B N d L m width schedule ξ ζ).ofLp
((dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m)
(((Fintype.equivFin (DSVDensityRationalPublicMultiscalePhase S B)) φ, a), i), (dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv S B N d L m)
(((Fintype.equivFin (DSVDensityRationalPublicMultiscalePhase S B)) ψ, b), j)) = (if φ = ψ then ↑(√↑(B ^ S))⁻¹ else 0) * (dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ).ofLp (a, b) * (embezzlementState m).ofLp (i, j)
def
QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseSigmaProductEquiv
{H : Type u_1}
(B m : ℕ)
:
The finite equivalence encoding DSV density rational public bucket coherent phase sigma product.
Equations
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicMultiscaleBucketCoherentSigmaState
{H : Type u_1}
{m : ℕ}
(S B : ℕ)
(history : EuclideanSpace ℂ (H × H))
(work : DSVDensityRationalPublicMultiscalePhaseIndex S B → H → H → EuclideanSpace ℂ (Fin m × Fin m))
:
EuclideanSpace ℂ
(((_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × H) × Fin m) × (_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × H) × Fin m)
The quantum state representing DSV density rational public multiscale bucket coherent sigma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousPureStoppedSigmaState
{S B N d L m : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(work :
DSVDensityRationalPublicMultiscalePhaseIndex S B →
DSVUniformDensityThresholdWholeHistoryLocalIndex N d L →
DSVUniformDensityThresholdWholeHistoryLocalIndex N d L → EuclideanSpace ℂ (Fin m × Fin m))
:
EuclideanSpace ℂ
(((_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ×
Fin m) × (_ : DSVDensityRationalPublicMultiscalePhaseIndex S B × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ×
Fin m)
The quantum state representing DSV density rational heterogeneous pure stopped sigma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor
{N : ℕ}
(n : ℕ)
(z : EuclideanSpace ℂ (Fin N × Fin N))
:
The DSV density rational mixed canonical prefix pure harmonic tensor construction used in the quantum parallel-repetition argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor_sub
{N : ℕ}
(n : ℕ)
(x y : EuclideanSpace ℂ (Fin N × Fin N))
:
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor_prefix_sub_norm_sq
{N n : ℕ}
(positive : 0 < n)
(r s : Fin (N + 1))
:
noncomputable def
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState
{d N : ℕ}
(w : ℝ)
(n : ℕ)
(ξ ζ : BipartiteUnitVector d)
:
The quantum state representing DSV density rational mixed canonical prefix physical accepted sigma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalSigmaWeighted_norm_sq
{H : Type u_1}
[Fintype H]
{n : ℕ}
(history : EuclideanSpace ℂ (H × H))
(work : H → H → EuclideanSpace ℂ (Fin n × Fin n))
:
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState_norm_sq
{d N n : ℕ}
{w : ℝ}
(width : 0 < w)
(grid : 0 < N)
(residual : 0 < n)
(ξ ζ : BipartiteUnitVector d)
: