Quantum parallel repetition, part 05

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

The total probability mass of exact fixed bob question.

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

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

The total probability mass of exact fixed alice question.

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

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

The exact reverse left side construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactReverseLeftSide seed = insert seed.coordinate (QuantumParallelRepetition.exactLeft seed.coordinate seed.partition)

def QuantumParallelRepetition.exactReverseRightSide {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : Finset M

The exact reverse right side construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactReverseRightSide seed = insert seed.coordinate (QuantumParallelRepetition.exactRight seed.coordinate seed.partition)

@[simp]

theorem QuantumParallelRepetition.exactReverseLeftSide_coordinate_mem {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : seed.coordinate ∈ exactReverseLeftSide seed

@[simp]

theorem QuantumParallelRepetition.exactReverseRightSide_coordinate_mem {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : seed.coordinate ∈ exactReverseRightSide seed

theorem QuantumParallelRepetition.exactReverseLeftSide_card {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (exactReverseLeftSide seed).card = (exactLeft seed.coordinate seed.partition).card + 1

theorem QuantumParallelRepetition.exactReverseRightSide_card {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (exactReverseRightSide seed).card = (exactRight seed.coordinate seed.partition).card + 1

theorem QuantumParallelRepetition.exactReverseLeftSide_markedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : reverseMarkedPartitionWeight (exactReverseLeftSide seed) seed.coordinate = forwardMarkedPartitionWeight M

theorem QuantumParallelRepetition.exactReverseRightSide_markedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : reverseMarkedPartitionWeight (exactReverseRightSide seed) seed.coordinate = forwardMarkedPartitionWeight 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

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)

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

The exact history accepted construction used in the quantum parallel-repetition argument.

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

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) : exactLocallySampleableLaw G n S D (i, x, y, r) = 0

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

The type used to represent exact global history local index in the exact sampling construction.

Equations

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

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)

The state vector representing exact global history.

Equations

• QuantumParallelRepetition.exactGlobalHistoryVector G n S D r z = QuantumParallelRepetition.taggedTensorVector r z

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)) : ‖exactGlobalHistoryVector G n S D r z‖ = ‖z‖

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

theorem QuantumParallelRepetition.exactGlobalHistoryLocalIndex_card_pos {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D)

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

The exact global history fin reindex construction used in the quantum parallel-repetition argument.

Equations

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

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) : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

The exact global history fin gamma construction used in the quantum parallel-repetition argument.

Equations

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

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) : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

The exact global history fin phi construction used in the quantum parallel-repetition argument.

Equations

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

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) : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))

The exact global history fin psi construction used in the quantum parallel-repetition argument.

Equations

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

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

The type used to represent exact source global state in the exact sampling construction.

Equations

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

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

The exact source tuple psi construction used in the quantum parallel-repetition argument.

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)

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

The exact source tuple gamma construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactSourceTupleGamma G n S D t = ↑(QuantumParallelRepetition.exactGlobalHistoryFinGamma G n S D t.2.2.2 t.2.1)

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

The exact source tuple phi construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactSourceTuplePhi G n S D t = ↑(QuantumParallelRepetition.exactGlobalHistoryFinPhi G n S D t.2.2.2 t.2.2.1)

theorem QuantumParallelRepetition.exactSourceTuplePsi_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)) (t : ExactLocallySampleableTuple X Y A B D) : ‖exactSourceTuplePsi G n S D t‖ = 1

theorem QuantumParallelRepetition.exactSourceTupleGamma_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)) (t : ExactLocallySampleableTuple X Y A B D) : ‖exactSourceTupleGamma G n S D t‖ = 1

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)) (η : ℝ) : Prop

The numerical bound for exact source state distance.

Equations

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

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) : ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2 * ‖exactPsi G n S D r x y - exactPhi G n S D r y‖ ^ 2 ≤ 4 * ‖exactUnnormalizedPsi G n S D r x y - exactUnnormalizedPhi G n S D r y‖ ^ 2

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

The information increment contributed by exact fair alice history entropy.

Equations

• QuantumParallelRepetition.exactFairAliceHistoryEntropyIncrement G n S D r = ∑ y : Y, G.marginalY y * QuantumParallelRepetition.exactFairAliceQuestionEntropyIncrement✝ G n S D r y

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

The information increment contributed by exact fair bob history entropy.

Equations

• QuantumParallelRepetition.exactFairBobHistoryEntropyIncrement G n S D r = ∑ x : X, G.marginalX x * QuantumParallelRepetition.exactFairBobQuestionEntropyIncrement✝ G n S D r x

noncomputable def QuantumParallelRepetition.exactFairHistoryPriorWeight {X : Type u_1} {Y : Type u_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) : ℝ

The probability weight for exact fair history prior.

Equations

• QuantumParallelRepetition.exactFairHistoryPriorWeight G n D r = QuantumParallelRepetition.exactSeedWeight r.seed * QuantumParallelRepetition.exactRevealMass G n D r.seed r.history

theorem QuantumParallelRepetition.exactFairHistoryPriorWeight_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)) (r : ExactHistoryFlag X Y A B D) : 0 ≤ exactFairHistoryPriorWeight G n D r

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

The error rate associated with exact source classical information.

Equations

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

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

The numerical bound for exact source classical information.

Equations

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

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

The finite equivalence encoding exact alice information.

Equations

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

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

The finite equivalence encoding exact bob information.

Equations

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

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

The exact alice information posterior construction used in the quantum parallel-repetition argument.

Equations

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

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

The exact alice information reference construction used in the quantum parallel-repetition argument.

Equations

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

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

The exact bob information posterior construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactBobInformationPosterior G n S D t = QuantumParallelRepetition.exactLocallySampleableLaw G n S D ((QuantumParallelRepetition.exactBobInformationEquiv D).symm t)

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

The exact bob information reference construction used in the quantum parallel-repetition argument.

Equations

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

theorem QuantumParallelRepetition.exact_source_equation_twenty_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)

noncomputable def QuantumParallelRepetition.exactSourcePinskerRate {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The error rate associated with exact source pinsker.

Equations

• QuantumParallelRepetition.exactSourcePinskerRate G n S D = √(QuantumParallelRepetition.exactSourceClassicalInformationRate G n S D / 2)

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.exactSourcePrefixFlagEquiv {Ω : Type u_5} {V : Type u_6} {Z : Type u_7} {h : ℕ} : (Ω × (Fin h → V)) × Z ≃ (Ω × Z) × (Fin h → V)

The finite equivalence encoding exact source prefix flag.

Equations

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

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

The marginal distribution of exact alice question prior.

Equations

• QuantumParallelRepetition.exactAliceQuestionPriorMarginal G x = ∑ y : Y, G.questionWeight x y

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

The marginal distribution of exact bob question prior.

Equations

• QuantumParallelRepetition.exactBobQuestionPriorMarginal G y = ∑ x : X, G.questionWeight x y

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 : Ω → ℝ) : ClassicalInformation.groupedMass projection mass = ClassicalInformation.groupedMass projection mass

theorem QuantumParallelRepetition.exactGroupedMass_congr {Ω : Type u_5} {κ : Type u_6} [Fintype Ω] (first second : DecidableEq κ) (projection₁ projection₂ : Ω → κ) (mass₁ mass₂ : Ω → ℝ) (projection_eq : projection₁ = projection₂) (mass_eq : mass₁ = mass₂) : ClassicalInformation.groupedMass projection₁ mass₁ = ClassicalInformation.groupedMass projection₂ mass₂

Grouped masses agree when their projections and source weights agree, independently of the chosen decidable-equality implementations on the target.

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

The exact alice source marginal information construction used in the quantum parallel-repetition argument.

Equations

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

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

The exact bob source marginal information construction used in the quantum parallel-repetition argument.

Equations

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

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

The exact alice source conditional information construction used in the quantum parallel- repetition argument.

Equations

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

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

The exact bob source conditional information construction used in the quantum parallel- repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseLeftRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactReverseLeftSide seed) ≃ Fin ((exactLeft seed.coordinate seed.partition).card + 1)

The rank map for exact reverse left.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseRightRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactReverseRightSide seed) ≃ Fin ((exactRight seed.coordinate seed.partition).card + 1)

The rank map for exact reverse right.

Equations

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

@[simp]

theorem QuantumParallelRepetition.exactReverseLeftRank_coordinate {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (exactReverseLeftRank seed) ⟨seed.coordinate, ⋯⟩ = seed.leftCut

@[simp]

theorem QuantumParallelRepetition.exactReverseRightRank_coordinate {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (exactReverseRightRank seed) ⟨seed.coordinate, ⋯⟩ = seed.rightCut

theorem QuantumParallelRepetition.exactReverseLeftRank_old {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) (j : ↥(exactLeft seed.coordinate seed.partition)) : (exactReverseLeftRank seed) ⟨↑j, ⋯⟩ = seed.leftCut.succAbove ((exactLeftRank seed) j)

theorem QuantumParallelRepetition.exactReverseRightRank_old {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) (j : ↥(exactRight seed.coordinate seed.partition)) : (exactReverseRightRank seed) ⟨↑j, ⋯⟩ = seed.rightCut.succAbove ((exactRightRank seed) j)

def QuantumParallelRepetition.exactOrderedSidePrefix {M : Type u_1} [DecidableEq M] (side : Finset M) (rank : ↥side ≃ Fin side.card) (cut : Fin (side.card + 1)) : Finset M

The exact ordered side prefix construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactOrderedSidePrefix side rank cut = Finset.image Subtype.val {j : ↥side | ↑(rank j) < ↑cut}

theorem QuantumParallelRepetition.exactOrderedSidePrefix_mem_iff {M : Type u_1} [DecidableEq M] (side : Finset M) (rank : ↥side ≃ Fin side.card) (cut : Fin (side.card + 1)) (j : M) : j ∈ exactOrderedSidePrefix side rank cut ↔ ∃ (hj : j ∈ side), ↑(rank ⟨j, hj⟩) < ↑cut

structure QuantumParallelRepetition.ExactReverseSideContext (M : Type u_1) [Fintype M] [DecidableEq M] (side : Finset M) : Type u_1

The information retained when decoding one side of a reverse seed.

• otherSide : Finset M

  The coordinates on the opposite side of the partition.

• sideRank : ↥side ≃ Fin side.card

  The rank equivalence for the decoded side.

• otherRank : ↥self.otherSide ≃ Fin self.otherSide.card

  The rank equivalence for the opposite side.

• otherCut : Fin (self.otherSide.card + 1)

  The reveal cut on the opposite side.

• ignoredBit : Bool

  The partition bit omitted by the reverse encoding.

• otherSide_eq_complement : self.otherSide = Finset.univ \ side

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

The exact reverse context other prefix construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactReverseContextOtherPrefix context = QuantumParallelRepetition.exactOrderedSidePrefix context.otherSide context.otherRank context.otherCut

theorem QuantumParallelRepetition.exactReverseLeftSide_complement {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactRight seed.coordinate seed.partition = Finset.univ \ exactReverseLeftSide seed

theorem QuantumParallelRepetition.exactReverseRightSide_complement {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactLeft seed.coordinate seed.partition = Finset.univ \ exactReverseRightSide seed

noncomputable def QuantumParallelRepetition.exactReverseAliceContext {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ExactReverseSideContext M (exactReverseLeftSide seed)

The data context recording exact reverse alice.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobContext {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ExactReverseSideContext M (exactReverseRightSide seed)

The data context recording exact reverse bob.

Equations

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

noncomputable def QuantumParallelRepetition.exactDefaultReverseSideContext {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) : ExactReverseSideContext M side

The data context recording exact default reverse side.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseAliceContextAt {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : ExactReverseSideContext M side

The exact reverse alice context at construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobContextAt {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : ExactReverseSideContext M side

The exact reverse bob context at construction used in the quantum parallel-repetition argument.

Equations

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

@[simp]

theorem QuantumParallelRepetition.exactReverseAliceContextAt_actual {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactReverseAliceContextAt (exactReverseLeftSide seed) seed = exactReverseAliceContext seed

@[simp]

theorem QuantumParallelRepetition.exactReverseBobContextAt_actual {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactReverseBobContextAt (exactReverseRightSide seed) seed = exactReverseBobContext seed

@[simp]

theorem QuantumParallelRepetition.exactReverseAliceContext_otherPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactReverseContextOtherPrefix (exactReverseAliceContext seed) = exactRightPrefix seed

@[simp]

theorem QuantumParallelRepetition.exactReverseBobContext_otherPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactReverseContextOtherPrefix (exactReverseBobContext seed) = exactLeftPrefix seed

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactReverseAliceFixedInformation (X : Type u_5) (Y : Type u_6) {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max u_5 u_6)

The type used to represent exact reverse alice fixed information in the exact sampling construction.

Equations

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

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactReverseBobFixedInformation (X : Type u_5) (Y : Type u_6) {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : Type (max u_6 u_5)

The type used to represent exact reverse bob fixed information in the exact sampling construction.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseAliceSourceProjection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : ExactJointOutcome X Y A B D → ExactReverseAliceFixedInformation X Y D side × (Fin side.card → Y)

The projection associated with exact reverse alice source.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobSourceProjection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {n : ℕ} (D : Finset (Fin n)) (side : Finset (SourceRemainingCoordinate D)) : ExactJointOutcome X Y A B D → ExactReverseBobFixedInformation X Y D side × (Fin side.card → X)

The projection associated with exact reverse bob source.

Equations

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

@[simp]

theorem QuantumParallelRepetition.exactReverseAliceContext_marked_rank {M : Type u_5} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↑((exactReverseAliceContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = ↑seed.leftCut

@[simp]

theorem QuantumParallelRepetition.exactReverseBobContext_marked_rank {M : Type u_5} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↑((exactReverseBobContext seed).sideRank ⟨seed.coordinate, ⋯⟩) = ↑seed.rightCut

def QuantumParallelRepetition.exactReverseContextPrefixBefore {M : Type u_5} [Fintype M] [DecidableEq M] {side : Finset M} (context : ExactReverseSideContext M side) (position : Fin side.card) : Finset M

The exact reverse context prefix before construction used in the quantum parallel-repetition argument.

Equations

• QuantumParallelRepetition.exactReverseContextPrefixBefore context position = QuantumParallelRepetition.exactOrderedSidePrefix side context.sideRank position.castSucc

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) : Ω × (Fin h → V) → (Ω × (Fin h → V)) × V

The finite encoding of exact prefix next.

Equations

• QuantumParallelRepetition.exactPrefixNextCode default k t = (QuantumParallelRepetition.finitePrefixMask default k.castSucc t, t.2 k)

theorem QuantumParallelRepetition.exactPrefixNextCode_comp {Ω : Type u_1} {V : Type u_2} {h : ℕ} (default : V) (k : Fin h) : exactPrefixNextCode default k ∘ finitePrefixMask default k.succ = exactPrefixNextCode default k

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)

theorem QuantumParallelRepetition.exactReverseAlicePartitionFiber_card {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (coordinate : M) (member : coordinate ∈ side) : Fintype.card { partition : M → Bool // insert coordinate (exactLeft coordinate partition) = side } = 2

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.exactFiniteIndicator_sum {T : Type u_1} [Fintype T] (predicate : T → Prop) [DecidablePred predicate] (weight : ℝ) : (∑ t : T, if predicate t then weight else 0) = ↑(Fintype.card { t : T // predicate t }) * weight

theorem QuantumParallelRepetition.exactReverseAlicePartitionFiber_sum {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (coordinate : M) (member : coordinate ∈ side) (weight : ℝ) : (∑ partition : M → Bool, if insert coordinate (exactLeft coordinate partition) = side then weight else 0) = 2 * weight

theorem QuantumParallelRepetition.exactReverseBobPartitionFiber_sum {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (coordinate : M) (member : coordinate ∈ side) (weight : ℝ) : (∑ partition : M → Bool, if insert coordinate (exactRight coordinate partition) = side then weight else 0) = 2 * 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) : ClassicalInformation.groupedMass exactReverseLeftSide exactSeedWeight side = reversePartitionWeight side

theorem QuantumParallelRepetition.exactReverseBobSide_marginal {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) : ClassicalInformation.groupedMass exactReverseRightSide exactSeedWeight side = reversePartitionWeight side

noncomputable def QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : ℝ

The probability weight for exact reverse alice conditional seed.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobConditionalSeedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : ℝ

The probability weight for exact reverse bob conditional seed.

Equations

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

theorem QuantumParallelRepetition.exactReverseAliceConditionalSeedWeight_nonneg {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : 0 ≤ exactReverseAliceConditionalSeedWeight side seed

theorem QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_nonneg {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (seed : ExactForwardSeed M) : 0 ≤ exactReverseBobConditionalSeedWeight side seed

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) : ∑ seed : ExactForwardSeed M, exactReverseAliceConditionalSeedWeight side seed = 1

theorem QuantumParallelRepetition.exactReverseBobConditionalSeedWeight_sum {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (nonempty : side.Nonempty) : ∑ seed : ExactForwardSeed M, exactReverseBobConditionalSeedWeight side seed = 1

noncomputable def QuantumParallelRepetition.exactReverseAliceConditionalSeedLaw {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (side : Finset M) : FiniteEventLaw (ExactForwardSeed M)

The finite probability law for exact reverse alice conditional seed.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobConditionalSeedLaw {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (side : Finset M) : FiniteEventLaw (ExactForwardSeed M)

The finite probability law for exact reverse bob conditional seed.

Equations

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

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

The finite probability law for reweighted seed prior event.

Equations

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

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)

The reweighted seed win event construction used in the quantum parallel-repetition argument.

Equations

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

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

The reweighted seed posterior construction used in the quantum parallel-repetition argument.

Equations

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

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] (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) : U × Z → ℝ

The finite probability law for reweighted seed flagged projection.

Equations

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

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] [Finite 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] {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) → ℝ

The reweighted seed prefix joint construction used in the quantum parallel-repetition argument.

Equations

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

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] {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) → ℝ

The reweighted seed prefix prior construction used in the quantum parallel-repetition argument.

Equations

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

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] {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)) : 0 ≤ reweightedSeedPrefixJoint seedLaw G n S D projection t

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] {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)) : 0 ≤ reweightedSeedPrefixPrior seedLaw G n S D projection t

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

The information increment contributed by reweighted seed prefix entropy.

Equations

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

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] [Finite Ω] [Finite 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.exactReverseAliceMarkerCode {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (side : Finset M) × ExactReverseSideContext M side × Fin side.card

The finite encoding of exact reverse alice marker.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobMarkerCode {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : (side : Finset M) × ExactReverseSideContext M side × Fin side.card

The finite encoding of exact reverse bob marker.

Equations

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

@[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) : a.coordinate = b.coordinate

theorem QuantumParallelRepetition.exactReverseBobMarkerCode_coordinate_injective {M : Type u_1} [Fintype M] [DecidableEq M] {a b : ExactForwardSeed M} (same : exactReverseBobMarkerCode a = exactReverseBobMarkerCode b) : a.coordinate = b.coordinate

theorem QuantumParallelRepetition.exactReverseAliceMarkerCode_partition_injective {M : Type u_1} [Fintype M] [DecidableEq M] {a b : ExactForwardSeed M} (same : exactReverseAliceMarkerCode a = exactReverseAliceMarkerCode b) : a.partition = b.partition

theorem QuantumParallelRepetition.exactReverseBobMarkerCode_partition_injective {M : Type u_1} [Fintype M] [DecidableEq M] {a b : ExactForwardSeed M} (same : exactReverseBobMarkerCode a = exactReverseBobMarkerCode b) : a.partition = b.partition

theorem QuantumParallelRepetition.exactReverseAliceMarkerCode_injective {M : Type u_1} [Fintype M] [DecidableEq M] : Function.Injective exactReverseAliceMarkerCode

theorem QuantumParallelRepetition.exactReverseBobMarkerCode_injective {M : Type u_1} [Fintype M] [DecidableEq M] : Function.Injective exactReverseBobMarkerCode

noncomputable def QuantumParallelRepetition.exactReverseAliceMarkerDecode {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : ExactForwardSeed M

The exact reverse alice marker decode construction used in the quantum parallel-repetition argument.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobMarkerDecode {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : ExactForwardSeed M

The exact reverse bob marker decode construction used in the quantum parallel-repetition argument.

Equations

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

@[simp]

theorem QuantumParallelRepetition.exactReverseAliceMarkerDecode_coordinate {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : (exactReverseAliceMarkerDecode side context marker).coordinate = ↑(context.sideRank.symm marker)

@[simp]

theorem QuantumParallelRepetition.exactReverseBobMarkerDecode_coordinate {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : (exactReverseBobMarkerDecode side context marker).coordinate = ↑(context.sideRank.symm marker)

@[simp]

theorem QuantumParallelRepetition.exactReverseAliceMarkerDecode_side {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : exactReverseLeftSide (exactReverseAliceMarkerDecode side context marker) = side

@[simp]

theorem QuantumParallelRepetition.exactReverseBobMarkerDecode_side {M : Type u_1} [Fintype M] [DecidableEq M] (side : Finset M) (context : ExactReverseSideContext M side) (marker : Fin side.card) : exactReverseRightSide (exactReverseBobMarkerDecode side context marker) = side

@[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 ↑(context.sideRank.symm marker) = 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 ↑(context.sideRank.symm marker) = context.ignoredBit

theorem QuantumParallelRepetition.exactSigmaFinCutTransport {M : Type u_1} (source target : Finset M) (same : source = target) (cut : Fin (target.card + 1)) : ⟨source, (finCongr ⋯) cut⟩ = ⟨target, cut⟩

theorem QuantumParallelRepetition.exactSigmaSideRankTransport {M : Type u_1} (source target : Finset M) (same : source = target) (rank : ↥target ≃ Fin target.card) : ⟨source, (Equiv.subtypeEquivRight ⋯).trans (rank.trans (finCongr ⋯))⟩ = ⟨target, rank⟩

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] : ExactForwardSeed M ≃ (side : Finset M) × ExactReverseSideContext M side × Fin side.card

The finite equivalence encoding exact reverse alice weighted marker.

Equations

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

noncomputable def QuantumParallelRepetition.exactReverseBobWeightedMarkerEquiv {M : Type u_1} [Fintype M] [DecidableEq M] : ExactForwardSeed M ≃ (side : Finset M) × ExactReverseSideContext M side × Fin side.card

The finite equivalence encoding exact reverse bob weighted marker.

Equations

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

theorem QuantumParallelRepetition.exactUniformFiniteMarkedAverage_sum (n : ℕ) (weight : ℝ) (statistic : Fin n → ℝ) : ∑ _marker : Fin n, weight * ((∑ position : Fin n, statistic position) / ↑n) = ∑ marker : Fin n, weight * statistic marker

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

The entropy quantity for exact reverse alice filter operator marker.

Equations

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

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

The entropy quantity for exact reverse bob filter operator marker.

Equations

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

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

The potential function controlling exact fair alice history high operator.

Equations

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

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

The potential function controlling exact fair alice history low operator.

Equations

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

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

The potential function controlling exact fair bob history high operator.

Equations

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

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

The potential function controlling exact fair bob history low operator.

Equations

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

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

The potential function controlling exact reverse alice filter high operator.

Equations

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

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

The potential function controlling exact reverse alice filter low operator.

Equations

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

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

The potential function controlling exact reverse bob filter high operator.

Equations

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

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

The potential function controlling exact reverse bob filter low operator.

Equations

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

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} {n : ℕ} (fixed : Finset (Fin n)) (j : Fin n) (fresh : j ∉ fixed) (candidate known : Fin n → T) (value : T) : (∀ k ∈ insert j fixed, candidate k = Function.update known j value k) ↔ candidate j = value ∧ ∀ k ∈ fixed, candidate k = known k

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)

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

The total probability mass of exact fair conditioned answer born.

Equations

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

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) : exactFiberQuestionWeight G n D seed history x y xs ys = 0

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) : exactLocallySampleableCode D (r.seed, o) = (r.seed.coordinate, x, y, r) ↔ exactRevealCode D r.seed (o.1, o.2.1) = r.history ∧ o.1 ↑r.seed.coordinate = x ∧ o.2.1 ↑r.seed.coordinate = y ∧ (∀ (j : ↥D), o.2.2.1 ↑j = r.aliceAnswer j) ∧ ∀ (j : ↥D), o.2.2.2 ↑j = r.bobAnswer j

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

The total probability mass of exact fair full outcome born.

Equations

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

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) : exactFairFullOutcomeBornMass G n S D r x y = exactFairConditionedAnswerBornMass G n S D r x 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

theorem QuantumParallelRepetition.exactGlobalHistoryFinPsi_sub_Phi_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : ‖↑(exactGlobalHistoryFinPsi G n S D r x y) - ↑(exactGlobalHistoryFinPhi G n S D r y)‖ = ‖exactPsi G n S D r x y - exactPhi G n S D r y‖

theorem QuantumParallelRepetition.exactLocallySampleableLaw_zero_of_coordinate_mismatch {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (i : SourceRemainingCoordinate D) (x : X) (y : Y) (r : ExactHistoryFlag X Y A B D) (different : i ≠ r.seed.coordinate) : exactLocallySampleableLaw G n S D (i, x, y, r) = 0

theorem QuantumParallelRepetition.exactFairPosteriorExpectation_reindex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (f : ExactLocallySampleableTuple X Y A B D → ℝ) : ∑ t : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D t * f t = ∑ r : ExactHistoryFlag X Y A B D, ∑ y : Y, ∑ x : X, exactLocallySampleableLaw G n S D (r.seed.coordinate, x, y, r) * f (r.seed.coordinate, x, y, r)

noncomputable def QuantumParallelRepetition.exactFairAcceptedAliceEntropy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The entropy quantity for exact fair accepted alice.

Equations

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

noncomputable def QuantumParallelRepetition.exactFairAcceptedBobEntropy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

The entropy quantity for exact fair accepted bob.

Equations

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

def QuantumParallelRepetition.ExactFairOperatorEntropyBound {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (η : ℝ) : Prop

The numerical bound for exact fair operator entropy.

Equations

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

theorem QuantumParallelRepetition.exactSourceStateDistanceBound_of_fair_operator_entropy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (η : ℝ) (positive : 0 < repeatedPostselectionMass G n S D) (entropy : ExactFairOperatorEntropyBound G n S D η) : ExactSourceStateDistanceBound G n S D η