Quantum parallel repetition, part 11 #
theorem
QuantumParallelRepetition.unconditionalActualC485GenericRetainedWinningBorn
{X Y A B s t u v ι κ : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype s]
[Fintype t]
[Fintype u]
[Fintype v]
[Fintype ι]
[Fintype κ]
[DecidableEq s]
[DecidableEq t]
[DecidableEq u]
[DecidableEq v]
[DecidableEq ι]
[DecidableEq κ]
(G : Game X Y A B)
(eA : ι ≃ s × t)
(eB : κ ≃ u × v)
(PA : POVM A s)
(PB : POVM B u)
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
:
quadraticExpectation
(Matrix.toEuclideanCLM
(directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA PA)
(directDSVActualReindexedRetainedPOVM eB PB) x y))
z = quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (directDSVActualLocalPOVMWinningEffect G PA PB x y) 1))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)
theorem
QuantumParallelRepetition.unconditionalActualC485GenericSelectedWinningRegroupGauge
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{P N d m : ℕ}
{ι κ R T : Type}
[Fintype ι]
[Fintype κ]
[Fintype R]
[Fintype T]
[DecidableEq ι]
[DecidableEq κ]
[DecidableEq R]
[DecidableEq T]
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(pair : R × R ≃ T)
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
:
let selected := UnconditionalSelectedCopyLocalIndex P d N m;
have stage := physical8SelectedGlobalTargetWorkEquiv P N d m;
have gaugedAlice := directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM alice PA);
have gaugedBob := directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM bob PB);
have plainAlice := directDSVActualReindexedRetainedPOVM stage PA;
have plainBob := directDSVActualReindexedRetainedPOVM stage PB;
have regrouped :=
(LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl (selected × selected)).prodCongr pair))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z);
quadraticExpectation
(Matrix.toEuclideanCLM
(directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM eA gaugedAlice)
(directDSVActualReindexedRetainedPOVM eB gaugedBob) x y))
z = quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G plainAlice plainBob x y) 1))
(unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice)
(unconditionalMixedConjugateSigmaAtomLift P bob) regrouped)
theorem
QuantumParallelRepetition.unconditionalActualC485GenericDecodedWinningBorn
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{P N d m : ℕ}
{ι κ R T : Type}
[Fintype ι]
[Fintype κ]
[Fintype R]
[Fintype T]
[DecidableEq ι]
[DecidableEq κ]
[DecidableEq R]
[DecidableEq T]
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(pair : R × R ≃ T)
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
(actual :
EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T))
(decoded :
unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice)
(unconditionalMixedConjugateSigmaAtomLift P bob)
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
((Equiv.refl
(UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr
pair))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = actual)
:
let selected := UnconditionalSelectedCopyLocalIndex P d N m;
have stage := physical8SelectedGlobalTargetWorkEquiv P N d m;
quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM stage PA)
(directDSVActualReindexedRetainedPOVM stage PB) x y)
1))
actual = quadraticExpectation
(Matrix.toEuclideanCLM
(directDSVActualLocalPOVMWinningEffect G
(directDSVActualReindexedRetainedPOVM eA
(directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM alice PA)))
(directDSVActualReindexedRetainedPOVM eB
(directDSVActualReindexedRetainedPOVM stage (unitaryConjugatePOVM bob PB)))
x y))
z
theorem
QuantumParallelRepetition.unconditionalActualC485SourceSelectedDecodedWinningBorn
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{P N d m : ℕ}
{ι κ R T : Type}
[Fintype ι]
[Fintype κ]
[Fintype R]
[Fintype T]
[DecidableEq ι]
[DecidableEq κ]
[DecidableEq R]
[DecidableEq T]
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(selectedA : POVM A (UnconditionalSelectedCopyLocalIndex P d N m))
(selectedB : POVM B (UnconditionalSelectedCopyLocalIndex P d N m))
(selectedA_eq : selectedA = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PA)
(selectedB_eq : selectedB = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PB)
(eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(pair : R × R ≃ T)
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
(actual :
EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T))
(decoded :
unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice)
(unconditionalMixedConjugateSigmaAtomLift P bob)
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
((Equiv.refl
(UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr
pair))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = actual)
:
quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G selectedA selectedB x y) 1))
actual = quadraticExpectation
(Matrix.toEuclideanCLM
(directDSVActualLocalPOVMWinningEffect G
(directDSVActualReindexedRetainedPOVM eA
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM alice PA)))
(directDSVActualReindexedRetainedPOVM eB
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM bob PB)))
x y))
z
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceAliceTarget
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
:
ExactSourceSharedFlag X Y A B D denominator →
X → BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))
Alice's target vector determined by the shared source flag and her question.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceBobTarget
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
:
ExactSourceSharedFlag X Y A B D denominator →
Y → BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))
Bob's target vector determined by the shared source flag and his question.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.unconditionalActualC485CompleteDecodedPhysicalBorn
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{P N d m : ℕ}
{ι κ R T : Type}
[Fintype ι]
[Fintype κ]
[Fintype R]
[Fintype T]
[DecidableEq ι]
[DecidableEq κ]
[DecidableEq R]
[DecidableEq T]
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(selectedA : POVM A (UnconditionalSelectedCopyLocalIndex P d N m))
(selectedB : POVM B (UnconditionalSelectedCopyLocalIndex P d N m))
(selectedA_eq : selectedA = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PA)
(selectedB_eq : selectedB = directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) PB)
(eA : ι ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(eB : κ ≃ UnconditionalSelectedCopyLocalIndex P d N m × R)
(pair : R × R ≃ T)
(rawA : POVM A ι)
(rawB : POVM B κ)
(rawA_eq :
rawA = directDSVActualReindexedRetainedPOVM eA
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM alice PA)))
(rawB_eq :
rawB = directDSVActualReindexedRetainedPOVM eB
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM bob PB)))
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
(source cleaned :
EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × T))
(source_eq : source = cleaned)
(decoded :
unconditionalMixedConjugateSelectedBranchLocalAction (unconditionalMixedConjugateSigmaAtomLift P alice)
(unconditionalMixedConjugateSigmaAtomLift P bob)
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
((Equiv.refl
(UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr
pair))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv eA eB)) z)) = cleaned)
:
quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G selectedA selectedB x y) 1))
source = quadraticExpectation (Matrix.toEuclideanCLM (directDSVActualLocalPOVMWinningEffect G rawA rawB x y)) z
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceAliceFlagPOVM
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[DecidableEq A]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
(a₀ : A)
(P N L m : ℕ)
:
ExactSourceSharedFlag X Y A B D denominator →
Fin (L + 1) →
X →
POVM A
(UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)
The positive operator-valued measurement implementing unconditional actual fair source alice flag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceBobFlagPOVM
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[DecidableEq B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
(b₀ : B)
(P N L m : ℕ)
:
ExactSourceSharedFlag X Y A B D denominator →
Fin (L + 1) →
Y →
POVM B
(UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)
The positive operator-valued measurement implementing unconditional actual fair source bob flag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceAliceStoppingUnitary
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
:
ExactSourceSharedFlag X Y A B D denominator →
X →
↥(Matrix.unitaryGroup
((_ : Fin (L + 1)) ×
UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)
ℂ)
The unitary operator implementing unconditional actual fair source alice stopping.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceBobStoppingUnitary
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(cleanup : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
:
ExactSourceSharedFlag X Y A B D denominator →
Y →
↥(Matrix.unitaryGroup
((_ : Fin (L + 1)) ×
UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m)
ℂ)
The unitary operator implementing unconditional actual fair source bob stopping.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.unconditionalActualPairedDecodedMatchedCleanedVector
{F X Y : Type}
{P N d L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(ξ : F → X → BipartiteUnitVector d)
(ζ : F → Y → BipartiteUnitVector d)
(A C : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(grid : 0 < N)
(flag : F)
(x : X)
(y : Y)
(j : Fin L)
(positive : 0 < width (schedule j))
:
have phase := unconditionalActualOneScaleFixedSourcePhaseSplit P;
have outer := unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phase j;
have pair := unconditionalActualC485RetainedHistoryPairEquiv j;
have stopped :=
actualStoppingBranchVector
(actualStoppingQuestionLocalAction (physical8OneScaleActualAliceStoppingUnitary phase Q width schedule ξ A flag x)
(physical8OneScaleActualBobStoppingUnitary phase Q width schedule ζ C flag y)
(unconditionalSourcePhysicalCleanedStoppingFixedSource 1 P N d L m))
j.succ j.succ;
unconditionalMixedConjugateSelectedBranchLocalAction
(unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVDensityRationalCanonicalAliceBasis (ξ flag x))))
(unconditionalMixedConjugateSigmaAtomLift P (conjugateUnitary (dSVUniformDensityThresholdLeftBobBasis (ζ flag y))))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
((Equiv.refl
(UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr
pair))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (directDSVActualBilateralRetainedIndexEquiv outer outer)) stopped)) = integratorActualC485CleanedVector Q width schedule (ξ flag x) (ζ flag y) A C j
noncomputable def
QuantumParallelRepetition.unconditionalActualC485RawPhysicalVerifierBorn
{X Y A B ι κ : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
(G : Game X Y A B)
(PA : POVM A ι)
(PB : POVM B κ)
(x : X)
(y : Y)
(z : EuclideanSpace ℂ (ι × κ))
:
The quadratic expectation of the physical winning effect in the supplied vector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourceHistoryStopBorn
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(a₀ : A)
(b₀ : B)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(h : ExactLocallySampleableTuple X Y A B D)
(j : Fin L)
:
The Born-rule weight for unconditional actual fair source history stop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualFairSourcePhysicalStopBorn
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[DecidableEq A]
[DecidableEq B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
(a₀ : A)
(b₀ : B)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(flag : ExactSourceSharedFlag X Y A B D denominator)
(x : X)
(y : Y)
(j : Fin L)
:
The Born-rule weight for unconditional actual fair source physical stop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.unconditionalActualFairSourcePhysicalStopBornWitness
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[DecidableEq A]
[DecidableEq B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
(a₀ : A)
(b₀ : B)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(grid : 0 < N)
(width_positive : ∀ (s : Fin 1), 0 < width s)
(flag : ExactSourceSharedFlag X Y A B D denominator)
(x : X)
(y : Y)
(matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true)
(j : Fin L)
:
unconditionalActualFairSourceHistoryStopBorn G n S D a₀ b₀ Q width schedule UA UB
(exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)) j = unconditionalActualFairSourcePhysicalStopBorn G n S D denominator numerator nonempty a₀ b₀ Q width schedule UA UB flag
x y j
theorem
QuantumParallelRepetition.unconditionalActualFairSourcePhysicalBranchWitness
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[DecidableEq A]
[DecidableEq B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(denominator : ℕ)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
(a₀ : A)
(b₀ : B)
{P N L m : ℕ}
(Q : ℕ)
(width : Fin 1 → ℝ)
(schedule : Fin L → Fin 1)
(UA UB : Fin P → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(grid : 0 < N)
(width_positive : ∀ (s : Fin 1), 0 < width s)
(flag : ExactSourceSharedFlag X Y A B D denominator)
(x : X)
(y : Y)
(matching : exactSourcePermutationMatched D denominator numerator nonempty (flag, x, y) = true)
:
∑ j : Fin L,
unconditionalActualFairSourceHistoryStopBorn G n S D a₀ b₀ Q width schedule UA UB
(exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y)) j = ∑ j : Fin L,
unconditionalActualFairSourcePhysicalStopBorn G n S D denominator numerator nonempty a₀ b₀ Q width schedule UA UB
flag x y j