Quantum parallel repetition, part 10 #
theorem
QuantumParallelRepetition.unconditionalPhysicalOneScaleActualGlobalFiberPOVM_nested
{C : Type u_1}
[Fintype C]
{P N d L m : ℕ}
{R : Type}
[Fintype R]
[DecidableEq R]
(phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R)
(j : Fin L)
(source : POVM C (Fin d))
:
directDSVActualReindexedRetainedPOVM (physical8OneScaleActualGlobalFiberEquiv phaseSplit j) source = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phaseSplit j)
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)
theorem
QuantumParallelRepetition.unconditionalPhysicalOneScaleOriginalFlagPOVM_succ_nested
{C : Type u_1}
{Z : Type u_2}
[Fintype C]
[DecidableEq C]
{P N d L m : ℕ}
{R : Type}
[Fintype R]
[DecidableEq R]
(phaseSplit : DSVDensityRationalPublicMultiscalePhaseIndex 1 P ≃ Fin P × R)
(default : C)
(source : Z → POVM C (Fin d))
(j : Fin L)
(x : Z)
:
physical8OneScaleOriginalFlagPOVM phaseSplit default source j.succ x = directDSVActualReindexedRetainedPOVM (unconditionalSourcePhysicalCleanedFullLocalIndexEquiv phaseSplit j)
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) (source x))
theorem
QuantumParallelRepetition.unconditionalSelectedGaugeRetainedPOVMNaturality_effect
{C : Type}
[Fintype C]
{P N d m : ℕ}
(basis : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(source : POVM C (Fin d))
(a : C)
:
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM basis source)).effect
a = (unitaryConjugatePOVM (unconditionalMixedConjugateSigmaAtomLift P basis)
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)).effect
a
theorem
QuantumParallelRepetition.unconditionalSelectedGaugeRetainedPOVMNaturality
{C : Type}
[Fintype C]
{P N d m : ℕ}
(basis : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(source : POVM C (Fin d))
:
directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m)
(unitaryConjugatePOVM basis source) = unitaryConjugatePOVM (unconditionalMixedConjugateSigmaAtomLift P basis)
(directDSVActualReindexedRetainedPOVM (physical8SelectedGlobalTargetWorkEquiv P N d m) source)
theorem
QuantumParallelRepetition.unconditionalActualFairSourceSelectedRetainedWinningEffectGauge
{X Y A B : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
{P N d m : ℕ}
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(x : X)
(y : Y)
:
have e := physical8SelectedGlobalTargetWorkEquiv P N d m;
have U := unconditionalMixedConjugateSigmaAtomLift P alice;
have V := unconditionalMixedConjugateSigmaAtomLift P bob;
directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM alice PA))
(directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM bob PB)) x y = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V).conjTranspose * directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e PA)
(directDSVActualReindexedRetainedPOVM e PB) x y * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V
theorem
QuantumParallelRepetition.unconditionalActualFairSourceSelectedRetainedWinningBornGauge
{X Y A B τ : Type}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype τ]
[DecidableEq τ]
{P N d m : ℕ}
(G : Game X Y A B)
(alice bob : ↥(Matrix.unitaryGroup (Fin d) ℂ))
(PA : POVM A (Fin d))
(PB : POVM B (Fin d))
(x : X)
(y : Y)
(z : EuclideanSpace ℂ ((UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m) × τ))
:
have e := physical8SelectedGlobalTargetWorkEquiv P N d m;
have U := unconditionalMixedConjugateSigmaAtomLift P alice;
have V := unconditionalMixedConjugateSigmaAtomLift P bob;
quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G
(directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM alice PA))
(directDSVActualReindexedRetainedPOVM e (unitaryConjugatePOVM bob PB)) x y)
1))
z = quadraticExpectation
(Matrix.toEuclideanCLM
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(directDSVActualLocalPOVMWinningEffect G (directDSVActualReindexedRetainedPOVM e PA)
(directDSVActualReindexedRetainedPOVM e PB) x y)
1))
(unconditionalMixedConjugateSelectedBranchLocalAction U V z)
theorem
QuantumParallelRepetition.unconditionalActualC485RetainedPureWorkReindexBorn
{s t v : Type}
[Fintype s]
[DecidableEq s]
[Fintype t]
[DecidableEq t]
[Fintype v]
[DecidableEq v]
(e : t ≃ v)
(winning : Matrix s s ℂ)
(z : EuclideanSpace ℂ (s × t))
:
quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) winning 1)) z = quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) winning 1))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ ((Equiv.refl s).prodCongr e)) z)
def
QuantumParallelRepetition.unconditionalActualC485RetainedHistoryPairEquiv
{P N d L : ℕ}
(j : Fin L)
:
The finite equivalence encoding unconditional actual c 485 retained history pair.
Equations
Instances For
theorem
QuantumParallelRepetition.unconditionalActualC485FullBilateralWorkRegroup
{P N d L m : ℕ}
(j : Fin L)
(z :
EuclideanSpace ℂ
(UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m × UnconditionalSourcePhysicalStoppingPhaseFiber 1 P N d L m))
:
(LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
((Equiv.refl
(UnconditionalSelectedCopyLocalIndex P d N m × UnconditionalSelectedCopyLocalIndex P d N m)).prodCongr
(unconditionalActualC485RetainedHistoryPairEquiv j)))
((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ
(directDSVActualBilateralRetainedIndexEquiv
(unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P) j)
(unconditionalSourcePhysicalCleanedFullLocalIndexEquiv (unconditionalActualOneScaleFixedSourcePhaseSplit P)
j)))
z) = (unconditionalSourcePhysicalCleanedFullBilateralStateIsometry (unconditionalActualOneScaleFixedSourcePhaseSplit P) j)
z
theorem
QuantumParallelRepetition.unconditionalWeightedClippedMatchedVerifierAndMassLoss
{I : Type u_1}
{K : Type u_2}
[Fintype I]
[Fintype K]
(weight : I → ℝ)
(weight_nonnegative : ∀ (i : I), 0 ≤ weight i)
(weight_normalized : ∑ i : I, weight i = 1)
(win : I → ℝ)
(win_bounded : ∀ (i : I), win i ≤ 1)
{H : I × K → Type u_3}
[(p : I × K) → NormedAddCommGroup (H p)]
[(p : I × K) → InnerProductSpace ℂ (H p)]
(effect : (p : I × K) → H p →L[ℂ] H p)
(contraction : ∀ (p : I × K), ‖effect p‖ ≤ 1)
(actual canonical source : (p : I × K) → H p)
(actual_mass : ∑ i : I, weight i * ∑ k : K, ‖actual (i, k)‖ ^ 2 ≤ 1)
(canonical_mass : ∑ i : I, weight i * ∑ k : K, ‖canonical (i, k)‖ ^ 2 ≤ 1)
(canonical_row_mass : ∀ (i : I), ∑ k : K, ‖canonical (i, k)‖ ^ 2 ≤ 1)
(same_work_mass : ∀ (i : I) (k : K), ‖source (i, k)‖ = ‖canonical (i, k)‖)
(supported_born :
∀ (i : I),
weight i ≠ 0 → ∀ (k : K), quadraticExpectation (effect (i, k)) (source (i, k)) = ‖source (i, k)‖ ^ 2 * win i)
(Δclean Δclip bad : ℝ)
(clean_deviation : ∑ i : I, weight i * ∑ k : K, ‖actual (i, k) - canonical (i, k)‖ ^ 2 ≤ Δclean)
(clip_deviation : ∑ i : I, weight i * ∑ k : K, ‖canonical (i, k) - source (i, k)‖ ^ 2 ≤ Δclip)
(actual_success : 1 - bad ≤ ∑ i : I, weight i * ∑ k : K, ‖actual (i, k)‖ ^ 2)
:
theorem
QuantumParallelRepetition.unconditionalFairPhysicalFlaggedStoppingTransfer
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(denominator : ℕ)
(denominator_positive : 0 < denominator)
(numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ)
(rational_normalized :
∀ (index : ExactLocalSamplerIndex X Y D),
∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator)
(support_preserving :
∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D),
0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history →
0 < numerator index history)
(nonempty :
∀ (index : ExactLocalSamplerIndex X Y D), (ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty)
{L : ℕ}
{ι : Fin (L + 1) → Type}
[(r : Fin (L + 1)) → Fintype (ι r)]
[(r : Fin (L + 1)) → DecidableEq (ι r)]
(PA : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → X → POVM A (ι r))
(PB : ExactSourceSharedFlag X Y A B D denominator → (r : Fin (L + 1)) → Y → POVM B (ι r))
(U : ExactSourceSharedFlag X Y A B D denominator → X → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ))
(V : ExactSourceSharedFlag X Y A B D denominator → Y → ↥(Matrix.unitaryGroup ((r : Fin (L + 1)) × ι r) ℂ))
(z :
ExactSourceSharedFlag X Y A B D denominator → EuclideanSpace ℂ (((r : Fin (L + 1)) × ι r) × (r : Fin (L + 1)) × ι r))
(z_normalized : ∀ (flag : ExactSourceSharedFlag X Y A B D denominator), ‖z flag‖ = 1)
(matched : ExactSourceSharedFlag X Y A B D denominator × X × Y → Bool)
{K : Type u_1}
[Fintype K]
{H : ExactLocallySampleableTuple X Y A B D × K → Type u_2}
[(p : ExactLocallySampleableTuple X Y A B D × K) → NormedAddCommGroup (H p)]
[(p : ExactLocallySampleableTuple X Y A B D × K) → InnerProductSpace ℂ (H p)]
(effect : (p : ExactLocallySampleableTuple X Y A B D × K) → H p →L[ℂ] H p)
(contraction : ∀ (p : ExactLocallySampleableTuple X Y A B D × K), ‖effect p‖ ≤ 1)
(actual canonical source : (p : ExactLocallySampleableTuple X Y A B D × K) → H p)
(actual_mass :
∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k)‖ ^ 2 ≤ 1)
(canonical_mass :
∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖canonical (h, k)‖ ^ 2 ≤ 1)
(canonical_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ k : K, ‖canonical (h, k)‖ ^ 2 ≤ 1)
(same_work_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D) (k : K), ‖source (h, k)‖ = ‖canonical (h, k)‖)
(supported_born :
∀ (h : ExactLocallySampleableTuple X Y A B D),
exactLocallySampleableLaw G n S D h ≠ 0 →
∀ (k : K),
quadraticExpectation (effect (h, k)) (source (h, k)) = ‖source (h, k)‖ ^ 2 * exactSourceConditionalWinningProbability G n S D h)
(epsilon lam deviation clipping bad : ℝ)
(clean_deviation :
∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k) - canonical (h, k)‖ ^ 2 ≤ deviation)
(clip_deviation :
∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * ∑ k : K, ‖canonical (h, k) - source (h, k)‖ ^ 2 ≤ clipping)
(actual_success :
1 - bad ≤ ∑ h : ExactLocallySampleableTuple X Y A B D, exactLocallySampleableLaw G n S D h * ∑ k : K, ‖actual (h, k)‖ ^ 2)
(history_born_nonnegative :
∀ (h : ExactLocallySampleableTuple X Y A B D), 0 ≤ ∑ k : K, quadraticExpectation (effect (h, k)) (actual (h, k)))
(history_born_bounded :
∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ k : K, quadraticExpectation (effect (h, k)) (actual (h, k)) ≤ 1)
(source_failure : uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < epsilon / 2)
(total_variation :
Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator))
(exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ lam)
(mismatch :
(∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y,
flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if matched outcome = true then 0 else 1) ≤ 4 * lam)
(matched_physical_branch :
∀ (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) (y : Y),
matched (flag, x, y) = true →
∑ k : K,
quadraticExpectation (effect (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k))
(actual (exactSourceAliceSampleTuple D denominator numerator nonempty (flag, x, y), k)) ≤ ∑ j : Fin L,
quadraticExpectation
(Matrix.toEuclideanCLM (actualStoppingBranchWinningEffect G (PA flag) (PB flag) j.succ j.succ x y))
(actualStoppingBranchVector (actualStoppingQuestionLocalAction (U flag x) (V flag y) (z flag)) j.succ
j.succ))
:
1 - epsilon / 2 - 5 * lam - (bad + 4 * √deviation + 2 * √clipping) ≤ (pureFlaggedStrategy G (exactSourceSharedFlagWeight D denominator) ⋯ ⋯ z z_normalized
(fun (flag : ExactSourceSharedFlag X Y A B D denominator) (x : X) =>
unitaryConjugatePOVM (U flag x) (dependentBlockPOVM fun (r : Fin (L + 1)) => PA flag r x))
fun (flag : ExactSourceSharedFlag X Y A B D denominator) (y : Y) =>
unitaryConjugatePOVM (V flag y) (dependentBlockPOVM fun (r : Fin (L + 1)) => PB flag r y)).winProbability
theorem
QuantumParallelRepetition.unconditionalActualLocalPOVMWinningEffect_posSemidef
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
{s : Type u_5}
{t : Type u_6}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype s]
[Fintype t]
[DecidableEq s]
[DecidableEq t]
(G : Game X Y A B)
(PA : POVM A s)
(PB : POVM B t)
(x : X)
(y : Y)
:
(directDSVActualLocalPOVMWinningEffect G PA PB x y).PosSemidef
theorem
QuantumParallelRepetition.unconditionalActualLocalPOVMWinningEffect_complement_posSemidef
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
{s : Type u_5}
{t : Type u_6}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype s]
[Fintype t]
[DecidableEq s]
[DecidableEq t]
(G : Game X Y A B)
(PA : POVM A s)
(PB : POVM B t)
(x : X)
(y : Y)
:
(1 - directDSVActualLocalPOVMWinningEffect G PA PB x y).PosSemidef
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_isPositive
{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 : ℕ}
(j : Fin L)
(x : X)
(y : Y)
:
(integratorActualC485WinningEffect G n S D a₀ b₀ j x y).IsPositive
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_complement_isPositive
{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 : ℕ}
(j : Fin L)
(x : X)
(y : Y)
:
(1 - integratorActualC485WinningEffect G n S D a₀ b₀ j x y).IsPositive
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_born_nonnegative
{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 : ℕ}
(j : Fin L)
(x : X)
(y : Y)
(z : IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j)
:
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_born_le_mass
{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 : ℕ}
(j : Fin L)
(x : X)
(y : Y)
(z : IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j)
:
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_bounds
{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 : ℕ}
(actual :
ExactLocallySampleableTuple X Y A B D →
(j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j)
(actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1)
(h : ExactLocallySampleableTuple X Y A B D)
:
0 ≤ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ∧ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ≤ 1
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_nonnegative
{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 : ℕ}
(actual :
ExactLocallySampleableTuple X Y A B D →
(j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j)
(actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1)
(h : ExactLocallySampleableTuple X Y A B D)
:
0 ≤ ∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j)
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVerifier_historyBorn_bounded
{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 : ℕ}
(actual :
ExactLocallySampleableTuple X Y A B D →
(j : Fin L) → IntegratorActualC485BranchSpace 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L m j)
(actual_row_mass : ∀ (h : ExactLocallySampleableTuple X Y A B D), ∑ j : Fin L, ‖actual h j‖ ^ 2 ≤ 1)
(h : ExactLocallySampleableTuple X Y A B D)
:
∑ j : Fin L, quadraticExpectation (integratorActualC485WinningEffect G n S D a₀ b₀ j h.2.1 h.2.2.1) (actual h j) ≤ 1
noncomputable def
QuantumParallelRepetition.unconditionalActualC485FairSourceDiagonalWork
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(w : ℝ)
(N P : ℕ)
{L : ℕ}
(schedule : Fin L → Fin 1)
(u : ExactLocallySampleableTuple X Y A B D)
(j : Fin L)
:
EuclideanSpace ℂ (IntegratorActualC485RetainedIndex 1 P N (Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) L j)
The unconditional actual c 485 fair source diagonal work construction used in the quantum parallel-repetition argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
{w : ℝ}
{N P L m : ℕ}
(width : 0 < w)
(grid : 0 < N)
(fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1))
(schedule : Fin L → Fin 1)
:
The energy quantity for unconditional actual c 485 fair source clip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
QuantumParallelRepetition.unconditionalActualC485FairSourceDiagonalWork_row
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
{w : ℝ}
{N P L m : ℕ}
(width : 0 < w)
(grid : 0 < N)
(dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D))
(phases : 0 < P)
(harmonic : 0 < m)
(schedule : Fin L → Fin 1)
(u : ExactLocallySampleableTuple X Y A B D)
:
theorem
QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy_le
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(D : Finset (Fin n))
(remaining : 0 < (Finset.univ \ D).card)
(source_positive : 0 < repeatedPostselectionMass G n S D)
{w : ℝ}
{N P L m : ℕ}
(width : 0 < w)
(grid : 0 < N)
(dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D))
(fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1))
(phases : 0 < P)
(harmonic : 0 < m)
(schedule : Fin L → Fin 1)
:
unconditionalActualC485FairSourceClipEnergy G n S D width grid fine schedule ≤ 16 * martingaleRate G n S D + 8 * (1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N)
theorem
QuantumParallelRepetition.unconditionalActualC485FairSourceClipEnergy_le_budget
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[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)
(source_positive : 0 < repeatedPostselectionMass G n S D)
{w δ : ℝ}
{N P L m : ℕ}
(width : 0 < w)
(grid : 0 < N)
(dimension : 0 < Fintype.card (ExactGlobalHistoryLocalIndex G n S D))
(fine : ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1))
(phases : 0 < P)
(harmonic : 0 < m)
(schedule : Fin L → Fin 1)
(scalar : 1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N ≤ 3 * δ / 2)
:
unconditionalActualC485FairSourceClipEnergy G n S D width grid fine schedule ≤ 16 * martingaleRate G n S D + 8 * (3 * δ / 2)
theorem
QuantumParallelRepetition.unconditionalActualFairSelectedLocalAction_norm_sq
{ι τ : Type}
[Fintype ι]
[DecidableEq ι]
[Fintype τ]
[DecidableEq τ]
(U V : ↥(Matrix.unitaryGroup ι ℂ))
(z : EuclideanSpace ℂ ((ι × ι) × τ))
:
theorem
QuantumParallelRepetition.unconditionalActualFairCleanedVector_norm_sq
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(Q : ℕ)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(j : Fin L)
:
‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑j * dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑j
theorem
QuantumParallelRepetition.unconditionalActualFairCleanedRow_eq_stoppedSuccess
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(Q : ℕ)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
:
∑ j : Fin L, ‖integratorActualC485CleanedVector Q width schedule ξ ζ A C j‖ ^ 2 = dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ
theorem
QuantumParallelRepetition.unconditionalActualFairCleanedRow_le_one
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(Q : ℕ)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
:
theorem
QuantumParallelRepetition.unconditionalActualFairWeightedCleanedMass_le_one
{I : Type}
[Fintype I]
{S B N d L m : ℕ}
(weight : I → ℝ)
(weight_nonnegative : ∀ (h : I), 0 ≤ weight h)
(weight_normalized : ∑ h : I, weight h = 1)
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : I → BipartiteUnitVector d)
(Q : ℕ)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
:
theorem
QuantumParallelRepetition.unconditionalActualFairWeightedStoppedSuccess
{I : Type}
[Fintype I]
{S B N d L m : ℕ}
(weight : I → ℝ)
(weight_normalized : ∑ h : I, weight h = 1)
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : I → BipartiteUnitVector d)
(Q : ℕ)
(A C : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ))
(async terminal : ℝ)
(asynchronous_bound :
∑ h : I, weight h * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ h) (ζ h) ≤ async)
(terminal_bound :
∑ h : I, weight h * dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ h) (ζ h) ≤ terminal)
:
theorem
QuantumParallelRepetition.unconditionalActualFairCanonicalVector_norm_sq
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(j : Fin L)
(positive : 0 < width (schedule j))
(fine : ↑d / ↑N < 1 / (width (schedule j) + 1))
:
‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖ ^ 2 = ‖integratorActualC485NormalizedDiagonalWork width schedule ξ ζ j‖ ^ 2
theorem
QuantumParallelRepetition.unconditionalActualFairCanonicalRow_le_one
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1))
:
theorem
QuantumParallelRepetition.unconditionalActualFairWeightedCanonicalMass_le_one
{I : Type}
[Fintype I]
{S B N d L m : ℕ}
(weight : I → ℝ)
(weight_nonnegative : ∀ (h : I), 0 ≤ weight h)
(weight_normalized : ∑ h : I, weight h = 1)
(phases : 0 < B)
(grid : 0 < N)
(dimension : 0 < d)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(width_positive : ∀ (s : Fin S), 0 < width s)
(schedule : Fin L → Fin S)
(ξ ζ : I → BipartiteUnitVector d)
(fine : ∀ (s : Fin S), ↑d / ↑N < 1 / (width s + 1))
:
theorem
QuantumParallelRepetition.unconditionalActualFairSourceVector_norm_sq
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(ψ : EuclideanSpace ℂ (Fin d × Fin d))
(unit : ‖ψ‖ = 1)
(j : Fin L)
:
‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ ^ 2 = ‖integratorActualC485NormalizedDiagonalWork width schedule ξ ζ j‖ ^ 2
theorem
QuantumParallelRepetition.unconditionalActualFairSourceCanonicalVector_norm_sq
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(ψ : EuclideanSpace ℂ (Fin d × Fin d))
(unit : ‖ψ‖ = 1)
(j : Fin L)
(positive : 0 < width (schedule j))
(fine : ↑d / ↑N < 1 / (width (schedule j) + 1))
:
‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ ^ 2 = ‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖ ^ 2
theorem
QuantumParallelRepetition.unconditionalActualFairSourceCanonicalVector_norm
{S B N d L m : ℕ}
(phases : 0 < B)
(grid : 0 < N)
(harmonic : 0 < m)
(width : Fin S → ℝ)
(schedule : Fin L → Fin S)
(ξ ζ : BipartiteUnitVector d)
(ψ : EuclideanSpace ℂ (Fin d × Fin d))
(unit : ‖ψ‖ = 1)
(j : Fin L)
(positive : 0 < width (schedule j))
(fine : ↑d / ↑N < 1 / (width (schedule j) + 1))
:
‖integratorActualC485SourceVector width schedule ξ ζ ψ j‖ = ‖integratorActualC485CanonicalVector schedule ξ ζ j positive grid fine‖
theorem
QuantumParallelRepetition.unconditionalActualSourceSamplerBounds
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(base : ExactHistoryFlag X Y A B D)
(gamma : ℝ)
(gamma_positive : 0 < gamma)
:
∃ (denominator : ℕ),
0 < denominator ∧ ∃ (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ),
(∀ (index : ExactLocalSamplerIndex X Y D),
∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) ∧ (∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D),
0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history →
0 < numerator index history) ∧ ∃ (nonempty :
∀ (index : ExactLocalSamplerIndex X Y D),
(ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty),
Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator))
(exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ exactSourcePinskerRate G n S D + gamma ∧ (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y,
flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if exactSourcePermutationMatched D denominator numerator nonempty outcome = true then 0 else 1) ≤ 4 * (exactSourcePinskerRate G n S D + gamma)
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalSameGridWeightedStoppingLedger
{d N : ℕ}
(dimension : 0 < d)
(grid : 0 < N)
(w δ : ℝ)
(large : 1 ≤ w)
(precision : 0 < δ)
(bounded : δ ≤ 1)
(grid_budget : 2 * (w + 1) * (↑d / ↑N) ≤ δ)
(t : ℝ)
(t_positive : 0 < t)
(t_bounded : t ≤ 1)
(rho : ℝ)
(rho_positive : 0 < rho)
{ι : Type}
[Fintype ι]
(weight : ι → ℝ)
(weight_nonnegative : ∀ (i : ι), 0 ≤ weight i)
(weight_normalized : ∑ i : ι, weight i = 1)
(ξ ζ : ι → BipartiteUnitVector d)
(eta : ℝ)
(source_energy : ∑ i : ι, weight i * ‖↑(ξ i) - ↑(ζ i)‖ ^ 2 ≤ 32 * eta)
:
∃ (L : ℕ) (B : ℕ) (Q : ℕ) (m : ℕ),
0 < L ∧ 0 < B ∧ 0 < Q ∧ 0 < m ∧ ∃ (A : Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (C :
Fin B → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)),
have width := fun (x : Fin 1) => w;
have schedule := fun (x : Fin L) => 0;
(∀ (i : ι),
dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ i) (ζ i) ≤ 8 * √2 * ‖↑(ξ i) - ↑(ζ i)‖ + δ) ∧ (∀ (i : ι), dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ i) (ζ i) ≤ δ ^ 2) ∧ ∑ i : ι,
weight i * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule (ξ i) (ζ i) ≤ 64 * √eta + δ ∧ ∑ i : ι, weight i * dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule (ξ i) (ζ i) ≤ δ ^ 2 ∧ ∑ i : ι,
weight i * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m width schedule (ξ i) (ζ i) A C ≤ 34 / t * (64 * √eta + δ) + 4 * rho ^ 2 + (16 * (Real.exp 1 - 1) + 4) * t
theorem
QuantumParallelRepetition.unconditionalSmallSourcePhysicalLoss
(K eta alpha deviation clipping : ℝ)
(lowerBound : 1024 + 8 * (4 * √(34 + unconditionalPrefactorBucketCoefficient) + 2) ≤ K)
(eta_nonnegative : 0 ≤ eta)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(small : 64 * √eta + alpha ^ (1 / 3) ≤ 1)
(actual_deviation :
deviation ≤ 34 / √(64 * √eta + alpha ^ (1 / 3)) * (64 * √eta + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √eta + alpha ^ (1 / 3)))
(actual_clipping : clipping ≤ 16 * eta + 8 * (3 * alpha ^ (1 / 3) / 2))
:
theorem
QuantumParallelRepetition.unconditionalSmallSourcePhysicalRoundedLower
(K eta alpha deviation clipping epsilon lam actual : ℝ)
(lowerBound : 1024 + 8 * (4 * √(34 + unconditionalPrefactorBucketCoefficient) + 2) ≤ K)
(eta_nonnegative : 0 ≤ eta)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(small : 64 * √eta + alpha ^ (1 / 3) ≤ 1)
(actual_deviation :
deviation ≤ 34 / √(64 * √eta + alpha ^ (1 / 3)) * (64 * √eta + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √eta + alpha ^ (1 / 3)))
(actual_clipping : clipping ≤ 16 * eta + 8 * (3 * alpha ^ (1 / 3) / 2))
(lam_nonnegative : 0 ≤ lam)
(actual_original_verifier :
1 - epsilon / 2 - 5 * lam - (64 * √eta + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 4 * √clipping + 2 * √(8 * eta)) ≤ actual)
:
theorem
QuantumParallelRepetition.pdfQuantitativeGreedyConditioning
{X : Type u_1}
{Y : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
(G : Game X Y A B)
(n : ℕ)
(S : Strategy (G.repeat n))
(τ d θ : ℝ)
(_n_positive : 0 < n)
(threshold : 0 < τ)
(threshold_lt_one : τ < 1)
(_rate_positive : 0 < d)
(rate_small : d ≤ τ / 2)
(above_exponential : Real.exp (-d * ↑n) < θ)
(realized : θ ≤ S.winProbability)
:
∃ (D : Finset (Fin n)),
↑D.card < d * ↑n / τ ∧ ↑n / 2 < ↑(Finset.univ \ D).card ∧ θ ≤ repeatedPostselectionMass G n S D ∧ S.winProbability ≤ repeatedPostselectionMass G n S D ∧ 0 < repeatedPostselectionMass G n S D ∧ 0 < (Finset.univ \ D).card ∧ uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < τ
theorem
QuantumParallelRepetition.pdfFixedExponentialBound_of_sourceEquationTwentyNine
{X : Type u_1}
{Y : Type u_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 : ℝ)
(construct :
∀ (S : Strategy (G.repeat n)),
Real.exp (-d * ↑n) < S.winProbability →
∃ (rounded : Strategy G) (K₀ : ℝ) (α : ℝ) (η : ℝ) (lam : ℝ),
roundedWinningLowerBound (1 - entangledValue G) K₀ α η lam ≤ rounded.winProbability ∧ totalSamplingLoss K₀ α η lam < (1 - entangledValue G) / 2)
:
theorem
QuantumParallelRepetition.pdfPredicate_not_accepted_of_entangledValue_eq_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)
(zero : entangledValue G = 0)
(x : X)
(y : Y)
(a : A)
(b : B)
(supported : 0 < G.questionWeight x y)
:
theorem
QuantumParallelRepetition.pdf_distributionUniformExponential_of_uniform_source_rounding
(rounding :
∃ (K : ℝ),
1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
0 < (Finset.univ \ D).card →
0 < repeatedPostselectionMass G n S D →
∀ (alpha gamma : ℝ),
0 < alpha →
alpha ≤ 1 →
0 < gamma →
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 →
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D)
(exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability)
:
∃ (c : ℝ),
0 < c ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B),
Nonempty A →
Nonempty B →
0 < 1 - entangledValue G →
∀ (n : ℕ),
0 < n →
repeatedEntangledValue G n ≤ Real.exp
(-(c * ((1 - entangledValue G) ^ 13 / (1 - entangledValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)
The constant used to control unconditional source physical rounding universal.
Equations
Instances For
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_sourceSampler
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(gamma : ℝ)
(gamma_positive : 0 < gamma)
:
∃ (base : ExactHistoryFlag X Y A B D) (denominator : ℕ),
0 < denominator ∧ ∃ (numerator : ExactLocalSamplerIndex X Y D → ExactHistoryFlag X Y A B D → ℕ),
(∀ (index : ExactLocalSamplerIndex X Y D),
∑ history : ExactHistoryFlag X Y A B D, numerator index history = denominator) ∧ (∀ (index : ExactLocalSamplerIndex X Y D) (history : ExactHistoryFlag X Y A B D),
0 < exactLocalConditionalFamily D base (exactLocallySampleableLaw G n S D) index history →
0 < numerator index history) ∧ ∃ (nonempty :
∀ (index : ExactLocalSamplerIndex X Y D),
(ClassicalSampling.rationalMarked denominator (numerator index)).Nonempty),
Pinsker.finiteTotalVariation (flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator))
(exactSourceAliceFlagCoupling G n S D denominator numerator nonempty) ≤ exactSourcePinskerRate G n S D + gamma ∧ (∑ outcome : ExactSourceSharedFlag X Y A B D denominator × X × Y,
flaggedQuestionWeight G (exactSourceSharedFlagWeight D denominator) outcome * if exactSourcePermutationMatched D denominator numerator nonempty outcome = true then 0 else 1) ≤ 4 * (exactSourcePinskerRate G n S D + gamma)
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_fairTargetEnergy
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
:
∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * ‖↑(exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1) - ↑(exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1)‖ ^ 2 ≤ 32 * martingaleRate G n S D
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_fairStoppingHazard
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(alpha : ℝ)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1)
:
∃ (w : ℝ) (N : ℕ) (L : ℕ) (B' : ℕ) (Q : ℕ) (m : ℕ),
1 ≤ w ∧ 0 < N ∧ 0 < L ∧ 0 < B' ∧ 0 < Q ∧ 0 < m ∧ 2 * (w + 1) * (↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N) ≤ alpha ^ (1 / 3) ∧ ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) / ↑N < 1 / (w + 1) ∧ 1 / w + ↑(Fintype.card (ExactGlobalHistoryLocalIndex G n S D)) * w / ↑N ≤ 3 * alpha ^ (1 / 3) / 2 ∧ ∃ (UA : Fin B' → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)) (UB :
Fin B' → Option ℕ → ↥(Matrix.unitaryGroup (Fin (N * m)) ℂ)),
have width := fun (x : Fin 1) => w;
have schedule := fun (x : Fin L) => 0;
have eta := martingaleRate G n S D;
have delta := alpha ^ (1 / 3);
have t := √(64 * √eta + delta);
have rho := alpha ^ (1 / 12);
(∀ (ξ : BipartiteUnitVector (Fintype.card (ExactGlobalHistoryLocalIndex G n S D))),
‖↑ξ - dSVDensityRationalCanonicalAcceptedTarget w N ξ‖ ^ 2 ≤ 3 * delta / 2) ∧ ∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule
(exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1)
(exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) ≤ 64 * √eta + delta ∧ ∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule
(exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1)
(exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) ≤ delta ^ 2 ∧ ∑ h : ExactLocallySampleableTuple X Y A B D,
exactLocallySampleableLaw G n S D h * dSVDensityRationalHeterogeneousStoppedCommonPrefixHazard Q m width schedule
(exactGlobalHistoryFinGamma G n S D h.2.2.2 h.2.1)
(exactGlobalHistoryFinPhi G n S D h.2.2.2 h.2.2.1) UA UB ≤ 34 / t * (64 * √eta + delta) + 4 * rho ^ 2 + unconditionalPrefactorBucketCoefficient * t
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_largeVerifierBound
(K eta alpha lam epsilon : ℝ)
(lowerBound : 128 ≤ K)
(eta_nonnegative : 0 ≤ eta)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(lam_nonnegative : 0 ≤ lam)
(epsilon_nonnegative : 0 ≤ epsilon)
(large : 1 < 64 * √eta + alpha ^ (1 / 3))
:
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_exists_large
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(K alpha gamma : ℝ)
(lowerBound : 128 ≤ K)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(gamma_positive : 0 < gamma)
(large : 1 < 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3))
:
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D)
(exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_smallRoundedLower
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(alpha gamma deviation clipping : ℝ)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(gamma_positive : 0 < gamma)
(small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1)
(actual_deviation :
deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)))
(actual_clipping : clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2))
(rounded : Strategy G)
(actual_original_verifier :
1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 4 * √clipping + 2 * √(8 * martingaleRate G n S D)) ≤ rounded.winProbability)
:
roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha
(martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.unconditionalSourcePhysicalRounding_smallRoundedLower_of_stoppedVerifier
{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))
(remaining : 0 < (Finset.univ \ D).card)
(positive : 0 < repeatedPostselectionMass G n S D)
(alpha gamma deviation clipping : ℝ)
(alpha_positive : 0 < alpha)
(alpha_bounded : alpha ≤ 1)
(gamma_positive : 0 < gamma)
(small : 64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1)
(actual_deviation :
deviation ≤ 34 / √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) * (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)) + 4 * (alpha ^ (1 / 12)) ^ 2 + unconditionalPrefactorBucketCoefficient * √(64 * √(martingaleRate G n S D) + alpha ^ (1 / 3)))
(actual_clipping : clipping ≤ 16 * martingaleRate G n S D + 8 * (3 * alpha ^ (1 / 3) / 2))
(rounded : Strategy G)
(stopped_verifier :
1 - (1 - entangledValue G) / 2 - 5 * (exactSourcePinskerRate G n S D + gamma) - (64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) + (alpha ^ (1 / 3)) ^ 2 + 4 * √deviation + 2 * √clipping) ≤ rounded.winProbability)
:
roundedWinningLowerBound (1 - entangledValue G) unconditionalSourcePhysicalRoundingUniversalConstant alpha
(martingaleRate G n S D) (exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability
theorem
QuantumParallelRepetition.unconditionalSourceOneGameRounding_uniform_of_small
(small_rounding :
∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
0 < (Finset.univ \ D).card →
0 < repeatedPostselectionMass G n S D →
∀ (alpha gamma : ℝ),
0 < alpha →
alpha ≤ 1 →
0 < gamma →
64 * √(martingaleRate G n S D) + alpha ^ (1 / 3) ≤ 1 →
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 →
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G)
unconditionalSourcePhysicalRoundingUniversalConstant alpha (martingaleRate G n S D)
(exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability)
:
∃ (K : ℝ),
1 ≤ K ∧ ∀ {X Y A B : Type} [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B]
(G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)),
0 < (Finset.univ \ D).card →
0 < repeatedPostselectionMass G n S D →
∀ (alpha gamma : ℝ),
0 < alpha →
alpha ≤ 1 →
0 < gamma →
uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) D < (1 - entangledValue G) / 2 →
∃ (rounded : Strategy G),
roundedWinningLowerBound (1 - entangledValue G) K alpha (martingaleRate G n S D)
(exactSourcePinskerRate G n S D + gamma) ≤ rounded.winProbability