theorem
QuantumParallelRepetition.exactGlobalHistoryFinPsi_sub_Phi_norm
{X : Type u_1}
{Y : Type u_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)
:
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_zero_of_coordinate_mismatch
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(different : i ≠ r.seed.coordinate)
:
theorem
QuantumParallelRepetition.exactFairPosteriorExpectation_reindex
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(f : ExactLocallySampleableTuple X Y A B D → ℝ)
:
∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t * f t = ∑ r : ExactHistoryFlag X Y A B D,
∑ y : Y, ∑ x : X, exactLocallySampleableLaw G n S D (r.seed.coordinate, x, y, r) * f (r.seed.coordinate, x, y, r)
noncomputable def
QuantumParallelRepetition.exactFairAcceptedAliceEntropy
{X : Type u_1}
{Y : Type u_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))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAcceptedBobEntropy
{X : Type u_1}
{Y : Type u_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))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAcceptedAliceVariation
{X : Type u_1}
{Y : Type u_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))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAcceptedBobVariation
{X : Type u_1}
{Y : Type u_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))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairPsiPhiDistance_mul_postselection_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
:
(∑ t : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D t * ‖exactSourceTuplePsi G n S D t - exactSourceTuplePhi G n S D t‖ ^ 2) * repeatedPostselectionMass G n S D ≤ 4 * exactFairAcceptedAliceVariation G n S D
theorem
QuantumParallelRepetition.exactFairGammaPsiDistance_mul_postselection_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
:
(∑ t : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D t * ‖exactSourceTupleGamma G n S D t - exactSourceTuplePsi G n S D t‖ ^ 2) * repeatedPostselectionMass G n S D ≤ 4 * exactFairAcceptedBobVariation G n S D
def
QuantumParallelRepetition.ExactFairOperatorEntropyBound
{X : Type u_1}
{Y : Type u_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))
(η : ℝ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactSourceStateDistanceBound_of_fair_operator_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))
(η : ℝ)
(positive : 0 < repeatedPostselectionMass G n S D)
(entropy : ExactFairOperatorEntropyBound G n S D η)
:
ExactSourceStateDistanceBound G n S D η
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)
:
noncomputable def
QuantumParallelRepetition.exactJointPrefixQuestionMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixedX fixedY : Finset (Fin n))
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointPrefixAliceOperatorMass
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointPrefixBobOperatorMass
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactJointPrefixQuestionMass_eq_sum_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 : ℕ)
(fixedX fixedY : Finset (Fin n))
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY = ∑ ys : Fin n → Y, if ∀ j ∈ fixedY, ys j = knownY j then exactFixedAliceQuestionMass G n fixedX knownX ys else 0
theorem
QuantumParallelRepetition.exactJointPrefixQuestionMass_eq_sum_bob
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixedX fixedY : Finset (Fin n))
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY = ∑ xs : Fin n → X, if ∀ j ∈ fixedX, xs j = knownX j then exactFixedBobQuestionMass G n fixedY xs knownY else 0
theorem
QuantumParallelRepetition.exactJointPrefixQuestionMass_insert_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 : ℕ)
(fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedX)
(opposite_fixed : j ∈ fixedY)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(x : X)
:
exactJointPrefixQuestionMass G n (insert j fixedX) fixedY (Function.update knownX j x) knownY = G.conditionalXGivenY (knownY j) x * exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixQuestionMass_insert_bob
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixedX fixedY : Finset (Fin n))
(j : Fin n)
(opposite_fixed : j ∈ fixedX)
(fresh : j ∉ fixedY)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(y : Y)
:
exactJointPrefixQuestionMass G n fixedX (insert j fixedY) knownX (Function.update knownY j y) = G.conditionalYGivenX (knownX j) y * exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixQuestionAtom_zero_of_mass_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 : ℕ)
(fixedX fixedY : Finset (Fin n))
(knownX : Fin n → X)
(knownY : Fin n → Y)
(zero : exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY = 0)
(xs : Fin n → X)
(ys : Fin n → Y)
:
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorMass_zero_of_mass_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(zero : exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY = 0)
:
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorMass_zero_of_mass_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(zero : exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY = 0)
:
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorMass_sum_insert
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedX)
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
∑ x : X, exactJointPrefixAliceOperatorMass G n S D (insert j fixedX) fixedY answer (Function.update knownX j x) knownY = exactJointPrefixAliceOperatorMass G n S D fixedX fixedY answer knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorMass_sum_insert
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedY)
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
∑ y : Y, exactJointPrefixBobOperatorMass G n S D fixedX (insert j fixedY) answer knownX (Function.update knownY j y) = exactJointPrefixBobOperatorMass G n S D fixedX fixedY answer knownX knownY
noncomputable def
QuantumParallelRepetition.exactJointPrefixAliceOperatorFilter
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointPrefixBobOperatorFilter
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorFilter_martingale
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedX)
(opposite_fixed : j ∈ fixedY)
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(supported : exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY ≠ 0)
:
∑ x : X,
G.conditionalXGivenY (knownY j) x • exactJointPrefixAliceOperatorFilter G n S D (insert j fixedX) fixedY answer (Function.update knownX j x) knownY = exactJointPrefixAliceOperatorFilter G n S D fixedX fixedY answer knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorFilter_martingale
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(j : Fin n)
(opposite_fixed : j ∈ fixedX)
(fresh : j ∉ fixedY)
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(supported : exactJointPrefixQuestionMass G n fixedX fixedY knownX knownY ≠ 0)
:
∑ y : Y,
G.conditionalYGivenX (knownX j) y • exactJointPrefixBobOperatorFilter G n S D fixedX (insert j fixedY) answer knownX (Function.update knownY j y) = exactJointPrefixBobOperatorFilter G n S D fixedX fixedY answer knownX knownY
noncomputable def
QuantumParallelRepetition.exactFairAliceQuestionMask
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobQuestionMask
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactRevealCode_eq_iff_fair_question_masks
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(q q' : ExactFullQuestion X Y n)
:
exactRevealCode D seed q' = exactRevealCode D seed q ↔ (∀ j ∈ exactFairAliceQuestionMask D seed, q'.1 j = q.1 j) ∧ ∀ j ∈ exactFairBobQuestionMask D seed, q'.2 j = q.2 j
theorem
QuantumParallelRepetition.exactAliceQuestionMass_eq_jointPrefixQuestionMass
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
:
exactAliceQuestionMass G n D seed (exactRevealCode D seed q) (q.1 ↑seed.coordinate) = exactJointPrefixQuestionMass G n (insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed))
(exactFairBobQuestionMask D seed) q.1 q.2
theorem
QuantumParallelRepetition.exactBobQuestionMass_eq_jointPrefixQuestionMass
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
:
exactBobQuestionMass G n D seed (exactRevealCode D seed q) (q.2 ↑seed.coordinate) = exactJointPrefixQuestionMass G n (exactFairAliceQuestionMask D seed)
(insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)) q.1 q.2
theorem
QuantumParallelRepetition.exactAliceQuestionFilter_eq_jointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → A)
:
exactAliceQuestionFilter G n S D seed (exactRevealCode D seed q) answer (q.1 ↑seed.coordinate) = exactJointPrefixAliceOperatorFilter G n S D (insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed))
(exactFairBobQuestionMask D seed) answer q.1 q.2
theorem
QuantumParallelRepetition.exactBobQuestionFilter_eq_jointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → B)
:
exactBobQuestionFilter G n S D seed (exactRevealCode D seed q) answer (q.2 ↑seed.coordinate) = exactJointPrefixBobOperatorFilter G n S D (exactFairAliceQuestionMask D seed)
(insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)) answer q.1 q.2
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorMass_eq_sum_bobMass
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
exactJointPrefixAliceOperatorMass G n S D fixedX fixedY answer knownX knownY = ∑ xs : Fin n → X,
if ∀ j ∈ fixedX, xs j = knownX j then
exactFixedBobQuestionMass G n fixedY xs knownY • conditionedAliceEffect G n S D answer xs
else 0
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorMass_eq_sum_aliceMass
{X : Type u_1}
{Y : Type u_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 fixedX fixedY : Finset (Fin n))
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
:
exactJointPrefixBobOperatorMass G n S D fixedX fixedY answer knownX knownY = ∑ ys : Fin n → Y,
if ∀ j ∈ fixedY, ys j = knownY j then
exactFixedAliceQuestionMass G n fixedX knownX ys • conditionedBobEffect G n S D answer ys
else 0
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorMass_insert_bob
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D fixedX fixedY : Finset (Fin n))
(j : Fin n)
(opposite_fixed : j ∈ fixedX)
(fresh : j ∉ fixedY)
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(y : Y)
:
exactJointPrefixAliceOperatorMass G n S D fixedX (insert j fixedY) answer knownX (Function.update knownY j y) = G.conditionalYGivenX (knownX j) y • exactJointPrefixAliceOperatorMass G n S D fixedX fixedY answer knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorMass_insert_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 : ℕ)
(S : Strategy (G.repeat n))
(D fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedX)
(opposite_fixed : j ∈ fixedY)
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(x : X)
:
exactJointPrefixBobOperatorMass G n S D (insert j fixedX) fixedY answer (Function.update knownX j x) knownY = G.conditionalXGivenY (knownY j) x • exactJointPrefixBobOperatorMass G n S D fixedX fixedY answer knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixAliceOperatorFilter_insert_bob
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D fixedX fixedY : Finset (Fin n))
(j : Fin n)
(opposite_fixed : j ∈ fixedX)
(fresh : j ∉ fixedY)
(answer : ↥D → A)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(y : Y)
(edge : G.conditionalYGivenX (knownX j) y ≠ 0)
:
exactJointPrefixAliceOperatorFilter G n S D fixedX (insert j fixedY) answer knownX (Function.update knownY j y) = exactJointPrefixAliceOperatorFilter G n S D fixedX fixedY answer knownX knownY
theorem
QuantumParallelRepetition.exactJointPrefixBobOperatorFilter_insert_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 : ℕ)
(S : Strategy (G.repeat n))
(D fixedX fixedY : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixedX)
(opposite_fixed : j ∈ fixedY)
(answer : ↥D → B)
(knownX : Fin n → X)
(knownY : Fin n → Y)
(x : X)
(edge : G.conditionalXGivenY (knownY j) x ≠ 0)
:
exactJointPrefixBobOperatorFilter G n S D (insert j fixedX) fixedY answer (Function.update knownX j x) knownY = exactJointPrefixBobOperatorFilter G n S D fixedX fixedY answer knownX knownY
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
noncomputable def
QuantumParallelRepetition.exactReverseAliceHighQuestionPotential
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseAliceLowQuestionPotential
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobHighQuestionPotential
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobLowQuestionPotential
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceHighOperatorPotential_eq_question
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseAliceFilterHighOperatorPotential G n S D side context marker = exactReverseAliceHighQuestionPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseAliceLowOperatorPotential_eq_question
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseAliceFilterLowOperatorPotential G n S D side context marker = exactReverseAliceLowQuestionPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseBobHighOperatorPotential_eq_question
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseBobFilterHighOperatorPotential G n S D side context marker = exactReverseBobHighQuestionPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseBobLowOperatorPotential_eq_question
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseBobFilterLowOperatorPotential G n S D side context marker = exactReverseBobLowQuestionPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseAliceFilterOperatorMarkerEntropy_eq_question_sub
{X : Type u_1}
{Y : Type u_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)
:
exactReverseAliceFilterOperatorMarkerEntropy G n S D side context marker = exactReverseAliceHighQuestionPotential G n S D side context marker - exactReverseAliceLowQuestionPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseBobFilterOperatorMarkerEntropy_eq_question_sub
{X : Type u_1}
{Y : Type u_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)
:
exactReverseBobFilterOperatorMarkerEntropy G n S D side context marker = exactReverseBobHighQuestionPotential G n S D side context marker - exactReverseBobLowQuestionPotential G n S D side context marker
def
QuantumParallelRepetition.exactReverseContextQuestionPrefix
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(k : ℕ)
:
Equations
- QuantumParallelRepetition.exactReverseContextQuestionPrefix D side context k = Finset.image (fun (j : ↥side) => ↑↑j) {j : ↥side | ↑(context.sideRank j) < k}
Instances For
def
QuantumParallelRepetition.exactReverseAlicePrefixXMask
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(k : ℕ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactReverseAliceFixedYMask
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactReverseBobFixedXMask
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactReverseBobPrefixYMask
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(k : ℕ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseContextQuestionPrefix_eq_image
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseContextQuestionPrefix D side context ↑marker = Finset.image Subtype.val (exactReverseContextPrefixBefore context marker)
theorem
QuantumParallelRepetition.exactReverseAlicePrefixXMask_eq_fair
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
exactReverseAlicePrefixXMask D (exactReverseRightSide seed) (exactReverseBobContext seed)
↑((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = exactFairAliceQuestionMask D seed
theorem
QuantumParallelRepetition.exactReverseAliceFixedYMask_eq_insert_fair
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
exactReverseAliceFixedYMask D (exactReverseRightSide seed) (exactReverseBobContext seed) = insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)
theorem
QuantumParallelRepetition.exactReverseBobFixedXMask_eq_insert_fair
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
exactReverseBobFixedXMask D (exactReverseLeftSide seed) (exactReverseAliceContext seed) = insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed)
theorem
QuantumParallelRepetition.exactReverseBobPrefixYMask_eq_fair
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
exactReverseBobPrefixYMask D (exactReverseLeftSide seed) (exactReverseAliceContext seed)
↑((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = exactFairBobQuestionMask D seed
theorem
QuantumParallelRepetition.exactReverseContextQuestionPrefix_succ
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseContextQuestionPrefix D side context (↑marker + 1) = insert (↑↑(context.sideRank.symm marker)) (exactReverseContextQuestionPrefix D side context ↑marker)
theorem
QuantumParallelRepetition.exactFairAliceQuestionMask_coordinate_not_mem
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
↑seed.coordinate ∉ exactFairAliceQuestionMask D seed
theorem
QuantumParallelRepetition.exactFairBobQuestionMask_coordinate_not_mem
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
↑seed.coordinate ∉ exactFairBobQuestionMask D seed
noncomputable def
QuantumParallelRepetition.exactReverseAliceAlignedCfcPrefixPotential
{X : Type u_1}
{Y : Type u_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)
(k : ℕ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobAlignedCfcPrefixPotential
{X : Type u_1}
{Y : Type u_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)
(k : ℕ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceAlignedCfcPrefixPotential_telescope
{X : Type u_1}
{Y : Type u_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)
:
∑ k ∈ Finset.range side.card,
(exactReverseAliceAlignedCfcPrefixPotential G n S D side context (k + 1) - exactReverseAliceAlignedCfcPrefixPotential G n S D side context k) = exactReverseAliceAlignedCfcPrefixPotential G n S D side context side.card - exactReverseAliceAlignedCfcPrefixPotential G n S D side context 0
theorem
QuantumParallelRepetition.exactReverseBobAlignedCfcPrefixPotential_telescope
{X : Type u_1}
{Y : Type u_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)
:
∑ k ∈ Finset.range side.card,
(exactReverseBobAlignedCfcPrefixPotential G n S D side context (k + 1) - exactReverseBobAlignedCfcPrefixPotential G n S D side context k) = exactReverseBobAlignedCfcPrefixPotential G n S D side context side.card - exactReverseBobAlignedCfcPrefixPotential G n S D side context 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.exactJointPrefixQuestionMass_pos_of_question
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixedX fixedY : Finset (Fin n))
(knownX : Fin n → X)
(knownY : Fin n → Y)
(positive : 0 < (G.repeat n).questionWeight knownX knownY)
:
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.exactFairAliceMeanFilter_eq_jointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → A)
(supported : exactPriorQuestionWeight G n q ≠ 0)
:
exactAliceMeanFilter G n S D seed (exactRevealCode D seed q) answer (q.2 ↑seed.coordinate) = exactJointPrefixAliceOperatorFilter G n S D (exactFairAliceQuestionMask D seed)
(insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)) answer q.1 q.2
theorem
QuantumParallelRepetition.exactFairBobMeanFilter_eq_jointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → B)
(supported : exactPriorQuestionWeight G n q ≠ 0)
:
exactBobMeanFilter G n S D seed (exactRevealCode D seed q) answer (q.1 ↑seed.coordinate) = exactJointPrefixBobOperatorFilter G n S D (insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed))
(exactFairBobQuestionMask D seed) answer q.1 q.2
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.exactReverseAlicePrefixXMask_succ
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseAlicePrefixXMask D side context (↑marker + 1) = insert (↑↑(context.sideRank.symm marker)) (exactReverseAlicePrefixXMask D side context ↑marker)
theorem
QuantumParallelRepetition.exactReverseBobPrefixYMask_succ
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseBobPrefixYMask D side context (↑marker + 1) = insert (↑↑(context.sideRank.symm marker)) (exactReverseBobPrefixYMask D side context ↑marker)
theorem
QuantumParallelRepetition.exactReverseAliceLowQuestionPotential_eq_alignedPrefix
{X : Type u_1}
{Y : Type u_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)
:
exactReverseAliceLowQuestionPotential G n S D side context marker = exactReverseAliceAlignedCfcPrefixPotential G n S D side context ↑marker
theorem
QuantumParallelRepetition.exactReverseBobLowQuestionPotential_eq_alignedPrefix
{X : Type u_1}
{Y : Type u_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)
:
exactReverseBobLowQuestionPotential G n S D side context marker = exactReverseBobAlignedCfcPrefixPotential G n S D side context ↑marker
theorem
QuantumParallelRepetition.exactAliceQuestionFilter_eq_fullJointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → A)
(supported : exactPriorQuestionWeight G n q ≠ 0)
:
exactAliceQuestionFilter G n S D seed (exactRevealCode D seed q) answer (q.1 ↑seed.coordinate) = exactJointPrefixAliceOperatorFilter G n S D (insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed))
(insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)) answer q.1 q.2
theorem
QuantumParallelRepetition.exactBobQuestionFilter_eq_fullJointPrefixOperatorFilter
{X : Type u_1}
{Y : Type u_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)
(q : ExactFullQuestion X Y n)
(answer : ↥D → B)
(supported : exactPriorQuestionWeight G n q ≠ 0)
:
exactBobQuestionFilter G n S D seed (exactRevealCode D seed q) answer (q.2 ↑seed.coordinate) = exactJointPrefixBobOperatorFilter G n S D (insert (↑seed.coordinate) (exactFairAliceQuestionMask D seed))
(insert (↑seed.coordinate) (exactFairBobQuestionMask D seed)) answer q.1 q.2
theorem
QuantumParallelRepetition.exactReverseAliceHighQuestionPotential_eq_alignedPrefix
{X : Type u_1}
{Y : Type u_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)
:
exactReverseAliceHighQuestionPotential G n S D side context marker = exactReverseAliceAlignedCfcPrefixPotential G n S D side context (↑marker + 1)
theorem
QuantumParallelRepetition.exactReverseBobHighQuestionPotential_eq_alignedPrefix
{X : Type u_1}
{Y : Type u_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)
:
exactReverseBobHighQuestionPotential G n S D side context marker = exactReverseBobAlignedCfcPrefixPotential G n S D side context (↑marker + 1)
theorem
QuantumParallelRepetition.exactReverseAliceFilterOperatorMarkerEntropy_eq_aligned_step
{X : Type u_1}
{Y : Type u_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)
:
exactReverseAliceFilterOperatorMarkerEntropy G n S D side context marker = exactReverseAliceAlignedCfcPrefixPotential G n S D side context (↑marker + 1) - exactReverseAliceAlignedCfcPrefixPotential G n S D side context ↑marker
theorem
QuantumParallelRepetition.exactReverseBobFilterOperatorMarkerEntropy_eq_aligned_step
{X : Type u_1}
{Y : Type u_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)
:
exactReverseBobFilterOperatorMarkerEntropy G n S D side context marker = exactReverseBobAlignedCfcPrefixPotential G n S D side context (↑marker + 1) - exactReverseBobAlignedCfcPrefixPotential G n S D side context ↑marker
theorem
QuantumParallelRepetition.exactReverseAliceFilterOperatorMarkerEntropy_sum_telescope
{X : Type u_1}
{Y : Type u_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, exactReverseAliceFilterOperatorMarkerEntropy G n S D side context marker = exactReverseAliceAlignedCfcPrefixPotential G n S D side context side.card - exactReverseAliceAlignedCfcPrefixPotential G n S D side context 0
theorem
QuantumParallelRepetition.exactReverseBobFilterOperatorMarkerEntropy_sum_telescope
{X : Type u_1}
{Y : Type u_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, exactReverseBobFilterOperatorMarkerEntropy G n S D side context marker = exactReverseBobAlignedCfcPrefixPotential G n S D side context side.card - exactReverseBobAlignedCfcPrefixPotential G n S D side context 0
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactFixedSeedOutcomeTuple
(X : Type u_5)
(Y : Type u_6)
(A : Type u_7)
(B : Type u_8)
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
Type (max (max u_6 u_5) (max (max u_6 u_5) u_8) u_7)
Equations
- QuantumParallelRepetition.ExactFixedSeedOutcomeTuple X Y A B D seed = (QuantumParallelRepetition.ExactRevealHistory X Y D seed × (↥D → A) × (↥D → B) × X × Y)
Instances For
def
QuantumParallelRepetition.exactFixedSeedOutcomeCode
{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))
(seed : ExactRemainingSeed D)
(outcome : ExactOutcome X Y A B n)
:
ExactFixedSeedOutcomeTuple X Y A B D seed
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFixedSeedOutcomeCode_fiber_iff
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(aliceAnswer : ↥D → A)
(bobAnswer : ↥D → B)
(x : X)
(y : Y)
(outcome : ExactOutcome X Y A B n)
:
theorem
QuantumParallelRepetition.exactFixedSeedGroupedBornMass_eq
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(aliceAnswer : ↥D → A)
(bobAnswer : ↥D → B)
(x : X)
(y : Y)
:
ClassicalInformation.groupedMass (exactFixedSeedOutcomeCode D seed) (strategyEventLaw (G.repeat n) S).weight
(history, aliceAnswer, bobAnswer, x, y) = exactFairFullOutcomeBornMass G n S D
{ seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer } x y
theorem
QuantumParallelRepetition.exactFixedSeedOutcomeCode_accepted_iff
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(outcome : ExactOutcome X Y A B n)
:
exactHistoryAccepted G n D
{ seed := seed, history := (exactFixedSeedOutcomeCode D seed outcome).1,
aliceAnswer := (exactFixedSeedOutcomeCode D seed outcome).2.1,
bobAnswer := (exactFixedSeedOutcomeCode D seed outcome).2.2.1 } ↔ outcome ∈ FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D
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
noncomputable def
QuantumParallelRepetition.exactReverseAliceAcceptedScalarEntropy
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceLowOperatorPotential_neg_le_scalarEntropy
{X : Type u_1}
{Y : Type u_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)
:
-exactReverseAliceFilterLowOperatorPotential G n S D side context marker ≤ exactReverseAliceAcceptedScalarEntropy G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseAliceAlignedCfcPrefixPotential_last_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)
(nonempty : 0 < side.card)
:
theorem
QuantumParallelRepetition.exactReverseAliceFilterOperatorMarkerEntropy_sum_le_scalarEntropy
{X : Type u_1}
{Y : Type u_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)
(nonempty : 0 < side.card)
:
∑ marker : Fin side.card, exactReverseAliceFilterOperatorMarkerEntropy G n S D side context marker ≤ exactReverseAliceAcceptedScalarEntropy G n S D side context ⟨0, nonempty⟩
noncomputable def
QuantumParallelRepetition.exactReverseBobAcceptedScalarEntropy
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseBobFilterLowOperatorPotential_neg_le_scalarEntropy
{X : Type u_1}
{Y : Type u_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)
:
-exactReverseBobFilterLowOperatorPotential G n S D side context marker ≤ exactReverseBobAcceptedScalarEntropy G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseBobAlignedCfcPrefixPotential_terminal_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)
(sideNonempty : 0 < side.card)
:
theorem
QuantumParallelRepetition.exactReverseBobFilterOperatorMarkerEntropy_sum_le_scalarEntropy
{X : Type u_1}
{Y : Type u_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)
(sideNonempty : 0 < side.card)
:
∑ marker : Fin side.card, exactReverseBobFilterOperatorMarkerEntropy G n S D side context marker ≤ exactReverseBobAcceptedScalarEntropy G n S D side context ⟨0, sideNonempty⟩
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
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactFairAliceScalarAtom
(X : Type u_5)
(Y : Type u_6)
(A : Type u_7)
(B : Type u_8)
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
Type (max (max u_6 u_5) (max u_6 u_8) u_7)
Equations
- QuantumParallelRepetition.ExactFairAliceScalarAtom X Y A B D seed = (QuantumParallelRepetition.ExactRevealHistory X Y D seed × (↥D → A) × (↥D → B) × Y)
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAliceScalarCountingWeight
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairAliceScalarAtom X Y A B D seed)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAliceScalarBornMass
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairAliceScalarAtom X Y A B D seed)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactFairBobScalarAtom
(X : Type u_5)
(Y : Type u_6)
(A : Type u_7)
(B : Type u_8)
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
Type (max (max u_6 u_5) (max u_5 u_8) u_7)
Equations
- QuantumParallelRepetition.ExactFairBobScalarAtom X Y A B D seed = (QuantumParallelRepetition.ExactRevealHistory X Y D seed × (↥D → A) × (↥D → B) × X)
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobScalarCountingWeight
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairBobScalarAtom X Y A B D seed)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobScalarBornMass
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairBobScalarAtom X Y A B D seed)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairAliceScalarCountingWeight_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(atom : ExactFairAliceScalarAtom X Y A B D seed)
:
theorem
QuantumParallelRepetition.exactFairBobScalarCountingWeight_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(atom : ExactFairBobScalarAtom X Y A B D seed)
:
theorem
QuantumParallelRepetition.exactFairAliceScalarBornMass_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))
(seed : ExactRemainingSeed D)
(atom : ExactFairAliceScalarAtom X Y A B D seed)
:
theorem
QuantumParallelRepetition.exactFairBobScalarBornMass_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))
(seed : ExactRemainingSeed D)
(atom : ExactFairBobScalarAtom X Y A B D seed)
:
theorem
QuantumParallelRepetition.exactFairAliceScalarCountingWeight_sum_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
∑ atom : ExactFairAliceScalarAtom X Y A B D seed, exactFairAliceScalarCountingWeight G n D seed atom ≤ fullHistoryAnswerCount D
theorem
QuantumParallelRepetition.exactFairBobScalarCountingWeight_sum_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
:
∑ atom : ExactFairBobScalarAtom X Y A B D seed, exactFairBobScalarCountingWeight G n D seed atom ≤ fullHistoryAnswerCount D
theorem
QuantumParallelRepetition.exactFairAliceScalarBornMass_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)
:
∑ atom : ExactFairAliceScalarAtom X Y A B D seed,
exactFairAliceScalarCountingWeight G n D seed atom * exactFairAliceScalarBornMass G n S D seed atom = repeatedPostselectionMass G n S D
theorem
QuantumParallelRepetition.exactFairBobScalarBornMass_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)
:
∑ atom : ExactFairBobScalarAtom X Y A B D seed,
exactFairBobScalarCountingWeight G n D seed atom * exactFairBobScalarBornMass G n S D seed atom = repeatedPostselectionMass G n S D
theorem
QuantumParallelRepetition.exactFairAliceScalarBornMass_le_one
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairAliceScalarAtom X Y A B D seed)
:
theorem
QuantumParallelRepetition.exactFairBobScalarBornMass_le_one
{X : Type u_1}
{Y : Type u_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)
(atom : ExactFairBobScalarAtom X Y A B D seed)
:
noncomputable def
QuantumParallelRepetition.exactFairAliceSeedScalarEntropy
{X : Type u_1}
{Y : Type u_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.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobSeedScalarEntropy
{X : Type u_1}
{Y : Type u_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.
Instances For
theorem
QuantumParallelRepetition.exactFairAliceSeedScalarEntropy_eq_weighted
{X : Type u_1}
{Y : Type u_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)
:
exactFairAliceSeedScalarEntropy G n S D seed = ∑ atom : ExactFairAliceScalarAtom X Y A B D seed,
exactFairAliceScalarCountingWeight G n D seed atom * (exactFairAliceScalarBornMass G n S D seed atom).negMulLog
theorem
QuantumParallelRepetition.exactFairBobSeedScalarEntropy_eq_weighted
{X : Type u_1}
{Y : Type u_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)
:
exactFairBobSeedScalarEntropy G n S D seed = ∑ atom : ExactFairBobScalarAtom X Y A B D seed,
exactFairBobScalarCountingWeight G n D seed atom * (exactFairBobScalarBornMass G n S D seed atom).negMulLog
theorem
QuantumParallelRepetition.exactFairAliceSeedScalarEntropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(seed : ExactRemainingSeed D)
:
exactFairAliceSeedScalarEntropy G n S D seed ≤ repeatedPostselectionMass G n S D * Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D)
theorem
QuantumParallelRepetition.exactFairBobSeedScalarEntropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(seed : ExactRemainingSeed D)
:
exactFairBobSeedScalarEntropy G n S D seed ≤ repeatedPostselectionMass G n S D * Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D)
theorem
QuantumParallelRepetition.exactReverseAliceAcceptedScalarEntropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseAliceAcceptedScalarEntropy G n S D side context marker ≤ repeatedPostselectionMass G n S D * Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D)
theorem
QuantumParallelRepetition.exactReverseBobAcceptedScalarEntropy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(side : Finset (SourceRemainingCoordinate D))
(context : ExactReverseSideContext (SourceRemainingCoordinate D) side)
(marker : Fin side.card)
:
exactReverseBobAcceptedScalarEntropy G n S D side context marker ≤ repeatedPostselectionMass G n S D * Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D)
def
QuantumParallelRepetition.sourceAnswerAlphabetBound
(A : Type u_5)
(B : Type u_6)
[Fintype A]
[Fintype B]
:
Equations
- QuantumParallelRepetition.sourceAnswerAlphabetBound A B = max 1 (↑(Fintype.card A) * ↑(Fintype.card B))
Instances For
theorem
QuantumParallelRepetition.one_le_sourceAnswerAlphabetBound
(A : Type u_5)
(B : Type u_6)
[Fintype A]
[Fintype B]
:
theorem
QuantumParallelRepetition.sourceAnswerAlphabetBound_log_nonneg
(A : Type u_5)
(B : Type u_6)
[Fintype A]
[Fintype B]
:
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.divisor_greedy_log_cost_per_remaining_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))
{η : ℝ}
(hη : 0 < η)
{q : ℕ}
(hq : 2 ≤ q)
(D : Finset (Fin n))
(hD : D.card < n / q)
(hwitness : Real.exp (-(η / (4 * ↑q)) * ↑n) < S.winProbability)
(hmass :
S.winProbability ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))
:
Real.log
(fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) / ↑(Finset.univ \ D).card ≤ (2 * Real.log (sourceAnswerAlphabetBound A B) + η / 2) / ↑q
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.exactReversePartitionInverseCard_le
{M : Type u_5}
[Fintype M]
[DecidableEq M]
:
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 + δ)
:
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))
:
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)
:
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))
:
Equations
- QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i = if active : ↑i < L then width (schedule ⟨↑i, active⟩) else 0
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyMatrix
{β : Type u_1}
[Fintype β]
[DecidableEq β]
{L : ℕ}
(accepted : Fin L → β → Prop)
(U : ↥(Matrix.unitaryGroup β ℂ))
(flag i : Fin (L + 1))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyMatrix_eq_spectralMask
{β : Type u_1}
[Fintype β]
[DecidableEq β]
{L : ℕ}
(accepted : Fin L → β → Prop)
(U : ↥(Matrix.unitaryGroup β ℂ))
(flag i : Fin (L + 1))
:
dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyMatrix accepted U flag i = (↑U⁻¹ * Matrix.diagonal fun (atom : β) =>
if dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i atom then 1 else 0) * ↑U
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.dSVDensityRationalHeterogeneousActualPhysicalFlagBornAliceCopy_eq_optionalEffect
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ : BipartiteUnitVector d)
(flag i : Fin (L + 1))
:
dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyMatrix
(dSVDensityRationalHeterogeneousActualCopyAccepted width schedule ξ) (dSVUniformDensityAliceHistorySpectralCopy ξ)
flag i = dSVDensityRationalCompleteStoppedOptionalLocalEffect
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i)
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBornBobCopy_eq_optionalEffect
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ζ : BipartiteUnitVector d)
(flag i : Fin (L + 1))
:
dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyMatrix
(dSVDensityRationalHeterogeneousActualCopyAccepted width schedule ζ) (dSVUniformDensityBobHistoryCopyBasis ζ)⁻¹ flag
i = (dSVDensityRationalCompleteStoppedOptionalLocalEffect
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flag i)).transpose
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)) ℂ)
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)) ℂ)
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))
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 : ℕ)
:
Equations
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicMultiscaleBucketCoherentSigmaState
{H : Type u_1}
[Fintype H]
{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)
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)
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)
:
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)
:
noncomputable def
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome
{S N d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(i : Fin (L + 1))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_before
{S N d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(i : Fin (L + 1))
(before : ↑i < ↑j)
:
dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j i = dSVDensityRationalCompleteProjectiveOutcome (width (schedule ⟨↑i, ⋯⟩)) N ξ ζ false false
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_hit
{S N d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
:
dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j j.castSucc = dSVDensityRationalCompleteProjectiveOutcome (width (schedule j)) N ξ ζ true true
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome_after
{S N d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(i : Fin (L + 1))
(after : ↑j < ↑i)
:
dSVDensityRationalHeterogeneousActualCommonStopScheduledOutcome width schedule ξ ζ j i = dSVUniformDensityThresholdSharedState N d
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCommonStopPhysicalState_eq_outcomeProduct
{S N d L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(alice bob : DSVUniformDensityIndependentHistoryLocalIndex (L + 1) N d)
:
theorem
QuantumParallelRepetition.dSVDensityRationalPureFlagBorn_partition
{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))
:
dSVDensityRationalPublicMultiscaleFirstHitPhysicalFlagMismatchMass alice bob z + ∑ flag : Fin (L + 1), dSVDensityRationalPureBaseExactFlagBornMass alice bob z flag flag = ‖z‖ ^ 2
theorem
QuantumParallelRepetition.dSVDensityRationalPureMatchedFlagBorn_zero_succ
{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))
:
∑ flag : Fin (L + 1), dSVDensityRationalPureBaseExactFlagBornMass alice bob z flag flag = dSVDensityRationalPureBaseExactFlagBornMass alice bob z 0 0 + ∑ j : Fin L, dSVDensityRationalPureBaseExactFlagBornMass alice bob z j.succ j.succ
theorem
QuantumParallelRepetition.dSVDensityRationalPureFlagBorn_partition_zero_succ
{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))
:
dSVDensityRationalPublicMultiscaleFirstHitPhysicalFlagMismatchMass alice bob z + dSVDensityRationalPureBaseExactFlagBornMass alice bob z 0 0 + ∑ j : Fin L, dSVDensityRationalPureBaseExactFlagBornMass alice bob z j.succ j.succ = ‖z‖ ^ 2
theorem
QuantumParallelRepetition.dSVDensityRationalPureFlagBorn_normalized_partition_zero_succ
{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))
(normalized : ‖z‖ = 1)
:
dSVDensityRationalPublicMultiscaleFirstHitPhysicalFlagMismatchMass alice bob z + dSVDensityRationalPureBaseExactFlagBornMass alice bob z 0 0 + ∑ j : Fin L, dSVDensityRationalPureBaseExactFlagBornMass alice bob z j.succ j.succ = 1
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_eq_optionalProduct
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(flagAlice flagBob : Fin (L + 1))
:
dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ flagAlice flagBob = ∏ i : Fin (L + 1),
‖dSVDensityRationalCompleteStoppedOptionalOutcome
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagAlice i)
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L flagBob i)‖ ^ 2
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalMatchedCopyBorn
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(i : Fin (L + 1))
:
‖dSVDensityRationalCompleteStoppedOptionalOutcome
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L j.succ i)
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L j.succ i)‖ ^ 2 = if ↑i < ↑j then dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑i
else if ↑i = ↑j then dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j else 1
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_succ_succ_eq_stage
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
:
dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalNoHitCopyBorn
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(i : Fin (L + 1))
:
‖dSVDensityRationalCompleteStoppedOptionalOutcome
(dSVDensityRationalHeterogeneousActualPhysicalFlagBornCopyWidth width schedule i) N ξ ζ
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L 0 i)
(dSVDensityRationalCompleteStoppedOptionalLocalSchedule L 0 i)‖ ^ 2 = if ↑i < L then dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑i else 1
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagMass_zero_zero_eq_terminal
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ 0 0 = dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalBaseFlagBorn_eq_flagMass
{S d N L : ℕ}
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(flagAlice flagBob : Fin (L + 1))
:
dSVDensityRationalPureBaseExactFlagBornMass (fun (q : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) => q.fst)
(fun (q : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) => q.fst)
(dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ) flagAlice flagBob = dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ flagAlice flagBob
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalMatchedFlagMass_eq_stoppedSuccess
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
∑ j : Fin L, dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalFlagBorn_mass_partition
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ 0 0 + ∑ j : Fin L, dSVDensityRationalHeterogeneousActualPhysicalFlagMass N width schedule ξ ζ j.succ j.succ = 1
theorem
QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAsynchronousFlagMass_eq_stoppedAsynchronousMass
{S d N L : ℕ}
(grid : 0 < N)
(dimension : 0 < d)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
:
dSVDensityRationalHeterogeneousActualAsynchronousFlagMass N width schedule ξ ζ = dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalLocalAction_real_smul
{n : ℕ}
(A B : ↥(Matrix.unitaryGroup (Fin n) ℂ))
(r : ℝ)
(z : EuclideanSpace ℂ (Fin n × Fin n))
:
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor_real_smul
{N : ℕ}
(n : ℕ)
(r : ℝ)
(z : EuclideanSpace ℂ (Fin N × Fin N))
:
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalAcceptedSigmaState_apply
{d N n : ℕ}
{w : ℝ}
(width : 0 < w)
(grid : 0 < N)
(ξ ζ : BipartiteUnitVector d)
(i j : Fin d)
(k l : Fin N)
(a b : Fin n)
:
theorem
QuantumParallelRepetition.dSVDensityRationalMixedCanonicalPrefixPhysicalRankWeightedAtomError_eq
{N n : ℕ}
(grid : 0 < N)
(rank : Fin (N + 1))
(A B : ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ))
:
‖localUnitaryAction A B (dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (dSVCanonicalFailurePrefix rank)) - √↑↑rank • embezzlementState (N * n)‖ ^ 2 = ↑↑rank * ‖localUnitaryAction A B (tensorEmbezzlementTarget (dSVCanonicalFailureUnitRankFamily N grid rank)) - embezzlementState (N * n)‖ ^ 2
theorem
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCommonRank_eq
{d N : ℕ}
(w : ℝ)
(ξ ζ : BipartiteUnitVector d)
(i j : Fin d)
:
theorem
QuantumParallelRepetition.exists_proofDSVDensityRationalPublicBucketPhysicalRawRankCleanup_sq
{Ω : Type u_1}
{I : Type u_2}
[DecidableEq I]
{N : ℕ}
(grid : 0 < N)
(bucket : Ω → Fin (N + 1) → I)
(representative : Ω → I → Fin (N + 1))
(ε : ℝ)
(precision : 0 < ε)
:
∃ (n : ℕ),
0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)),
∀ (phase : Ω) (r s : Fin (N + 1)),
‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s))
(dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n (dSVCanonicalFailurePrefix r)) - √↑↑r • embezzlementState (N * n)‖ ^ 2 ≤ ↑↑r * (2 * ε ^ 2 + 8 * |↑↑r - ↑↑(representative phase (bucket phase r))| / ↑(max 1 (min ↑r ↑(representative phase (bucket phase r)))) + 4 * if bucket phase r = bucket phase s then 0 else 1)
theorem
QuantumParallelRepetition.exists_proofDSVDensityRationalPublicBucketPhysicalMixedPrefixCleanup_sq
{Ω : Type u_1}
{I : Type u_2}
[DecidableEq I]
{N : ℕ}
(grid : 0 < N)
(bucket : Ω → Fin (N + 1) → I)
(representative : Ω → I → Fin (N + 1))
(ε : ℝ)
(precision : 0 < ε)
:
∃ (n : ℕ),
0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)),
∀ (phase : Ω) (r s : Fin (N + 1)),
‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s))
(dSVDensityRationalMixedCanonicalPrefixPureHarmonicTensor n
(dSVCanonicalFailurePrefix (dSVDensityRationalPublicBucketPhysicalCommonRank r s))) - √↑↑r • embezzlementState (N * n)‖ ^ 2 ≤ 2 * |↑↑r - ↑↑s| + 2 * ↑↑r * (2 * ε ^ 2 + 8 * |↑↑r - ↑↑(representative phase (bucket phase r))| / ↑(max 1 (min ↑r ↑(representative phase (bucket phase r)))) + 4 * if bucket phase r = bucket phase s then 0 else 1)
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalPhaseWeightedMixedError
{d N n B : ℕ}
(Q : ℕ)
(w : ℝ)
(ξ ζ : BipartiteUnitVector d)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentMixedState
{d N B : ℕ}
(w : ℝ)
(n : ℕ)
(ξ ζ : BipartiteUnitVector d)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentTargetState
{d N B : ℕ}
(w : ℝ)
(n : ℕ)
(ξ ζ : BipartiteUnitVector d)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentLocalReset
{d N B n : ℕ}
(Q : ℕ)
(w : ℝ)
(ξ ζ : BipartiteUnitVector d)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ))
(z : EuclideanSpace ℂ (((_ : Fin B × Fin d) × Fin (N * n)) × (_ : Fin B × Fin d) × Fin (N * n)))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.dSVDensityRationalPublicBucketPhysicalCoherentMixedReset_distance_sq
{d N B n : ℕ}
(phases : 0 < B)
(Q : ℕ)
(w : ℝ)
(ξ ζ : BipartiteUnitVector d)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ))
:
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeightedCrossing_nonneg
{N : ℕ}
(Q B : ℕ)
(r s : Fin (N + 1))
:
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_val_pos
{N B : ℕ}
(Q : ℕ)
(phase : Fin B)
(r : Fin (N + 1))
(nonzero : ↑r ≠ 0)
:
0 < ↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r))
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_actual_log_sub_lt
{N B Q : ℕ}
(positive_Q : 0 < Q)
(phase : Fin B)
(r : Fin (N + 1))
(nonzero : ↑r ≠ 0)
:
|Real.log ↑↑r - Real.log
↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase
(dSVDensityRationalPublicLogRankBucket Q phase r))| < (↑B + 1) / ↑Q
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_rank_ratio_lt
{N B Q : ℕ}
(positive_Q : 0 < Q)
(phase : Fin B)
(r : Fin (N + 1))
(nonzero : ↑r ≠ 0)
:
↑↑r / ↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) < Real.exp ((↑B + 1) / ↑Q)
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_relative_sub_lt
{N B Q : ℕ}
(positive_Q : 0 < Q)
(phase : Fin B)
(r : Fin (N + 1))
(nonzero : ↑r ≠ 0)
:
(↑↑r - ↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase
(dSVDensityRationalPublicLogRankBucket Q phase r))) / ↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) < Real.exp ((↑B + 1) / ↑Q) - 1
theorem
QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_relative_abs_lt
{N B Q : ℕ}
(positive_Q : 0 < Q)
(phase : Fin B)
(r : Fin (N + 1))
(nonzero : ↑r ≠ 0)
:
|↑↑r - ↑↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase
(dSVDensityRationalPublicLogRankBucket Q phase r))| / ↑(max 1
(min ↑r
↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase
(dSVDensityRationalPublicLogRankBucket Q phase r)))) < Real.exp ((↑B + 1) / ↑Q) - 1