@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactLocallySampleableTuple
(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))
:
Type (max (max (max (max (max u_8 u_7) u_6) u_5) u_6) u_5)
Equations
Instances For
def
QuantumParallelRepetition.exactHistoryCode
{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))
(q : ExactJointOutcome X Y A B D)
:
ExactHistoryFlag X Y A B D
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactLocallySampleableCode
{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))
(q : ExactJointOutcome X Y A B D)
:
ExactLocallySampleableTuple X Y A B D
Equations
- QuantumParallelRepetition.exactLocallySampleableCode D q = (q.1.coordinate, q.2.1 ↑q.1.coordinate, q.2.2.1 ↑q.1.coordinate, QuantumParallelRepetition.exactHistoryCode D q)
Instances For
noncomputable def
QuantumParallelRepetition.exactLocallySampleableLaw
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
ExactLocallySampleableTuple X Y A B D → ℝ
Equations
Instances For
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_nonneg
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(t : ExactLocallySampleableTuple X Y A B D)
:
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_sum
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
:
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_eq_zero_of_question_zero
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(zero : G.questionWeight x y = 0)
:
noncomputable def
QuantumParallelRepetition.exactAliceLocalMass
{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))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(x : X)
:
Equations
- QuantumParallelRepetition.exactAliceLocalMass D Q i x = ∑ r : QuantumParallelRepetition.ExactHistoryFlag X Y A B D, ∑ y : Y, Q (i, x, y, r)
Instances For
noncomputable def
QuantumParallelRepetition.exactBobLocalMass
{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))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(y : Y)
:
Equations
- QuantumParallelRepetition.exactBobLocalMass D Q i y = ∑ r : QuantumParallelRepetition.ExactHistoryFlag X Y A B D, ∑ x : X, Q (i, x, y, r)
Instances For
theorem
QuantumParallelRepetition.exactAliceLocalMass_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]
{n : ℕ}
(D : Finset (Fin n))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
:
theorem
QuantumParallelRepetition.exactBobLocalMass_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]
{n : ℕ}
(D : Finset (Fin n))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(y : Y)
:
noncomputable def
QuantumParallelRepetition.exactAliceLocalConditional
{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))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(x : X)
(r : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactBobLocalConditional
{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))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactAliceLocalConditional_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
(r : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactBobLocalConditional_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactAliceLocalMass_zero_apply
{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))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(zero : exactAliceLocalMass D Q i x = 0)
:
theorem
QuantumParallelRepetition.exactBobLocalMass_zero_apply
{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))
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(zero : exactBobLocalMass D Q i y = 0)
:
theorem
QuantumParallelRepetition.exactAliceLocalConditional_zero_apply
{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))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(zero : exactAliceLocalConditional D base Q i x r = 0)
:
theorem
QuantumParallelRepetition.exactBobLocalConditional_zero_apply
{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))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(i : SourceRemainingCoordinate D)
(x : X)
(y : Y)
(r : ExactHistoryFlag X Y A B D)
(zero : exactBobLocalConditional D base Q i y r = 0)
:
theorem
QuantumParallelRepetition.exactAliceLocalConditional_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(x : X)
:
theorem
QuantumParallelRepetition.exactBobLocalConditional_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(i : SourceRemainingCoordinate D)
(y : Y)
:
noncomputable def
QuantumParallelRepetition.exactLocallySampleableJA
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactLocallySampleableJB
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactLocallySampleableJA_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)
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
theorem
QuantumParallelRepetition.exactLocallySampleableJB_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)
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
theorem
QuantumParallelRepetition.exactRemainingCoordinate_card_pos
{n : ℕ}
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
:
theorem
QuantumParallelRepetition.exactLocallySampleableJA_sum
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(base : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactLocallySampleableJB_sum
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(base : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_absolute_continuous_JA
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
exactLocallySampleableJA G n S D base t = 0 → exactLocallySampleableLaw G n S D t = 0
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_absolute_continuous_JB
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(t : ExactLocallySampleableTuple X Y A B D)
:
exactLocallySampleableJB G n S D base t = 0 → exactLocallySampleableLaw G n S D t = 0
theorem
QuantumParallelRepetition.exactLocallySampleableJA_pinsker
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
:
Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) ≤ √(Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) / 2)
theorem
QuantumParallelRepetition.exactLocallySampleableJB_pinsker
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
:
Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) ≤ √(Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) / 2)
noncomputable def
QuantumParallelRepetition.exactLocalConditionalFamily
{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))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(k : ExactLocalSamplerIndex X Y D)
(r : ExactHistoryFlag X Y A B D)
:
Equations
- QuantumParallelRepetition.exactLocalConditionalFamily D base Q (Sum.inl (i, x)) r = QuantumParallelRepetition.exactAliceLocalConditional D base Q i x r
- QuantumParallelRepetition.exactLocalConditionalFamily D base Q (Sum.inr (i, y)) r = QuantumParallelRepetition.exactBobLocalConditional D base Q i y r
Instances For
theorem
QuantumParallelRepetition.exactLocalConditionalFamily_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(nonnegative : ∀ (t : ExactLocallySampleableTuple X Y A B D), 0 ≤ Q t)
(k : ExactLocalSamplerIndex X Y D)
(r : ExactHistoryFlag X Y A B D)
:
theorem
QuantumParallelRepetition.exactLocalConditionalFamily_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]
{n : ℕ}
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(Q : ExactLocallySampleableTuple X Y A B D → ℝ)
(k : ExactLocalSamplerIndex X Y D)
:
noncomputable def
QuantumParallelRepetition.exactConditionalQuestionWeight
{X : Type u_1}
{Y : Type u_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)
(xs : Fin n → X)
(ys : Fin n → Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFiberQuestionMass_eq_jointQuestionMass
{X : Type u_1}
{Y : Type u_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)
:
noncomputable def
QuantumParallelRepetition.exactJointAliceQuestionFilter
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(y : Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointBobQuestionFilter
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(y : Y)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointAliceCoordinateFilter
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(y : Y)
(a : A)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactJointBobCoordinateFilter
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(y : Y)
(b : B)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFiber_born_of_rank_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)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
(EA : (Fin n → X) → Matrix S.Alice S.Alice ℂ)
(EB : (Fin n → Y) → Matrix S.Bob S.Bob ℂ)
:
((bornTracePairing S.state.matrix)
(∑ xs : Fin n → X,
(exactFiberAliceMarginal G n D seed history x y xs / exactFiberQuestionMass G n D seed history x y) • EA xs))
(∑ ys : Fin n → Y,
(exactFiberBobMarginal G n D seed history x y ys / exactFiberQuestionMass G n D seed history x y) • EB ys) = ∑ xs : Fin n → X,
∑ ys : Fin n → Y,
exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (EA xs)) (EB ys)
theorem
QuantumParallelRepetition.exactJointQuestionFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(aliceAnswer : ↥D → A)
(bobAnswer : ↥D → B)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
((bornTracePairing S.state.matrix) (exactJointAliceQuestionFilter G n S D seed history aliceAnswer x y))
(exactJointBobQuestionFilter G n S D seed history bobAnswer x y) = ∑ xs : Fin n → X,
∑ ys : Fin n → Y,
exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D aliceAnswer xs))
(conditionedBobEffect G n S D bobAnswer ys)
theorem
QuantumParallelRepetition.exactJointCoordinateFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(aliceAnswer : ↥D → A)
(bobAnswer : ↥D → B)
(x : X)
(y : Y)
(a : A)
(b : B)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
((bornTracePairing S.state.matrix) (exactJointAliceCoordinateFilter G n S D seed history aliceAnswer x y a))
(exactJointBobCoordinateFilter G n S D seed history bobAnswer x y b) = ∑ xs : Fin n → X,
∑ ys : Fin n → Y,
exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix)
(conditionedAliceCoordinateEffect G n S D aliceAnswer xs (↑seed.coordinate) a))
(conditionedBobCoordinateEffect G n S D bobAnswer ys (↑seed.coordinate) b)
noncomputable def
QuantumParallelRepetition.exactJointConditionalWinningMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactJointConditionalWinningMass_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(aliceAnswer : ↥D → A)
(bobAnswer : ↥D → B)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactJointConditionalWinningMass G n S D seed history aliceAnswer bobAnswer x y = ∑ a : A,
∑ b : B,
if G.predicate x y a b = true then
∑ xs : Fin n → X,
∑ ys : Fin n → Y,
exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix)
(conditionedAliceCoordinateEffect G n S D aliceAnswer xs (↑seed.coordinate) a))
(conditionedBobCoordinateEffect G n S D bobAnswer ys (↑seed.coordinate) b)
else 0
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_sum_bobQuestion
{X : Type u_1}
{Y : Type u_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)
(xs : Fin n → X)
(ys : Fin n → Y)
:
∑ y : Y, exactFiberQuestionWeight G n D seed history x y xs ys = if exactRevealCode D seed (xs, ys) = history ∧ xs ↑seed.coordinate = x then exactPriorQuestionWeight G n (xs, ys)
else 0
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_sum_aliceQuestion
{X : Type u_1}
{Y : Type u_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)
(xs : Fin n → X)
(ys : Fin n → Y)
:
∑ x : X, exactFiberQuestionWeight G n D seed history x y xs ys = if exactRevealCode D seed (xs, ys) = history ∧ ys ↑seed.coordinate = y then exactPriorQuestionWeight G n (xs, ys)
else 0
theorem
QuantumParallelRepetition.exactAliceQuestionMass_eq_sum_fiberMass
{X : Type u_1}
{Y : Type u_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)
:
exactAliceQuestionMass G n D seed history x = ∑ y : Y, exactFiberQuestionMass G n D seed history x y
theorem
QuantumParallelRepetition.exactBobQuestionMass_eq_sum_fiberMass
{X : Type u_1}
{Y : Type u_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)
:
theorem
QuantumParallelRepetition.exactCompatible_aliceMixed_coordinate_eq_or
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y y' : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
(ha : exactAliceQuestionCompatible D seed history x xs)
(ha' : exactAliceQuestionCompatible D seed history x xs')
(hb : exactBobQuestionCompatible D seed history y ys)
(hb' : exactBobQuestionCompatible D seed history y' ys')
(j : Fin n)
:
theorem
QuantumParallelRepetition.exactQuestionWeight_aliceMixed_rectangle
{X : Type u_1}
{Y : Type u_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' : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
(ha : exactAliceQuestionCompatible D seed history x xs)
(ha' : exactAliceQuestionCompatible D seed history x xs')
(hb : exactBobQuestionCompatible D seed history y ys)
(hb' : exactBobQuestionCompatible D seed history y' ys')
:
(G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_aliceMixed_rectangle
{X : Type u_1}
{Y : Type u_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' : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
:
exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x y' xs' ys' = exactFiberQuestionWeight G n D seed history x y' xs ys' * exactFiberQuestionWeight G n D seed history x y xs' ys
theorem
QuantumParallelRepetition.exactCompatible_bobMixed_coordinate_eq_or
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x x' : X)
(y : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
(ha : exactAliceQuestionCompatible D seed history x xs)
(ha' : exactAliceQuestionCompatible D seed history x' xs')
(hb : exactBobQuestionCompatible D seed history y ys)
(hb' : exactBobQuestionCompatible D seed history y ys')
(j : Fin n)
:
theorem
QuantumParallelRepetition.exactQuestionWeight_bobMixed_rectangle
{X : Type u_1}
{Y : Type u_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' : X)
(y : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
(ha : exactAliceQuestionCompatible D seed history x xs)
(ha' : exactAliceQuestionCompatible D seed history x' xs')
(hb : exactBobQuestionCompatible D seed history y ys)
(hb' : exactBobQuestionCompatible D seed history y ys')
:
(G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_bobMixed_rectangle
{X : Type u_1}
{Y : Type u_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' : X)
(y : Y)
(xs xs' : Fin n → X)
(ys ys' : Fin n → Y)
:
exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x' y xs' ys' = exactFiberQuestionWeight G n D seed history x y xs ys' * exactFiberQuestionWeight G n D seed history x' y xs' ys
theorem
QuantumParallelRepetition.exactFiberAliceMarginal_mul_cross_mass
{X : Type u_1}
{Y : Type u_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' : Y)
(xs : Fin n → X)
:
exactFiberAliceMarginal G n D seed history x y xs * exactFiberQuestionMass G n D seed history x y' = exactFiberAliceMarginal G n D seed history x y' xs * exactFiberQuestionMass G n D seed history x y
theorem
QuantumParallelRepetition.exactFiberBobMarginal_mul_cross_mass
{X : Type u_1}
{Y : Type u_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' : X)
(y : Y)
(ys : Fin n → Y)
:
exactFiberBobMarginal G n D seed history x y ys * exactFiberQuestionMass G n D seed history x' y = exactFiberBobMarginal G n D seed history x' y ys * exactFiberQuestionMass G n D seed history x y
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_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)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
(xs : Fin n → X)
(ys : Fin n → Y)
:
theorem
QuantumParallelRepetition.exactFiberQuestionMass_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)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
:
theorem
QuantumParallelRepetition.exactAliceFiberNormalizedRow
{X : Type u_1}
{Y : Type u_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)
(xs : Fin n → X)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactFiberAliceMarginal G n D seed history x y xs / exactFiberQuestionMass G n D seed history x y = (∑ yy : Y, exactFiberAliceMarginal G n D seed history x yy xs) / exactAliceQuestionMass G n D seed history x
theorem
QuantumParallelRepetition.exactBobFiberNormalizedColumn
{X : Type u_1}
{Y : Type u_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)
(ys : Fin n → Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactFiberBobMarginal G n D seed history x y ys / exactFiberQuestionMass G n D seed history x y = (∑ xx : X, exactFiberBobMarginal G n D seed history xx y ys) / exactBobQuestionMass G n D seed history y
theorem
QuantumParallelRepetition.exactAliceConditionalMatrix_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]
{d : Type u_5}
[Fintype d]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
(E : (Fin n → X) → Matrix d d ℂ)
:
(∑ 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) • E q.1
else 0) = ∑ xs : Fin n → X,
(exactFiberAliceMarginal G n D seed history x y xs / exactFiberQuestionMass G n D seed history x y) • E xs
theorem
QuantumParallelRepetition.exactBobConditionalMatrix_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]
{d : Type u_5}
[Fintype d]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
(E : (Fin n → Y) → Matrix d d ℂ)
:
(∑ 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) • E q.2
else 0) = ∑ ys : Fin n → Y,
(exactFiberBobMarginal G n D seed history x y ys / exactFiberQuestionMass G n D seed history x y) • E ys
theorem
QuantumParallelRepetition.exactAliceQuestionFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → A)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactAliceQuestionFilter G n S D seed history answer x = exactJointAliceQuestionFilter G n S D seed history answer x y
theorem
QuantumParallelRepetition.exactBobQuestionFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → B)
(x : X)
(y : Y)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactBobQuestionFilter G n S D seed history answer y = exactJointBobQuestionFilter G n S D seed history answer x y
theorem
QuantumParallelRepetition.exactAliceCoordinateFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → A)
(x : X)
(y : Y)
(a : A)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactAliceCoordinateFilter G n S D seed history answer x a = exactJointAliceCoordinateFilter G n S D seed history answer x y a
theorem
QuantumParallelRepetition.exactBobCoordinateFilter_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))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(answer : ↥D → B)
(x : X)
(y : Y)
(b : B)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
exactBobCoordinateFilter G n S D seed history answer y b = exactJointBobCoordinateFilter G n S D seed history answer x y b
theorem
QuantumParallelRepetition.exactSourceEquationTen
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(nonzero : exactFiberQuestionMass G n D seed history x y ≠ 0)
:
((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D seed history aliceAnswer x))
(exactBobQuestionFilter G n S D seed history bobAnswer y) = ∑ xs : Fin n → X,
∑ ys : Fin n → Y,
exactConditionalQuestionWeight G n D seed history x y xs ys * ((bornTracePairing S.state.matrix) (conditionedAliceEffect G n S D aliceAnswer xs))
(conditionedBobEffect G n S D bobAnswer ys)
noncomputable def
QuantumParallelRepetition.exactFixedBobQuestionMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixed : Finset (Fin n))
(xs : Fin n → X)
(known : Fin n → Y)
:
Equations
- QuantumParallelRepetition.exactFixedBobQuestionMass G n fixed xs known = ∑ ys : Fin n → Y, if ∀ j ∈ fixed, ys j = known j then (G.repeat n).questionWeight xs ys else 0
Instances For
noncomputable def
QuantumParallelRepetition.exactFixedAliceQuestionMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixed : Finset (Fin n))
(known : Fin n → X)
(ys : Fin n → Y)
:
Equations
- QuantumParallelRepetition.exactFixedAliceQuestionMass G n fixed known ys = ∑ xs : Fin n → X, if ∀ j ∈ fixed, xs j = known j then (G.repeat n).questionWeight xs ys else 0
Instances For
theorem
QuantumParallelRepetition.exactFixedBobQuestionMass_eq_product
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixed : Finset (Fin n))
(xs : Fin n → X)
(known : Fin n → Y)
:
exactFixedBobQuestionMass G n fixed xs known = ∏ j : Fin n, if j ∈ fixed then G.questionWeight (xs j) (known j) else G.marginalX (xs j)
theorem
QuantumParallelRepetition.exactFixedAliceQuestionMass_eq_product
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(fixed : Finset (Fin n))
(known : Fin n → X)
(ys : Fin n → Y)
:
exactFixedAliceQuestionMass G n fixed known ys = ∏ j : Fin n, if j ∈ fixed then G.questionWeight (known j) (ys j) else G.marginalY (ys j)
theorem
QuantumParallelRepetition.exactFixedBobQuestionMass_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 : ℕ)
(fixed : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixed)
(xs : Fin n → X)
(known : Fin n → Y)
(y : Y)
:
exactFixedBobQuestionMass G n (insert j fixed) xs (Function.update known j y) = G.conditionalYGivenX (xs j) y * exactFixedBobQuestionMass G n fixed xs known
theorem
QuantumParallelRepetition.exactFixedAliceQuestionMass_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 : ℕ)
(fixed : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixed)
(known : Fin n → X)
(ys : Fin n → Y)
(x : X)
:
exactFixedAliceQuestionMass G n (insert j fixed) (Function.update known j x) ys = G.conditionalXGivenY (ys j) x * exactFixedAliceQuestionMass G n fixed known ys
def
QuantumParallelRepetition.exactReverseLeftSide
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Finset M
Equations
Instances For
def
QuantumParallelRepetition.exactReverseRightSide
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Finset M
Equations
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseLeftSide_coordinate_mem
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseRightSide_coordinate_mem
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseLeftSide_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseRightSide_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseLeftSide_markedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseRightSide_markedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactRemainingReverse_relativeEntropy_budget
{n : ℕ}
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(increment : (s : Finset (SourceRemainingCoordinate D)) → Fin s.card → ℝ)
{cost : ℝ}
(nonnegative_cost : 0 ≤ cost)
(budget : ∀ (s : Finset (SourceRemainingCoordinate D)), ∑ k : Fin s.card, increment s k ≤ cost)
:
∑ s : Finset (SourceRemainingCoordinate D), reversePartitionWeight s * ((∑ k : Fin s.card, increment s k) / ↑s.card) ≤ 2 * cost / ↑(Finset.univ \ D).card
noncomputable def
QuantumParallelRepetition.exactReverseLeftSeedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseRightSeedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseLeftPermutation_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Fintype.card (Equiv.Perm ↥(exactReverseLeftSide seed)) = Fintype.card (Equiv.Perm ↥(exactLeft seed.coordinate seed.partition)) * ((exactLeft seed.coordinate seed.partition).card + 1)
theorem
QuantumParallelRepetition.exactReverseRightPermutation_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Fintype.card (Equiv.Perm ↥(exactReverseRightSide seed)) = Fintype.card (Equiv.Perm ↥(exactRight seed.coordinate seed.partition)) * ((exactRight seed.coordinate seed.partition).card + 1)
theorem
QuantumParallelRepetition.exactReverseLeftSeedWeight_eq_forward
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseRightSeedWeight_eq_forward
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
def
QuantumParallelRepetition.exactHistoryAccepted
{X : Type u_1}
{Y : Type u_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))
(r : ExactHistoryFlag X Y A B D)
:
Equations
- QuantumParallelRepetition.exactHistoryAccepted G n D r = ∀ (j : ↥D), G.predicate (r.history.aliceConditioned j) (r.history.bobConditioned j) (r.aliceAnswer j) (r.bobAnswer j) = true
Instances For
theorem
QuantumParallelRepetition.exactHistoryCode_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))
(q : ExactJointOutcome X Y A B D)
:
exactHistoryAccepted G n D (exactHistoryCode D q) ↔ q.2 ∈ FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_zero_of_not_accepted
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(not_accepted : ¬exactHistoryAccepted G n D r)
:
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactGlobalHistoryLocalIndex
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
Type (max (max (max u_1 u_2) u_3) u_4)
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactGlobalHistoryVector
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(z : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r))
:
EuclideanSpace ℂ (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D)
Equations
Instances For
theorem
QuantumParallelRepetition.exactGlobalHistoryVector_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)
(z : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r))
:
theorem
QuantumParallelRepetition.exactGlobalHistoryVector_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))
(r : ExactHistoryFlag X Y A B D)
(u v : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r))
:
exactGlobalHistoryVector G n S D r (u - v) = exactGlobalHistoryVector G n S D r u - exactGlobalHistoryVector G n S D r v
noncomputable def
QuantumParallelRepetition.exactGlobalHistoryFinReindex
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
EuclideanSpace ℂ (ExactGlobalHistoryLocalIndex G n S D × ExactGlobalHistoryLocalIndex G n S D) ≃ₗᵢ[ℂ] EuclideanSpace ℂ
(Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) × Fin (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)))
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactGlobalHistoryFinGamma
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactGlobalHistoryFinPhi
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactGlobalHistoryFinPsi
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactGlobalHistoryFinGamma_sub_Psi_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)
:
‖↑(exactGlobalHistoryFinGamma G n S D r x) - ↑(exactGlobalHistoryFinPsi G n S D r x y)‖ = ‖exactGamma G n S D r x - exactPsi G n S D r x y‖
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactSourceGlobalState
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactSourceTuplePsi
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(t : ExactLocallySampleableTuple X Y A B D)
:
ExactSourceGlobalState G n S D
Equations
- QuantumParallelRepetition.exactSourceTuplePsi G n S D t = ↑(QuantumParallelRepetition.exactGlobalHistoryFinPsi G n S D t.2.2.2 t.2.1 t.2.2.1)
Instances For
noncomputable def
QuantumParallelRepetition.exactSourceTupleGamma
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(t : ExactLocallySampleableTuple X Y A B D)
:
ExactSourceGlobalState G n S D
Equations
- QuantumParallelRepetition.exactSourceTupleGamma G n S D t = ↑(QuantumParallelRepetition.exactGlobalHistoryFinGamma G n S D t.2.2.2 t.2.1)
Instances For
noncomputable def
QuantumParallelRepetition.exactSourceTuplePhi
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(t : ExactLocallySampleableTuple X Y A B D)
:
ExactSourceGlobalState G n S D
Equations
- QuantumParallelRepetition.exactSourceTuplePhi G n S D t = ↑(QuantumParallelRepetition.exactGlobalHistoryFinPhi G n S D t.2.2.2 t.2.2.1)
Instances For
def
QuantumParallelRepetition.ExactSourceStateDistanceBound
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactPsiPhi_BornWeighted_normalized_distance
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactGammaPsi_BornWeighted_normalized_distance
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
‖exactUnnormalizedPsi G n S D r x y‖ ^ 2 * ‖exactGamma G n S D r x - exactPsi G n S D r x y‖ ^ 2 ≤ 4 * ‖exactUnnormalizedGamma G n S D r x - exactUnnormalizedPsi G n S D r x y‖ ^ 2
theorem
QuantumParallelRepetition.exactSourceEquationTwentyOne_of_fifteen
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(η : ℝ)
(distance : ExactSourceStateDistanceBound G n S D η)
:
∑ t : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D t * ‖exactSourceTupleGamma G n S D t - exactSourceTuplePhi G n S D t‖ ^ 2 ≤ 32 * η
noncomputable def
QuantumParallelRepetition.exactFairAliceQuestionEntropyIncrement
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobQuestionEntropyIncrement
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairAlice_conditional_variation_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)
(hy : 0 < G.marginalY y)
:
∑ x : X, G.conditionalXGivenY y x * ‖exactUnnormalizedPsi G n S D r x y - exactUnnormalizedPhi G n S D r y‖ ^ 2 ≤ exactFairAliceQuestionEntropyIncrement G n S D r y
theorem
QuantumParallelRepetition.exactFairBob_conditional_variation_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)
(hx : 0 < G.marginalX x)
:
∑ y : Y, G.conditionalYGivenX x y * ‖exactUnnormalizedPsi G n S D r x y - exactUnnormalizedGamma G n S D r x‖ ^ 2 ≤ exactFairBobQuestionEntropyIncrement G n S D r x
noncomputable def
QuantumParallelRepetition.exactFairAliceHistoryVariation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobHistoryVariation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAliceHistoryEntropyIncrement
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- QuantumParallelRepetition.exactFairAliceHistoryEntropyIncrement G n S D r = ∑ y : Y, G.marginalY y * QuantumParallelRepetition.exactFairAliceQuestionEntropyIncrement G n S D r y
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobHistoryEntropyIncrement
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- QuantumParallelRepetition.exactFairBobHistoryEntropyIncrement G n S D r = ∑ x : X, G.marginalX x * QuantumParallelRepetition.exactFairBobQuestionEntropyIncrement G n S D r x
Instances For
theorem
QuantumParallelRepetition.exactAcceptedFairAliceVariation_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,
if exactHistoryAccepted G n D r then exactFairHistoryPriorWeight G n D r * exactFairAliceHistoryVariation G n S D r
else 0) ≤ ∑ r : ExactHistoryFlag X Y A B D,
if exactHistoryAccepted G n D r then
exactFairHistoryPriorWeight G n D r * exactFairAliceHistoryEntropyIncrement G n S D r
else 0
theorem
QuantumParallelRepetition.exactAcceptedFairBobVariation_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,
if exactHistoryAccepted G n D r then exactFairHistoryPriorWeight G n D r * exactFairBobHistoryVariation G n S D r
else 0) ≤ ∑ r : ExactHistoryFlag X Y A B D,
if exactHistoryAccepted G n D r then
exactFairHistoryPriorWeight G n D r * exactFairBobHistoryEntropyIncrement G n S D r
else 0
noncomputable def
QuantumParallelRepetition.exactSourceClassicalInformationRate
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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
def
QuantumParallelRepetition.ExactSourceClassicalInformationBound
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFiniteRelativeEntropy_equiv
{ι : Type u_5}
{κ : Type u_6}
[Fintype ι]
[Fintype κ]
(e : ι ≃ κ)
(p q : ι → ℝ)
:
(Pinsker.finiteRelativeEntropy (fun (k : κ) => p (e.symm k)) fun (k : κ) => q (e.symm k)) = Pinsker.finiteRelativeEntropy p q
def
QuantumParallelRepetition.exactAliceInformationEquiv
{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))
:
ExactLocallySampleableTuple X Y A B D ≃ (SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D × Y
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactBobInformationEquiv
{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))
:
ExactLocallySampleableTuple X Y A B D ≃ (SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D × X
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactAliceInformationPosterior
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
(SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D × Y → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactAliceInformationReference
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
(SourceRemainingCoordinate D × X) × ExactHistoryFlag X Y A B D × Y → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactBobInformationPosterior
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
(SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D × X → ℝ
Equations
Instances For
noncomputable def
QuantumParallelRepetition.exactBobInformationReference
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
(SourceRemainingCoordinate D × Y) × ExactHistoryFlag X Y A B D × X → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exact_source_equation_twenty_four_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 : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
:
Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) = Pinsker.finiteRelativeEntropy (ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D))
(ClassicalInformation.jointFirstMarginal (exactAliceInformationReference G n S D base)) + ∑ ix : SourceRemainingCoordinate D × X,
ClassicalInformation.jointFirstMarginal (exactAliceInformationPosterior G n S D) ix * Pinsker.finiteRelativeEntropy
(ClassicalInformation.jointConditional (exactAliceInformationPosterior G n S D) ix)
(ClassicalInformation.jointConditional (exactAliceInformationReference G n S D base) ix)
theorem
QuantumParallelRepetition.exact_source_equation_twenty_four_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 : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
:
Pinsker.finiteRelativeEntropy (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) = Pinsker.finiteRelativeEntropy (ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D))
(ClassicalInformation.jointFirstMarginal (exactBobInformationReference G n S D base)) + ∑ iy : SourceRemainingCoordinate D × Y,
ClassicalInformation.jointFirstMarginal (exactBobInformationPosterior G n S D) iy * Pinsker.finiteRelativeEntropy (ClassicalInformation.jointConditional (exactBobInformationPosterior G n S D) iy)
(ClassicalInformation.jointConditional (exactBobInformationReference G n S D base) iy)
theorem
QuantumParallelRepetition.exact_source_alice_pinsker_of_classical_information
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(information : ExactSourceClassicalInformationBound G n S D base)
:
Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJA G n S D base) ≤ exactSourcePinskerRate G n S D
theorem
QuantumParallelRepetition.exact_source_bob_pinsker_of_classical_information
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(information : ExactSourceClassicalInformationBound G n S D base)
:
Pinsker.finiteTotalVariation (exactLocallySampleableLaw G n S D) (exactLocallySampleableJB G n S D base) ≤ exactSourcePinskerRate G n S D
theorem
QuantumParallelRepetition.exactSeedCoordinateFiber_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(coordinate : M)
:
∑ partition : M → Bool,
∑ leftOrder : Equiv.Perm ↥(exactLeft coordinate partition),
∑ rightOrder : Equiv.Perm ↥(exactRight coordinate partition),
∑ leftCut : Fin ((exactLeft coordinate partition).card + 1),
∑ rightCut : Fin ((exactRight coordinate partition).card + 1),
exactSeedWeight
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut } = 1 / ↑(Fintype.card M)
theorem
QuantumParallelRepetition.exactSeedWeight_coordinate_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(f : M → ℝ)
:
∑ seed : ExactForwardSeed M, exactSeedWeight seed * f seed.coordinate = ∑ i : M, 1 / ↑(Fintype.card M) * f i
theorem
QuantumParallelRepetition.exactSeedWeight_coordinate_marginal
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(i : M)
:
(∑ seed : ExactForwardSeed M, if seed.coordinate = i then exactSeedWeight seed else 0) = 1 / ↑(Fintype.card M)
def
QuantumParallelRepetition.exactAliceQuestionPriorMarginal
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(x : X)
:
Equations
- QuantumParallelRepetition.exactAliceQuestionPriorMarginal G x = ∑ y : Y, G.questionWeight x y
Instances For
def
QuantumParallelRepetition.exactBobQuestionPriorMarginal
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(y : Y)
:
Equations
- QuantumParallelRepetition.exactBobQuestionPriorMarginal G y = ∑ x : X, G.questionWeight x y
Instances For
theorem
QuantumParallelRepetition.exactAliceInformationReference_firstMarginal
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(i : SourceRemainingCoordinate D)
(x : X)
:
ClassicalInformation.jointFirstMarginal (exactAliceInformationReference G n S D base) (i, x) = exactAliceQuestionPriorMarginal G x / ↑(Fintype.card (SourceRemainingCoordinate D))
theorem
QuantumParallelRepetition.exactBobInformationReference_firstMarginal
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
(i : SourceRemainingCoordinate D)
(y : Y)
:
ClassicalInformation.jointFirstMarginal (exactBobInformationReference G n S D base) (i, y) = exactBobQuestionPriorMarginal G y / ↑(Fintype.card (SourceRemainingCoordinate D))
theorem
QuantumParallelRepetition.exactGroupedMass_decidableEq_irrel
{Ω : Type u_5}
{κ : Type u_6}
[Fintype Ω]
(first second : DecidableEq κ)
(projection : Ω → κ)
(mass : Ω → ℝ)
:
noncomputable def
QuantumParallelRepetition.exactAliceSourceMarginalInformation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactBobSourceMarginalInformation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactAliceSourceConditionalInformation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactBobSourceConditionalInformation
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(base : ExactHistoryFlag X Y A B D)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactInsertedRank
{M : Type u_1}
[DecidableEq M]
(i : M)
(side : Finset M)
(not_mem : i ∉ side)
(rank : ↥side ≃ Fin side.card)
(cut : Fin (side.card + 1))
:
Equations
- QuantumParallelRepetition.exactInsertedRank i side not_mem rank cut = (Finset.subtypeInsertEquivOption not_mem).trans (rank.optionCongr.trans (finSuccEquiv' cut).symm)
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactInsertedRank_marker
{M : Type u_1}
[DecidableEq M]
(i : M)
(side : Finset M)
(not_mem : i ∉ side)
(rank : ↥side ≃ Fin side.card)
(cut : Fin (side.card + 1))
:
noncomputable def
QuantumParallelRepetition.exactReverseLeftRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseRightRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseLeftRank_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseRightRank_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseLeftRank_old
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
(j : ↥(exactLeft seed.coordinate seed.partition))
:
theorem
QuantumParallelRepetition.exactReverseRightRank_old
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
(j : ↥(exactRight seed.coordinate seed.partition))
:
theorem
QuantumParallelRepetition.exactInsertedPrefixBefore_marker_eq
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(i : M)
(side : Finset M)
(not_mem : i ∉ side)
(rank : ↥side ≃ Fin side.card)
(cut : Fin (side.card + 1))
:
exactInsertedPrefixBefore i side not_mem rank cut = Finset.image Subtype.val {j : ↥side | ↑(rank j) < ↑cut}
noncomputable def
QuantumParallelRepetition.exactReverseLeftPrefixBeforeMarked
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Finset M
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseRightPrefixBeforeMarked
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Finset M
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseLeftPrefixBeforeMarked_eq
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseRightPrefixBeforeMarked_eq
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
def
QuantumParallelRepetition.exactOrderedSidePrefix
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(rank : ↥side ≃ Fin side.card)
(cut : Fin (side.card + 1))
:
Finset M
Equations
- QuantumParallelRepetition.exactOrderedSidePrefix side rank cut = Finset.image Subtype.val {j : ↥side | ↑(rank j) < ↑cut}
Instances For
theorem
QuantumParallelRepetition.exactInsertedPrefixBefore_mem_iff
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(i : M)
(side : Finset M)
(not_mem : i ∉ side)
(rank : ↥side ≃ Fin side.card)
(cut : Fin (side.card + 1))
(j : M)
:
j ∈ exactInsertedPrefixBefore i side not_mem rank cut ↔ ∃ (hj : j ∈ insert i side), ↑((exactInsertedRank i side not_mem rank cut) ⟨j, hj⟩) < ↑cut
structure
QuantumParallelRepetition.ExactReverseSideContext
(M : Type u_1)
[Fintype M]
[DecidableEq M]
(side : Finset M)
:
Type u_1
Instances For
@[instance_reducible]
instance
QuantumParallelRepetition.instFintypeExactReverseSideContext
{M✝ : Type u_1}
{inst✝ : Fintype M✝}
{inst✝¹ : DecidableEq M✝}
{side✝ : Finset M✝}
[Fintype M✝]
:
Fintype (ExactReverseSideContext M✝ side✝)
Equations
- One or more equations did not get rendered due to their size.
def
QuantumParallelRepetition.exactReverseContextOtherPrefix
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{side : Finset M}
(context : ExactReverseSideContext M side)
:
Finset M
Equations
- QuantumParallelRepetition.exactReverseContextOtherPrefix context = QuantumParallelRepetition.exactOrderedSidePrefix context.otherSide context.otherRank context.otherCut
Instances For
theorem
QuantumParallelRepetition.exactReverseLeftSide_complement
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseRightSide_complement
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
noncomputable def
QuantumParallelRepetition.exactReverseAliceContext
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobContext
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactDefaultReverseSideContext
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
:
ExactReverseSideContext M side
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseAliceContextAt
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
ExactReverseSideContext M side
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobContextAt
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
ExactReverseSideContext M side
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceContextAt_actual
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobContextAt_actual
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceContext_otherPrefix
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobContext_otherPrefix
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactReverseAliceFixedInformation
(X : Type u_5)
(Y : Type u_6)
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
:
Type (max u_5 u_6)
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
QuantumParallelRepetition.ExactReverseBobFixedInformation
(X : Type u_5)
(Y : Type u_6)
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
:
Type (max u_6 u_5)
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseAliceSourceProjection
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
:
ExactJointOutcome X Y A B D → ExactReverseAliceFixedInformation X Y D side × (Fin side.card → Y)
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobSourceProjection
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(side : Finset (SourceRemainingCoordinate D))
:
ExactJointOutcome X Y A B D → ExactReverseBobFixedInformation X Y D side × (Fin side.card → X)
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceContext_marked_rank
{M : Type u_5}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobContext_marked_rank
{M : Type u_5}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
def
QuantumParallelRepetition.exactReverseContextPrefixBefore
{M : Type u_5}
[Fintype M]
[DecidableEq M]
{side : Finset M}
(context : ExactReverseSideContext M side)
(position : Fin side.card)
:
Finset M
Equations
- QuantumParallelRepetition.exactReverseContextPrefixBefore context position = QuantumParallelRepetition.exactOrderedSidePrefix side context.sideRank position.castSucc
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceContext_prefix_before_marked
{M : Type u_5}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
exactReverseContextPrefixBefore (exactReverseAliceContext seed)
((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = exactLeftPrefix seed
theorem
QuantumParallelRepetition.exactReverseBobContext_prefix_before_marked
{M : Type u_5}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
exactReverseContextPrefixBefore (exactReverseBobContext seed)
((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = exactRightPrefix seed
def
QuantumParallelRepetition.exactPrefixNextCode
{Ω : Type u_1}
{V : Type u_2}
{h : ℕ}
(default : V)
(k : Fin h)
:
Equations
- QuantumParallelRepetition.exactPrefixNextCode default k t = (QuantumParallelRepetition.finitePrefixMask default k.castSucc t, t.2 k)
Instances For
theorem
QuantumParallelRepetition.exactPrefixNextDecode_comp
{Ω : Type u_1}
{V : Type u_2}
{h : ℕ}
(default : V)
(k : Fin h)
:
theorem
QuantumParallelRepetition.exactPrefixNextCode_comp
{Ω : Type u_1}
{V : Type u_2}
{h : ℕ}
(default : V)
(k : Fin h)
:
theorem
QuantumParallelRepetition.exactPrefixNext_relativeEntropy_eq
{Ω : Type u_1}
{V : Type u_2}
[Fintype Ω]
[Fintype V]
{h : ℕ}
(joint prior : Ω × (Fin h → V) → ℝ)
(joint_nonnegative : ∀ (t : Ω × (Fin h → V)), 0 ≤ joint t)
(prior_nonnegative : ∀ (t : Ω × (Fin h → V)), 0 ≤ prior t)
(absolute_continuity : ∀ (t : Ω × (Fin h → V)), prior t = 0 → joint t = 0)
(default : V)
(k : Fin h)
:
Pinsker.finiteRelativeEntropy (ClassicalInformation.groupedMass (exactPrefixNextCode default k) joint)
(ClassicalInformation.groupedMass (exactPrefixNextCode default k) prior) = finitePrefixRelativeEntropy joint prior default k.succ
theorem
QuantumParallelRepetition.exactPrefixNext_firstMarginal
{Ω : Type u_1}
{V : Type u_2}
[Fintype Ω]
[Fintype V]
{h : ℕ}
(mass : Ω × (Fin h → V) → ℝ)
(default : V)
(k : Fin h)
:
ClassicalInformation.jointFirstMarginal (ClassicalInformation.groupedMass (exactPrefixNextCode default k) mass) = ClassicalInformation.groupedMass (finitePrefixMask default k.castSucc) mass
theorem
QuantumParallelRepetition.exactPrefixEntropyIncrement_eq_conditional
{Ω : Type u_1}
{V : Type u_2}
[Fintype Ω]
[Fintype V]
{h : ℕ}
(joint prior : Ω × (Fin h → V) → ℝ)
(joint_nonnegative : ∀ (t : Ω × (Fin h → V)), 0 ≤ joint t)
(prior_nonnegative : ∀ (t : Ω × (Fin h → V)), 0 ≤ prior t)
(absolute_continuity : ∀ (t : Ω × (Fin h → V)), prior t = 0 → joint t = 0)
(joint_normalized : ∑ t : Ω × (Fin h → V), joint t = 1)
(prior_normalized : ∑ t : Ω × (Fin h → V), prior t = 1)
(default : V)
(k : Fin h)
:
finitePrefixRelativeEntropy joint prior default k.succ - finitePrefixRelativeEntropy joint prior default k.castSucc = ∑ context : Ω × (Fin h → V),
ClassicalInformation.groupedMass (finitePrefixMask default k.castSucc) joint context * Pinsker.finiteRelativeEntropy
(ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default k) joint)
context)
(ClassicalInformation.jointConditional (ClassicalInformation.groupedMass (exactPrefixNextCode default k) prior)
context)
def
QuantumParallelRepetition.exactReverseAliceCanonicalPartition
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(ignored : Bool)
:
M → Bool
Equations
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceCanonicalPartition_side
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
insert coordinate (exactLeft coordinate (exactReverseAliceCanonicalPartition side coordinate ignored)) = side
theorem
QuantumParallelRepetition.exactReverseAliceCanonicalPartition_unique
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(partition : M → Bool)
(fiber : insert coordinate (exactLeft coordinate partition) = side)
:
def
QuantumParallelRepetition.exactReverseAlicePartitionFiberEquiv
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
QuantumParallelRepetition.exactReverseBobCanonicalPartition
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(ignored : Bool)
:
M → Bool
Equations
Instances For
theorem
QuantumParallelRepetition.exactReverseBobCanonicalPartition_side
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
insert coordinate (exactRight coordinate (exactReverseBobCanonicalPartition side coordinate ignored)) = side
theorem
QuantumParallelRepetition.exactReverseBobCanonicalPartition_unique
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(partition : M → Bool)
(fiber : insert coordinate (exactRight coordinate partition) = side)
:
def
QuantumParallelRepetition.exactReverseBobPartitionFiberEquiv
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseBobPartitionFiber_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
:
Fintype.card { partition : M → Bool // insert coordinate (exactRight coordinate partition) = side } = 2
theorem
QuantumParallelRepetition.exactReverseAlicePartitionFiber_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(weight : ℝ)
:
theorem
QuantumParallelRepetition.exactReverseBobPartitionFiber_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(weight : ℝ)
:
theorem
QuantumParallelRepetition.exactReversePartition_orderCut_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(coordinate : M)
(partition : M → Bool)
:
∑ leftOrder : Equiv.Perm ↥(exactLeft coordinate partition),
∑ rightOrder : Equiv.Perm ↥(exactRight coordinate partition),
∑ leftCut : Fin ((exactLeft coordinate partition).card + 1),
∑ rightCut : Fin ((exactRight coordinate partition).card + 1),
exactSeedWeight
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut } = 1 / ↑(Fintype.card M) * (1 / ↑(Fintype.card (M → Bool)))
theorem
QuantumParallelRepetition.exactReverseAlicePartition_orderCut_fiber_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(partition : M → Bool)
:
(∑ leftOrder : Equiv.Perm ↥(exactLeft coordinate partition),
∑ rightOrder : Equiv.Perm ↥(exactRight coordinate partition),
∑ leftCut : Fin ((exactLeft coordinate partition).card + 1),
∑ rightCut : Fin ((exactRight coordinate partition).card + 1),
if exactReverseLeftSide
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut } = side then
exactSeedWeight
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut }
else 0) = if insert coordinate (exactLeft coordinate partition) = side then
1 / ↑(Fintype.card M) * (1 / ↑(Fintype.card (M → Bool)))
else 0
theorem
QuantumParallelRepetition.exactReverseBobPartition_orderCut_fiber_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(partition : M → Bool)
:
(∑ leftOrder : Equiv.Perm ↥(exactLeft coordinate partition),
∑ rightOrder : Equiv.Perm ↥(exactRight coordinate partition),
∑ leftCut : Fin ((exactLeft coordinate partition).card + 1),
∑ rightCut : Fin ((exactRight coordinate partition).card + 1),
if exactReverseRightSide
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut } = side then
exactSeedWeight
{ coordinate := coordinate, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder,
leftCut := leftCut, rightCut := rightCut }
else 0) = if insert coordinate (exactRight coordinate partition) = side then
1 / ↑(Fintype.card M) * (1 / ↑(Fintype.card (M → Bool)))
else 0
theorem
QuantumParallelRepetition.exactReverseAliceSide_marginal
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
:
theorem
QuantumParallelRepetition.exactReverseBobSide_marginal
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
:
noncomputable def
QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobConditionalSeedWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight_nonneg
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_nonneg
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight_cancel
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(seed : ExactForwardSeed M)
:
reversePartitionWeight side * exactReverseAliceConditionalSeedWeight side seed = if exactReverseLeftSide seed = side then exactSeedWeight seed else 0
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_cancel
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(seed : ExactForwardSeed M)
:
reversePartitionWeight side * exactReverseBobConditionalSeedWeight side seed = if exactReverseRightSide seed = side then exactSeedWeight seed else 0
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(nonempty : side.Nonempty)
:
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(nonempty : side.Nonempty)
:
noncomputable def
QuantumParallelRepetition.exactForwardSeedLaw
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
:
Equations
- QuantumParallelRepetition.exactForwardSeedLaw nonempty = { weight := QuantumParallelRepetition.exactSeedWeight, weight_nonneg := ⋯, weight_sum := ⋯ }
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseAliceConditionalSeedLaw
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobConditionalSeedLaw
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedLaw_weight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(hside : side.Nonempty)
(seed : ExactForwardSeed M)
:
(exactReverseAliceConditionalSeedLaw nonempty side).weight seed = exactReverseAliceConditionalSeedWeight side seed
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedLaw_weight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(hside : side.Nonempty)
(seed : ExactForwardSeed M)
:
(exactReverseBobConditionalSeedLaw nonempty side).weight seed = exactReverseBobConditionalSeedWeight side seed
def
QuantumParallelRepetition.reweightedSeedPriorEventLaw
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
[Fintype K]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
:
FiniteEventLaw (K × ExactOutcome X Y A B n)
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.reweightedSeedWinEvent
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
[Fintype K]
(G : Game X Y A B)
(n : ℕ)
(D : Finset (Fin n))
:
Finset (K × ExactOutcome X Y A B n)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.reweightedSeedWinEventMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
[Fintype K]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
(reweightedSeedPriorEventLaw seedLaw G n S).eventMass (reweightedSeedWinEvent G n D) = repeatedPostselectionMass G n S D
noncomputable def
QuantumParallelRepetition.reweightedSeedPosterior
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
[Fintype K]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
:
K × ExactOutcome X Y A B n → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.reweightedSeedPosterior_eq_product
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
[Fintype K]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(q : K × ExactOutcome X Y A B n)
:
reweightedSeedPosterior seedLaw G n S D q = seedLaw.weight q.1 * repeatedConditionedOutcomeLaw G n S D q.2
theorem
QuantumParallelRepetition.reweightedSeedProjection_relativeEntropy_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]
{K : Type u_5}
{U : Type u_6}
[Fintype K]
[Fintype U]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → U)
:
Pinsker.finiteRelativeEntropy (ClassicalInformation.groupedMass projection (reweightedSeedPosterior seedLaw G n S D))
(ClassicalInformation.groupedMass projection (reweightedSeedPriorEventLaw seedLaw G n S).weight) ≤ postselectionLogCost G n S D
noncomputable def
QuantumParallelRepetition.reweightedSeedFlaggedProjectionLaw
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{U : Type u_6}
{Z : Type u_7}
[Fintype K]
[Fintype U]
[Fintype Z]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(projection : K × ExactOutcome X Y A B n → U)
(flag : K × ExactOutcome X Y A B n → Z)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.reweightedSeedFlaggedProjectionLaw_firstMarginal
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{U : Type u_6}
{Z : Type u_7}
[Fintype K]
[Fintype U]
[Fintype Z]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(projection : K × ExactOutcome X Y A B n → U)
(flag : K × ExactOutcome X Y A B n → Z)
:
ClassicalInformation.jointFirstMarginal (reweightedSeedFlaggedProjectionLaw seedLaw G n S D projection flag) = ClassicalInformation.groupedMass projection (reweightedSeedPosterior seedLaw G n S D)
theorem
QuantumParallelRepetition.reweightedSeed_flagged_projection_relativeEntropy_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]
{K : Type u_5}
{U : Type u_6}
{Z : Type u_7}
[Fintype K]
[Fintype U]
[Fintype Z]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(flag_positive : 0 < Fintype.card Z)
(projection : K × ExactOutcome X Y A B n → U)
(flag : K × ExactOutcome X Y A B n → Z)
:
Pinsker.finiteRelativeEntropy (reweightedSeedFlaggedProjectionLaw seedLaw G n S D projection flag)
(uniformFlagReference
(ClassicalInformation.groupedMass projection (reweightedSeedPriorEventLaw seedLaw G n S).weight)) ≤ postselectionLogCost G n S D + Real.log ↑(Fintype.card Z)
theorem
QuantumParallelRepetition.reweightedSeed_source_equation_twenty_five
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{U : Type u_6}
[Fintype K]
[Fintype U]
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → U)
:
Pinsker.finiteRelativeEntropy
(reweightedSeedFlaggedProjectionLaw seedLaw G n S D projection fun (q : K × ExactOutcome X Y A B n) =>
repeatedConditionedAnswerFlag G n S D q.2)
(uniformFlagReference
(ClassicalInformation.groupedMass projection (reweightedSeedPriorEventLaw seedLaw G n S).weight)) ≤ postselectionLogCost G n S D + answerLogCost D
noncomputable def
QuantumParallelRepetition.reweightedSeedPrefixJoint
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
:
(Ω × ConditionedAnswerFlag A B D) × (Fin h → V) → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.reweightedSeedPrefixPrior
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
:
(Ω × ConditionedAnswerFlag A B D) × (Fin h → V) → ℝ
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.reweightedSeedPrefixJoint_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]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V))
:
theorem
QuantumParallelRepetition.reweightedSeedPrefixPrior_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]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V))
:
noncomputable def
QuantumParallelRepetition.reweightedSeedPrefixEntropyIncrement
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(default : V)
(k : Fin h)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.reweightedSeed_source_equation_twenty_six
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(default : V)
:
∑ k : Fin h, reweightedSeedPrefixEntropyIncrement seedLaw G n S D projection default k ≤ postselectionLogCost G n S D + answerLogCost D
theorem
QuantumParallelRepetition.reweightedSeedPrefixJoint_sum
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
:
∑ t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V), reweightedSeedPrefixJoint seedLaw G n S D projection t = 1
theorem
QuantumParallelRepetition.reweightedSeedPrefixPrior_sum
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
:
∑ t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V), reweightedSeedPrefixPrior seedLaw G n S D projection t = 1
theorem
QuantumParallelRepetition.reweightedSeedPrefix_absolute_continuity
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(t : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V))
:
reweightedSeedPrefixPrior seedLaw G n S D projection t = 0 → reweightedSeedPrefixJoint seedLaw G n S D projection t = 0
theorem
QuantumParallelRepetition.reweightedSeedPrefixEntropyIncrement_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]
{K : Type u_5}
{Ω : Type u_6}
{V : Type u_7}
[Fintype K]
[Fintype Ω]
[Fintype V]
{h : ℕ}
(seedLaw : FiniteEventLaw K)
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(positive : 0 < repeatedPostselectionMass G n S D)
(projection : K × ExactOutcome X Y A B n → Ω × (Fin h → V))
(default : V)
(k : Fin h)
:
reweightedSeedPrefixEntropyIncrement seedLaw G n S D projection default k = ∑ context : (Ω × ConditionedAnswerFlag A B D) × (Fin h → V),
ClassicalInformation.groupedMass (finitePrefixMask default k.castSucc)
(reweightedSeedPrefixJoint seedLaw G n S D projection) context * Pinsker.finiteRelativeEntropy
(ClassicalInformation.jointConditional
(ClassicalInformation.groupedMass (exactPrefixNextCode default k)
(reweightedSeedPrefixJoint seedLaw G n S D projection))
context)
(ClassicalInformation.jointConditional
(ClassicalInformation.groupedMass (exactPrefixNextCode default k)
(reweightedSeedPrefixPrior seedLaw G n S D projection))
context)
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedLaw_weight_cancel
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(seed : ExactForwardSeed M)
:
reversePartitionWeight side * (exactReverseAliceConditionalSeedLaw nonempty side).weight seed = if exactReverseLeftSide seed = side then exactSeedWeight seed else 0
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedLaw_weight_cancel
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(side : Finset M)
(seed : ExactForwardSeed M)
:
reversePartitionWeight side * (exactReverseBobConditionalSeedLaw nonempty side).weight seed = if exactReverseRightSide seed = side then exactSeedWeight seed else 0
noncomputable def
QuantumParallelRepetition.exactReverseSideContextWeight
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{side : Finset M}
(context : ExactReverseSideContext M side)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight_eq_context_div_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(seed : ExactForwardSeed M)
:
theorem
QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_eq_context_div_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(seed : ExactForwardSeed M)
:
exactReverseBobConditionalSeedWeight (exactReverseRightSide seed) seed = exactReverseSideContextWeight (exactReverseBobContext seed) / ↑(exactReverseRightSide seed).card
noncomputable def
QuantumParallelRepetition.exactReverseAliceMarkerCode
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
(side : Finset M) × ExactReverseSideContext M side × Fin side.card
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobMarkerCode
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
(side : Finset M) × ExactReverseSideContext M side × Fin side.card
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceMarkerCode_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
↑((exactReverseAliceMarkerCode seed).snd.1.sideRank.symm (exactReverseAliceMarkerCode seed).snd.2) = seed.coordinate
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobMarkerCode_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(seed : ExactForwardSeed M)
:
↑((exactReverseBobMarkerCode seed).snd.1.sideRank.symm (exactReverseBobMarkerCode seed).snd.2) = seed.coordinate
theorem
QuantumParallelRepetition.exactReverseAliceMarkerCode_coordinate_injective
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{a b : ExactForwardSeed M}
(same : exactReverseAliceMarkerCode a = exactReverseAliceMarkerCode b)
:
theorem
QuantumParallelRepetition.exactReverseBobMarkerCode_coordinate_injective
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{a b : ExactForwardSeed M}
(same : exactReverseBobMarkerCode a = exactReverseBobMarkerCode b)
:
theorem
QuantumParallelRepetition.exactReverseAliceMarkerCode_partition_injective
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{a b : ExactForwardSeed M}
(same : exactReverseAliceMarkerCode a = exactReverseAliceMarkerCode b)
:
theorem
QuantumParallelRepetition.exactReverseBobMarkerCode_partition_injective
{M : Type u_1}
[Fintype M]
[DecidableEq M]
{a b : ExactForwardSeed M}
(same : exactReverseBobMarkerCode a = exactReverseBobMarkerCode b)
:
def
QuantumParallelRepetition.exactDeleteMarkedRank
{M : Type u_1}
[DecidableEq M]
(i : M)
(side : Finset M)
(not_mem : i ∉ side)
(rank : ↥(insert i side) ≃ Fin (side.card + 1))
(cut : Fin (side.card + 1))
(marked : rank ⟨i, ⋯⟩ = cut)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactPermutationOfSideRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(rank : ↥side ≃ Fin side.card)
:
Equiv.Perm ↥side
Equations
Instances For
theorem
QuantumParallelRepetition.exactPermutationOfSideRank_rank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(rank : ↥side ≃ Fin side.card)
:
theorem
QuantumParallelRepetition.exactReverseAliceCanonicalPartition_otherSide
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
exactRight coordinate (exactReverseAliceCanonicalPartition side coordinate ignored) = Finset.univ \ side
theorem
QuantumParallelRepetition.exactReverseBobCanonicalPartition_otherSide
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
exactLeft coordinate (exactReverseBobCanonicalPartition side coordinate ignored) = Finset.univ \ side
theorem
QuantumParallelRepetition.exactReverseAliceCanonicalPartition_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
theorem
QuantumParallelRepetition.exactReverseBobCanonicalPartition_card
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(coordinate : M)
(member : coordinate ∈ side)
(ignored : Bool)
:
(exactRight coordinate (exactReverseBobCanonicalPartition side coordinate ignored)).card + 1 = side.card
noncomputable def
QuantumParallelRepetition.exactReverseAliceMarkerDecode
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobMarkerDecode
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_coordinate
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_side
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_side
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
@[simp]
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_ignoredBit
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
(exactReverseAliceMarkerDecode side context marker).partition
(exactReverseAliceMarkerDecode side context marker).coordinate = context.ignoredBit
@[simp]
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_ignoredBit
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
(exactReverseBobMarkerDecode side context marker).partition
(exactReverseBobMarkerDecode side context marker).coordinate = context.ignoredBit
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_otherRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactRight (exactReverseAliceMarkerDecode side context marker).coordinate
(exactReverseAliceMarkerDecode side context marker).partition,
exactRightRank (exactReverseAliceMarkerDecode side context marker)⟩ = ⟨context.otherSide, context.otherRank⟩
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_otherCut
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactRight (exactReverseAliceMarkerDecode side context marker).coordinate
(exactReverseAliceMarkerDecode side context marker).partition,
(exactReverseAliceMarkerDecode side context marker).rightCut⟩ = ⟨context.otherSide, context.otherCut⟩
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_sideRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactReverseLeftSide (exactReverseAliceMarkerDecode side context marker),
(exactReverseAliceContext (exactReverseAliceMarkerDecode side context marker)).sideRank⟩ = ⟨side, context.sideRank⟩
theorem
QuantumParallelRepetition.exactReverseAliceMarkerDecode_rightInverse
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
exactReverseAliceMarkerCode (exactReverseAliceMarkerDecode side context marker) = ⟨side, (context, marker)⟩
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_otherRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactLeft (exactReverseBobMarkerDecode side context marker).coordinate
(exactReverseBobMarkerDecode side context marker).partition,
exactLeftRank (exactReverseBobMarkerDecode side context marker)⟩ = ⟨context.otherSide, context.otherRank⟩
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_otherCut
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactLeft (exactReverseBobMarkerDecode side context marker).coordinate
(exactReverseBobMarkerDecode side context marker).partition,
(exactReverseBobMarkerDecode side context marker).leftCut⟩ = ⟨context.otherSide, context.otherCut⟩
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_sideRank
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
⟨exactReverseRightSide (exactReverseBobMarkerDecode side context marker),
(exactReverseBobContext (exactReverseBobMarkerDecode side context marker)).sideRank⟩ = ⟨side, context.sideRank⟩
theorem
QuantumParallelRepetition.exactReverseBobMarkerDecode_rightInverse
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(side : Finset M)
(context : ExactReverseSideContext M side)
(marker : Fin side.card)
:
exactReverseBobMarkerCode (exactReverseBobMarkerDecode side context marker) = ⟨side, (context, marker)⟩
noncomputable def
QuantumParallelRepetition.exactReverseAliceWeightedMarkerEquiv
{M : Type u_1}
[Fintype M]
[DecidableEq M]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactReverseBobWeightedMarkerEquiv
{M : Type u_1}
[Fintype M]
[DecidableEq M]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactReverseAliceOriginalSeedWeight_factor
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(seed : ExactForwardSeed M)
:
exactSeedWeight seed = reversePartitionWeight (exactReverseLeftSide seed) * (exactReverseSideContextWeight (exactReverseAliceContext seed) / ↑(exactReverseLeftSide seed).card)
theorem
QuantumParallelRepetition.exactReverseBobOriginalSeedWeight_factor
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(seed : ExactForwardSeed M)
:
exactSeedWeight seed = reversePartitionWeight (exactReverseRightSide seed) * (exactReverseSideContextWeight (exactReverseBobContext seed) / ↑(exactReverseRightSide seed).card)
theorem
QuantumParallelRepetition.exactReverseAliceUniformMarkedSeed_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(statistic : (side : Finset M) → ExactReverseSideContext M side → Fin side.card → ℝ)
:
∑ seed : ExactForwardSeed M,
exactSeedWeight seed * ((∑ marker : Fin (exactReverseLeftSide seed).card,
statistic (exactReverseLeftSide seed) (exactReverseAliceContext seed) marker) / ↑(exactReverseLeftSide seed).card) = ∑ seed : ExactForwardSeed M,
exactSeedWeight seed * statistic (exactReverseLeftSide seed) (exactReverseAliceContext seed)
((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩)
theorem
QuantumParallelRepetition.exactReverseBobUniformMarkedSeed_sum
{M : Type u_1}
[Fintype M]
[DecidableEq M]
(nonempty : 0 < Fintype.card M)
(statistic : (side : Finset M) → ExactReverseSideContext M side → Fin side.card → ℝ)
:
∑ seed : ExactForwardSeed M,
exactSeedWeight seed * ((∑ marker : Fin (exactReverseRightSide seed).card,
statistic (exactReverseRightSide seed) (exactReverseBobContext seed) marker) / ↑(exactReverseRightSide seed).card) = ∑ seed : ExactForwardSeed M,
exactSeedWeight seed * statistic (exactReverseRightSide seed) (exactReverseBobContext seed)
((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩)
noncomputable def
QuantumParallelRepetition.exactReverseAliceFilterOperatorMarkerEntropy
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactReverseBobFilterOperatorMarkerEntropy
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactFairAliceOperatorEntropy_reverse_marked_average
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < Fintype.card (SourceRemainingCoordinate D))
:
(∑ r : ExactHistoryFlag X Y A B D,
if exactHistoryAccepted G n D r then
exactFairHistoryPriorWeight G n D r * exactFairAliceHistoryEntropyIncrement G n S D r
else 0) = ∑ seed : ExactRemainingSeed D,
exactSeedWeight seed * ((∑ marker : Fin (exactReverseRightSide seed).card,
exactReverseAliceFilterOperatorMarkerEntropy G n S D (exactReverseRightSide seed)
(exactReverseBobContext seed) marker) / ↑(exactReverseRightSide seed).card)
theorem
QuantumParallelRepetition.exactFairBobOperatorEntropy_reverse_marked_average
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < Fintype.card (SourceRemainingCoordinate D))
:
(∑ r : ExactHistoryFlag X Y A B D,
if exactHistoryAccepted G n D r then
exactFairHistoryPriorWeight G n D r * exactFairBobHistoryEntropyIncrement G n S D r
else 0) = ∑ seed : ExactRemainingSeed D,
exactSeedWeight seed * ((∑ marker : Fin (exactReverseLeftSide seed).card,
exactReverseBobFilterOperatorMarkerEntropy G n S D (exactReverseLeftSide seed) (exactReverseAliceContext seed)
marker) / ↑(exactReverseLeftSide seed).card)
noncomputable def
QuantumParallelRepetition.exactFairAliceHistoryHighOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairAliceHistoryLowOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobHistoryHighOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.exactFairBobHistoryLowOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairAliceHistoryEntropy_eq_operatorPotential_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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairAliceHistoryEntropyIncrement G n S D r = exactFairAliceHistoryHighOperatorPotential G n S D r - exactFairAliceHistoryLowOperatorPotential G n S D r
theorem
QuantumParallelRepetition.exactFairBobHistoryEntropy_eq_operatorPotential_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))
(r : ExactHistoryFlag X Y A B D)
:
exactFairBobHistoryEntropyIncrement G n S D r = exactFairBobHistoryHighOperatorPotential G n S D r - exactFairBobHistoryLowOperatorPotential G n S D r
noncomputable def
QuantumParallelRepetition.exactReverseAliceFilterHighOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactReverseAliceFilterLowOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactReverseBobFilterHighOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactReverseBobFilterLowOperatorPotential
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactReverseAliceFilterOperatorMarkerEntropy_eq_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 = exactReverseAliceFilterHighOperatorPotential G n S D side context marker - exactReverseAliceFilterLowOperatorPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactReverseBobFilterOperatorMarkerEntropy_eq_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 = exactReverseBobFilterHighOperatorPotential G n S D side context marker - exactReverseBobFilterLowOperatorPotential G n S D side context marker
theorem
QuantumParallelRepetition.exactFixedQuestionPrefix_insert_iff
{T : Type u_5}
[DecidableEq T]
{n : ℕ}
(fixed : Finset (Fin n))
(j : Fin n)
(fresh : j ∉ fixed)
(candidate known : Fin n → T)
(value : T)
:
theorem
QuantumParallelRepetition.exactRevealCode_splitAt_independent
{X : Type u_1}
{Y : Type u_2}
[Fintype X]
[Fintype Y]
{n : ℕ}
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(x x' : X)
(y y' : Y)
(tailX : { j : Fin n // j ≠ ↑seed.coordinate } → X)
(tailY : { j : Fin n // j ≠ ↑seed.coordinate } → Y)
:
exactRevealCode D seed
((Equiv.funSplitAt (↑seed.coordinate) X).symm (x, tailX), (Equiv.funSplitAt (↑seed.coordinate) Y).symm (y, tailY)) = exactRevealCode D seed
((Equiv.funSplitAt (↑seed.coordinate) X).symm (x', tailX), (Equiv.funSplitAt (↑seed.coordinate) Y).symm (y', tailY))
theorem
QuantumParallelRepetition.exactRepeatedQuestionWeight_splitAt_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 : ℕ)
(i : Fin n)
(x : X)
(y : Y)
(tailX : { j : Fin n // j ≠ i } → X)
(tailY : { j : Fin n // j ≠ i } → Y)
:
(G.repeat n).questionWeight ((Equiv.funSplitAt i X).symm (x, tailX)) ((Equiv.funSplitAt i Y).symm (y, tailY)) = G.questionWeight x y * ∏ j : { j : Fin n // j ≠ i }, G.questionWeight (tailX j) (tailY j)
noncomputable def
QuantumParallelRepetition.exactFairQuestionTailWeight
{X : Type u_1}
{Y : Type u_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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairQuestionTailWeight_independent
{X : Type u_1}
{Y : Type u_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' : X)
(y y' : Y)
:
exactFairQuestionTailWeight G n D seed history x y = exactFairQuestionTailWeight G n D seed history x' y'
theorem
QuantumParallelRepetition.exactJointQuestionMass_eq_question_mul_tail
{X : Type u_1}
{Y : Type u_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 = G.questionWeight x y * exactFairQuestionTailWeight G n D seed history x y
theorem
QuantumParallelRepetition.exactJointQuestionMass_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, ∑ y : Y, exactJointQuestionMass G n D seed history x y = exactRevealMass G n D seed history
theorem
QuantumParallelRepetition.exactJointQuestionMass_eq_reveal_mul_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 : ℕ)
(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 = exactRevealMass G n D seed history * G.questionWeight x y
noncomputable def
QuantumParallelRepetition.exactFairConditionedAnswerBornMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFiberQuestionWeight_eq_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 : ℕ)
(D : Finset (Fin n))
(seed : ExactRemainingSeed D)
(history : ExactRevealHistory X Y D seed)
(x : X)
(y : Y)
(zero : exactFiberQuestionMass G n D seed history x y = 0)
(xs : Fin n → X)
(ys : Fin n → Y)
:
theorem
QuantumParallelRepetition.exactFairConditionedAnswerBornMass_eq_fiber_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)
:
exactFairConditionedAnswerBornMass G n S D r x y = exactFiberQuestionMass G n D r.seed r.history x y * ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2
theorem
QuantumParallelRepetition.exactFairConditionedAnswerBornMass_eq_reveal_question_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)
:
exactFairConditionedAnswerBornMass G n S D r x y = exactRevealMass G n D r.seed r.history * G.questionWeight x y * ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2
theorem
QuantumParallelRepetition.exactLocallySampleableCode_fixedSeed_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))
(r : ExactHistoryFlag X Y A B D)
(x : X)
(y : Y)
(o : ExactOutcome X Y A B n)
:
noncomputable def
QuantumParallelRepetition.exactFairFullOutcomeBornMass
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.exactFairFullOutcomeBornMass_eq_conditioned
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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.exactFairFullOutcomeBornMass_eq_reveal_question_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)
:
exactFairFullOutcomeBornMass G n S D r x y = exactRevealMass G n D r.seed r.history * G.questionWeight x y * ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2
theorem
QuantumParallelRepetition.exactLocallySampleableLaw_eq_fair_born
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(r : ExactHistoryFlag X Y A B D)
(x : X)
(y : Y)
:
exactLocallySampleableLaw G n S D (r.seed.coordinate, x, y, r) = if exactHistoryAccepted G n D r then
exactSeedWeight r.seed * exactRevealMass G n D r.seed r.history * G.questionWeight x y * ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2 / repeatedPostselectionMass G n S D
else 0