Quantum parallel repetition, part 03 #

∃ (n : ℕ), 0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ (phase : Ω) (r s : Fin D), ‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s)) (tensorEmbezzlementTarget (work r)) - embezzlementState (N * n)‖ ^ 2 ≤ 2 * ε ^ 2 + 2 * ‖↑(work r) - ↑(work (representative phase (bucket phase r)))‖ ^ 2 + 4 * if bucket phase r = bucket phase s then 0 else 1

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCanonicalPrefixCleanup_sq {Ω : Type u_1} {I : Type u_2} [DecidableEq I] {N : ℕ} (grid : 0 < N) (bucket : Ω → Fin (N + 1) → I) (representative : Ω → I → Fin (N + 1)) (ε : ℝ) (precision : 0 < ε) :

∃ (n : ℕ), 0 < n ∧ ∃ (A : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)) (B : Ω → I → ↥(Matrix.unitaryGroup (Fin (N * n)) ℂ)), ∀ (phase : Ω) (r s : Fin (N + 1)), ‖localUnitaryAction (A phase (bucket phase r)) (B phase (bucket phase s)) (tensorEmbezzlementTarget (dSVCanonicalFailureUnitRankFamily N grid r)) - embezzlementState (N * n)‖ ^ 2 ≤ 2 * ε ^ 2 + 8 * |↑↑r - ↑↑(representative phase (bucket phase r))| / ↑(max 1 (min ↑r ↑(representative phase (bucket phase r)))) + 4 * if bucket phase r = bucket phase s then 0 else 1

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory {H : Type u_1} (B : ℕ) (history : EuclideanSpace ℂ (H × H)) :

EuclideanSpace ℂ ((Fin B × H) × Fin B × H)

The transcript representation for DSV density rational public bucket coherent phase.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory_apply {H : Type u_1} (B : ℕ) (history : EuclideanSpace ℂ (H × H)) (φ ψ : Fin B) (a b : H) :

(dSVDensityRationalPublicBucketCoherentPhaseHistory B history).ofLp ((φ, a), ψ, b) = (ePRState B).ofLp (φ, ψ) * history.ofLp (a, b)

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseHistory_apply_norm_sq {H : Type u_1} {B : ℕ} (positive : 0 < B) (history : EuclideanSpace ℂ (H × H)) (φ ψ : Fin B) (a b : H) :

‖(dSVDensityRationalPublicBucketCoherentPhaseHistory B history).ofLp ((φ, a), ψ, b)‖ ^ 2 = (if φ = ψ then (↑B)⁻¹ else 0) * ‖history.ofLp (a, b)‖ ^ 2

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseSigmaState {H : Type u_1} {m : ℕ} (B : ℕ) (history : EuclideanSpace ℂ (H × H)) (work : Fin B → H → H → EuclideanSpace ℂ (Fin m × Fin m)) :

EuclideanSpace ℂ (((_ : Fin B × H) × Fin m) × (_ : Fin B × H) × Fin m)

The quantum state representing DSV density rational public bucket coherent phase sigma.

Equations

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

Instances For

source

def QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseLocalUnitary {H : Type u_1} {I : Type u_2} [Fintype H] [DecidableEq H] {B D m : ℕ} (rank : H → Fin D) (bucket : Fin B → Fin D → I) (A : Fin B → I → ↥(Matrix.unitaryGroup (Fin m) ℂ)) :

↥(Matrix.unitaryGroup ((_ : Fin B × H) × Fin m) ℂ)

The unitary operator implementing DSV density rational public bucket coherent phase local.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicBucketCoherentPhaseSigmaReset_distance_sq {H : Type u_1} {I : Type u_2} [Fintype H] [DecidableEq H] {B D m : ℕ} (phase_positive : 0 < B) (history : EuclideanSpace ℂ (H × H)) (rankA rankB : H → Fin D) (bucket : Fin B → Fin D → I) (A C : Fin B → I → ↥(Matrix.unitaryGroup (Fin m) ℂ)) (work target : Fin B → H → H → EuclideanSpace ℂ (Fin m × Fin m)) :

‖dSVUniformDensityPhysicalAsyncSigmaContinuation (fun (q : Fin B × H) => A q.1 (bucket q.1 (rankA q.2))) (fun (q : Fin B × H) => C q.1 (bucket q.1 (rankB q.2))) (dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history work) - dSVDensityRationalPublicBucketCoherentPhaseSigmaState B history target‖ ^ 2 = (∑ φ : Fin B, ∑ a : H, ∑ b : H, ‖history.ofLp (a, b)‖ ^ 2 * ‖localUnitaryAction (A φ (bucket φ (rankA a))) (C φ (bucket φ (rankB b))) (work φ a b) - target φ a b‖ ^ 2) / ↑B

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_real_log_bound {r s : ℝ} (positive_r : 0 < r) (positive_s : 0 < s) :

min r s * |Real.log r - Real.log s| ≤ |r - s|

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_zeroSafe_nat_bound (r s : ℕ) :

min ↑r ↑s * |Real.log ↑(max 1 r) - Real.log ↑(max 1 s)| ≤ |↑r - ↑s|

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_zeroSafe_fin_bound {N : ℕ} (r s : Fin (N + 1)) :

min ↑↑r ↑↑s * |Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑s)| ≤ |↑↑r - ↑↑s|

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) :

ℕ

The DSV density rational public log rank fine label construction used in the quantum parallel- repetition argument.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel Q r = ⌊↑Q * Real.log ↑(max 1 ↑r)⌋₊

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight (B : ℕ) :

Fin B → ℝ

The probability weight for DSV density rational public log rank phase.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight B x✝ = 1 / ↑B

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankPhaseWeight_sum {B : ℕ} (positive : 0 < B) :

∑ phase : Fin B, dSVDensityRationalPublicLogRankPhaseWeight B phase = 1

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) :

Option ℕ

The DSV density rational public log rank bucket construction used in the quantum parallel- repetition argument.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket Q phase r = if ↑r = 0 then none else some ((QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel Q r + ↑phase) / B)

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket_fineLabel_sub_lt {N B : ℕ} (Q : ℕ) (phase : Fin B) (r s : Fin (N + 1)) (nonzero_r : ↑r ≠ 0) (nonzero_s : ↑s ≠ 0) (same : dSVDensityRationalPublicLogRankBucket Q phase r = dSVDensityRationalPublicLogRankBucket Q phase s) :

|↑(dSVDensityRationalPublicLogRankFineLabel Q r) - ↑(dSVDensityRationalPublicLogRankFineLabel Q s)| < ↑B

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRank_logCoordinate_nonneg {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) :

0 ≤ ↑Q * Real.log ↑(max 1 ↑r)

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankFineLabel_bounds {N : ℕ} (Q : ℕ) (r : Fin (N + 1)) :

↑(dSVDensityRationalPublicLogRankFineLabel Q r) ≤ ↑Q * Real.log ↑(max 1 ↑r) ∧ ↑Q * Real.log ↑(max 1 ↑r) < ↑(dSVDensityRationalPublicLogRankFineLabel Q r) + 1

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket_log_sub_lt {N B Q : ℕ} (positive_Q : 0 < Q) (phase : Fin B) (r s : Fin (N + 1)) (nonzero_r : ↑r ≠ 0) (nonzero_s : ↑s ≠ 0) (same : dSVDensityRationalPublicLogRankBucket Q phase r = dSVDensityRationalPublicLogRankBucket Q phase s) :

|Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑s)| < (↑B + 1) / ↑Q

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketFiber {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) :

Finset (Fin (N + 1))

The nonzero ranks assigned to the given logarithmic bucket and public phase.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketFiber Q phase label = {r : Fin (N + 1) | ↑r ≠ 0 ∧ QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucket Q phase r = label}

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative {N B : ℕ} (Q : ℕ) (phase : Fin B) (label : Option ℕ) :

Fin (N + 1)

The DSV density rational public log rank bucket representative construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_same {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) :

↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) ≠ 0 ∧ dSVDensityRationalPublicLogRankBucket Q phase (dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)) = dSVDensityRationalPublicLogRankBucket Q phase r

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_le {N B : ℕ} (Q : ℕ) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) :

dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r) ≤ r

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogRankBucketRepresentative_log_sub_lt {N B Q : ℕ} (positive_Q : 0 < Q) (phase : Fin B) (r : Fin (N + 1)) (nonzero : ↑r ≠ 0) :

|Real.log ↑(max 1 ↑r) - Real.log ↑(max 1 ↑(dSVDensityRationalPublicLogRankBucketRepresentative Q phase (dSVDensityRationalPublicLogRankBucket Q phase r)))| < (↑B + 1) / ↑Q

source

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase (S B : ℕ) :

Type

The type used to represent DSV density rational public multiscale phase in the exact sampling construction.

Equations

QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase S B = (Fin S → Fin B)

Instances For

source

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseIndex (S B : ℕ) :

Type

The type used to represent DSV density rational public multiscale phase index in the exact sampling construction.

Equations

QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseIndex S B = Fin (Fintype.card (QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhase S B))

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhase_card (S B : ℕ) :

Fintype.card (DSVDensityRationalPublicMultiscalePhase S B) = B ^ S

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhase_card_pos {S B : ℕ} (positive : 0 < B) :

0 < Fintype.card (DSVDensityRationalPublicMultiscalePhase S B)

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPrefixHarmonicSpectralOverlap {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) :

ℝ

The overlap quantity for DSV density rational prefix harmonic spectral.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPrefixHarmonicSpectralOverlap_nonneg {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) :

0 ≤ dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) :

ℂ

The overlap quantity for DSV density rational local spectral pair basis.

Equations

QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j = ↑(QuantumParallelRepetition.unitaryBasisOverlap ⋯.eigenvectorUnitary ⋯.eigenvectorUnitary) i j

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairBasisOverlap_norm_sq {d : ℕ} (ξ ζ : BipartiteUnitVector d) (i j : Fin d) :

‖dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j‖ ^ 2 = dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairHistory {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) :

EuclideanSpace ℂ (Fin d × Fin d)

The transcript representation for DSV density rational local spectral pair.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalLocalSpectralPairHistory_apply_norm_sq {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) (i j : Fin d) :

‖(dSVDensityRationalLocalSpectralPairHistory N ξ ζ).ofLp (i, j)‖ ^ 2 = dSVDensityRationalPrefixHarmonicSpectralOverlap ξ ζ i j / (↑d * ↑N)

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalMixedCanonicalCrossMatrix {d : ℕ} (N : ℕ) (ξ ζ : BipartiteUnitVector d) :

Matrix (DSVUniformDensityThresholdLocalIndex N d) (DSVUniformDensityThresholdLocalIndex N d) ℂ

The transposed eigenbasis overlap, repeated on each threshold block.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalMixedCanonicalRawSource {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) :

EuclideanSpace ℂ (DSVUniformDensityThresholdLocalIndex N d × DSVUniformDensityThresholdLocalIndex N d)

The source object for DSV density rational mixed canonical raw.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalRawSource_apply {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) (k l : Fin N) (i j : Fin d) :

(dSVDensityRationalMixedCanonicalRawSource w N ξ ζ).ofLp (⟨k, i⟩, ⟨l, j⟩) = if k = l ∧ dSVDensityRationalProjectiveThresholdBin w N k (⋯.eigenvalues i) = true ∧ dSVDensityRationalProjectiveThresholdBin w N l (⋯.eigenvalues j) = true then dSVDensityRationalLocalSpectralPairBasisOverlap ξ ζ i j else 0

source

theorem QuantumParallelRepetition.dSVDensityRationalMixedCanonicalSpectralOutcome_eq {d : ℕ} (w : ℝ) (N : ℕ) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalCanonicalPrefixSpectralOutcome w N ξ ζ = ‖sharedThresholdResourceRaw fun (x : Fin N) => 1‖⁻¹ • dSVDensityRationalMixedCanonicalRawSource w N ξ ζ

source

def QuantumParallelRepetition.dSVDensityRationalPublicLogBilateralPureTensor {ι : Type u_1} {κ : Type u_2} (v : EuclideanSpace ℂ (ι × ι)) (u : EuclideanSpace ℂ (κ × κ)) :

EuclideanSpace ℂ ((ι × κ) × ι × κ)

Tensor two bipartite vectors while grouping each player's indices together.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogBilateralPureTensor v u = WithLp.toLp 2 fun (q : (ι × κ) × ι × κ) => v.ofLp (q.1.1, q.2.1) * u.ofLp (q.1.2, q.2.2)

Instances For

source

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseHistoryLocalIndex (B N d L : ℕ) :

Type

The type used to represent DSV density rational public log phase history local index in the exact sampling construction.

Equations

QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L = (Fin B × QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePureSource (B N d L : ℕ) :

EuclideanSpace ℂ (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L)

The shared history state tensored with the public-phase EPR state.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseHarmonicPureSource (B N d L m : ℕ) :

EuclideanSpace ℂ ((DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m) × DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m)

Adjoin the harmonic embezzlement state to the public-phase history source.

Equations

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

Instances For

source

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex (B N d L : ℕ) :

Type

The public-phase label paired with the residual whole-history catalyst index.

Equations

QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex B N d L = (Fin B × QuantumParallelRepetition.DSVUniformDensityThresholdWholeHistoryCatalystIndex N d L)

Instances For

source

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetSplitEquiv (B N d L : ℕ) :

DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L ≃ Fin d × DSVDensityRationalPublicLogPhaseCatalystIndex B N d L

Separate the target coordinate while retaining the phase in the catalyst index.

Equations

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

Instances For

source

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseResidual (B N d L m : ℕ) :

ℕ

The DSV density rational public log phase residual construction used in the quantum parallel- repetition argument.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseResidual B N d L m = Fintype.card (QuantumParallelRepetition.DSVDensityRationalPublicLogPhaseCatalystIndex B N d L) * m

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv (B N d L m : ℕ) :

DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L × Fin m ≃ Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m)

The finite equivalence encoding DSV density rational public log phase target first index.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource (B N d L m : ℕ) :

EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m) × Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m))

The source object for DSV density rational public log phase target first prepared.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource_apply (B N d L m : ℕ) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) (i j : Fin m) :

(dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource B N d L m).ofLp ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((φ, a), i), (dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) ((ψ, b), j)) = (if φ = ψ then ↑(√↑B)⁻¹ else 0) * (dSVUniformDensityThresholdWholeHistorySharedState N d L).ofLp (a, b) * (embezzlementState m).ofLp (i, j)

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource_norm {B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) :

‖dSVDensityRationalPublicLogPhaseTargetFirstPreparedSource B N d L m‖ = 1

source

@[reducible, inline]

abbrev QuantumParallelRepetition.DSVDensityRationalPublicMultiscalePhaseHistoryLocalIndex (S B N d L : ℕ) :

Type

The type used to represent DSV density rational public multiscale phase history local index in the exact sampling construction.

Equations

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

Instances For

source

def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseResidual (S B N d L m : ℕ) :

ℕ

The DSV density rational public multiscale phase residual construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstIndexEquiv (S B N d L m : ℕ) :

DSVDensityRationalPublicMultiscalePhaseHistoryLocalIndex S B N d L × Fin m ≃ Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m)

The finite equivalence encoding DSV density rational public multiscale phase target first index.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource (S B N d L m : ℕ) :

EuclideanSpace ℂ (Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m) × Fin (d * dSVDensityRationalPublicMultiscalePhaseResidual S B N d L m))

The source object for DSV density rational public multiscale phase target first prepared.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource_norm {S B N d L m : ℕ} (phases : 0 < B) (grid : 0 < N) (dimension : 0 < d) (harmonic : 0 < m) :

‖dSVDensityRationalPublicMultiscalePhaseTargetFirstPreparedSource S B N d L m‖ = 1

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift (B N d L m : ℕ) (U : ↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)) :

↥(Matrix.unitaryGroup (Fin (d * dSVDensityRationalPublicLogPhaseResidual B N d L m)) ℂ)

The DSV density rational public log phase actual target first local lift construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift_apply (B N d L m : ℕ) (U : ↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)) (a b : DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) (i j : Fin m) :

↑(dSVDensityRationalPublicLogPhaseActualTargetFirstLocalLift B N d L m U) ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) (a, i)) ((dSVDensityRationalPublicLogPhaseTargetFirstIndexEquiv B N d L m) (b, j)) = if i = j then ↑U a b else 0

source

def QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary (B : ℕ) {N d L : ℕ} (U : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)) :

↥(Matrix.unitaryGroup (DSVDensityRationalPublicLogPhaseHistoryLocalIndex B N d L) ℂ)

The unitary operator implementing DSV density rational public log phase physical history.

Equations

QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary B U = ⟨Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 ↑U, ⋯⟩

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary_apply (B : ℕ) {N d L : ℕ} (U : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)) (φ ψ : Fin B) (a b : DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) :

↑(dSVDensityRationalPublicLogPhasePhysicalHistoryUnitary B U) (φ, a) (ψ, b) = if φ = ψ then ↑U a b else 0

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAcceptSet {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) :

Finset (Fin L)

The stages whose actual history coordinates satisfy their acceptance predicates.

Equations

QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAcceptSet accepted history = {j : Fin L | accepted j (history j.castSucc)}

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) :

Fin (L + 1)

The DSV density rational heterogeneous actual first accepted construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_prefix_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (j : Fin L) :

dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = j.succ ↔ accepted j (history j.castSucc) ∧ ∀ i < j, ¬accepted i (history i.castSucc)

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_zero_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) :

dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = 0 ↔ ∀ (i : Fin L), ¬accepted i (history i.castSucc)

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptEquiv {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) :

Equiv.Perm ((_ : Fin (L + 1)) × (Fin (L + 1) → β))

Swap the zero flag with the first accepted stage, retaining the history.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) :

↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × (Fin (L + 1) → β)) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual first accept.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_mulVec {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (_ : Fin (L + 1)) × (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) :

(↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec v ⟨flag, history⟩ = v ⟨(Equiv.swap 0 (dSVDensityRationalHeterogeneousActualFirstAccepted accepted history)) flag, history⟩

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_zeroFlag {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) :

(↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec (fun (q : (_ : Fin (L + 1)) × (Fin (L + 1) → β)) => if q.fst = 0 then v q.snd else 0) ⟨flag, history⟩ = if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then v history else 0

source

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyAccepted {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (j : Fin L) (atom : DSVUniformDensityThresholdLocalIndex N d) :

Prop

The DSV density rational heterogeneous actual copy accepted construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyCondition {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (flag i : Fin (L + 1)) (atom : β) :

Prop

The DSV density rational heterogeneous actual copy condition construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_allFlags_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (flag : Fin (L + 1)) :

dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = flag ↔ ∀ (i : Fin (L + 1)), dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i (history i)

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_sourceProduct {β : Type u_1} [Fintype β] {L : ℕ} (accepted : Fin L → β → Prop) (flag : Fin (L + 1)) (A D : Fin (L + 1) → β → ℂ) :

(∑ history : Fin (L + 1) → β, (∏ i : Fin (L + 1), A i (history i)) * if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then ∏ i : Fin (L + 1), D i (history i) else 0) = ∏ i : Fin (L + 1), ∑ atom : β, A i atom * if dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i atom then D i atom else 0

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalLocalUnitary {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (U : ↥(Matrix.unitaryGroup β ℂ)) :

↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × (Fin (L + 1) → β)) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual physical local.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAliceUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) :

↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual alice.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualBobUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ζ : BipartiteUnitVector d) :

↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

The unitary operator implementing DSV density rational heterogeneous actual bob.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

EuclideanSpace ℂ (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

The quantum state representing DSV density rational heterogeneous actual physical.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState_norm {S N d L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

‖dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ‖ = 1

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) :

ℝ

The finite outcome encoding for DSV density rational heterogeneous physical stage.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

ℝ

The DSV density rational heterogeneous physical stage continue construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageSuccess {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

ℝ

The DSV density rational heterogeneous physical stage success construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

ℝ

The DSV density rational heterogeneous physical stage asynchronous construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) :

0 ≤ dSVDensityRationalHeterogeneousPhysicalStageOutcome N width schedule ξ ζ k alice bob

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k = 1

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) :

dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k = dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

ℝ

The DSV density rational heterogeneous physical survival construction used in the quantum parallel-repetition argument.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) :

0 ≤ dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

ℝ

The total probability mass of DSV density rational heterogeneous physical stopped success.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

ℝ

The total probability mass of DSV density rational heterogeneous physical stopped asynchronous.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

ℝ

The total probability mass of DSV density rational heterogeneous physical terminal.

Equations

QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ L

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStopped_mass_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = 1

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ = ∑ k : Fin L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑k * dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

0 ≤ dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

0 ≤ dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_lower {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) :

1 / (2 * (width (schedule k) + 1) * ↑d) ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_escape_ge_diagonal {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) :

dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_relative_diagonal_le {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) :

dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (width (schedule k) + 1) * (↑d / ↑N)

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedEscape_budget {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

∑ k ∈ Finset.range L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k * (dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k) ≤ 1

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_le_targetDistance {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (upper : ∀ (s : Fin S), width s ≤ W) (W_nonnegative : 0 ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (W + 1) * (↑d / ↑N)

source

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate (d : ℕ) (W : ℝ) :

ℝ

The error rate associated with DSV density rational heterogeneous physical uniform escape.

Equations

QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W = 1 / (2 * (W + 1) * ↑d)

Instances For

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_pos {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) :

0 < dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_le_half {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) :

dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ 1 / 2

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_ge_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) :

dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue_le_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) :

dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑k ≤ 1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_pow {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysical_exists_positive_horizon {d : ℕ} (dimension : 0 < d) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (precision : 0 < ε) :

∃ (L : ℕ), 0 < L ∧ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2

source

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_horizon {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (tail : (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) :

dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ ε ^ 2

source

noncomputable def QuantumParallelRepetition.fairPartitionWeight (α : Type u_2) [Fintype α] :

ℝ

The probability weight for fair partition.

Equations

QuantumParallelRepetition.fairPartitionWeight α = (2 ^ Fintype.card α)⁻¹

Instances For

source

noncomputable def QuantumParallelRepetition.reversePartitionWeight {α : Type u_1} [Fintype α] (s : Finset α) :

ℝ

The probability weight for reverse partition.

Equations

QuantumParallelRepetition.reversePartitionWeight s = QuantumParallelRepetition.fairPartitionWeight α * (2 * ↑s.card / ↑(Fintype.card α))

Instances For

source

noncomputable def QuantumParallelRepetition.forwardMarkedPartitionWeight (α : Type u_2) [Fintype α] :

ℝ

The probability weight for forward marked partition.

Equations

QuantumParallelRepetition.forwardMarkedPartitionWeight α = 2 * QuantumParallelRepetition.fairPartitionWeight α / ↑(Fintype.card α)

Instances For

source

noncomputable def QuantumParallelRepetition.reverseMarkedPartitionWeight {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (i : α) :

ℝ

The probability weight for reverse marked partition.

Equations

QuantumParallelRepetition.reverseMarkedPartitionWeight s i = if i ∈ s then QuantumParallelRepetition.reversePartitionWeight s / ↑s.card else 0

Instances For

source

theorem QuantumParallelRepetition.fairPartitionWeight_pos {α : Type u_1} [Fintype α] :

0 < fairPartitionWeight α

source

theorem QuantumParallelRepetition.fairPartitionWeight_nonneg {α : Type u_1} [Fintype α] :

0 ≤ fairPartitionWeight α

source

theorem QuantumParallelRepetition.fairPartitionWeight_sum {α : Type u_1} [Fintype α] :

∑ _s : Finset α, fairPartitionWeight α = 1

source

theorem QuantumParallelRepetition.reversePartitionWeight_nonneg {α : Type u_1} [Fintype α] (s : Finset α) :

0 ≤ reversePartitionWeight s

source

@[simp]

theorem QuantumParallelRepetition.reversePartitionWeight_empty {α : Type u_1} [Fintype α] :

reversePartitionWeight ∅ = 0

source

theorem QuantumParallelRepetition.reversePartitionWeight_pos_iff {α : Type u_1} [Fintype α] (hα : 0 < Fintype.card α) (s : Finset α) :

0 < reversePartitionWeight s ↔ s.Nonempty

source

theorem QuantumParallelRepetition.reverseMarkedPartitionWeight_eq_forward {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {i : α} (hi : i ∈ s) :

reverseMarkedPartitionWeight s i = forwardMarkedPartitionWeight α

source

theorem QuantumParallelRepetition.bornTracePairing_le_one_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hFcomplement : (1 - F).PosSemidef) :

((bornTracePairing ρ.matrix) F) 1 ≤ 1

source

theorem QuantumParallelRepetition.matrixLogEntropy_born_lower_bound_right {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) :

-((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

source

theorem QuantumParallelRepetition.fullHistoryWeight_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 L : Finset (Fin n)) :

∑ h : FullSubsetHistory X Y n D L, fullHistoryWeight G h = 1

source

theorem QuantumParallelRepetition.fullHistoryWinIndicator_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) :

fullHistoryWinIndicator G h α β ≤ 1

source

def QuantumParallelRepetition.fullHistoryAnswerCount {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) :

ℝ

The full history answer count construction used in the quantum parallel-repetition argument.

Equations

QuantumParallelRepetition.fullHistoryAnswerCount D = ↑(Fintype.card (↥D → A)) * ↑(Fintype.card (↥D → B))

Instances For

source

theorem QuantumParallelRepetition.fullHistoryAnswerCount_eq {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) :

fullHistoryAnswerCount D = ↑(Fintype.card A) ^ D.card * ↑(Fintype.card B) ^ D.card

source

@[reducible, inline]

abbrev QuantumParallelRepetition.FullHistoryEntropyAtom (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) (n : ℕ) (D L : Finset (Fin n)) :

Type (max (max u_6 u_5) u_8 u_7)

The type used to represent full history entropy atom in the exact sampling construction.

Equations

QuantumParallelRepetition.FullHistoryEntropyAtom X Y A B n D L = (QuantumParallelRepetition.FullSubsetHistory X Y n D L × (↥D → A) × (↥D → B))

Instances For

source

def QuantumParallelRepetition.fullHistoryAtomCountingWeight {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) :

ℝ

The probability weight for full history atom counting.

Equations

QuantumParallelRepetition.fullHistoryAtomCountingWeight G D L t = QuantumParallelRepetition.fullHistoryWeight G t.1 * QuantumParallelRepetition.fullHistoryWinIndicator G t.1 t.2.1 t.2.2

Instances For

source

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

ℝ

The total probability mass of full history atom born.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_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 L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) :

0 ≤ fullHistoryAtomCountingWeight G D L t

source

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) :

0 ≤ fullHistoryAtomBornMass G n S D L t

source

theorem QuantumParallelRepetition.bornTracePairing_contractions_le_one {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) :

((bornTracePairing ρ.matrix) F) G ≤ 1

source

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) :

fullHistoryAtomBornMass G n S D L t ≤ 1

source

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) :

∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t ≤ fullHistoryAnswerCount D

source

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) :

∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * fullHistoryAtomBornMass G n S D L t = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)

source

theorem QuantumParallelRepetition.fullHistoryAtomEntropy_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 L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) :

∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * (fullHistoryAtomBornMass G n S D L t).negMulLog ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

source

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_lower_bound {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) :

-((strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))) ≤ fullHistoryAliceEntropyPotential G n S D L

source

structure QuantumParallelRepetition.FullCoordinateRevealHistory (X : Type u_1) (Y : Type u_2) (n : ℕ) (D L : Finset (Fin n)) (i : Fin n) :

Type (max u_1 u_2)

A transcript in which one additional coordinate is being revealed.

aliceConditioned : ↥D → X
Alice's conditioned part of the transcript.
bobConditioned : ↥D → Y
Bob's conditioned part of the transcript.
aliceRevealed : ↥L → X
Alice's already revealed questions.
bobRemaining : ↥(fullHistoryRemaining n D (insert i L)) → Y
Bob's questions outside the revealed coordinates.

Instances For

source

theorem QuantumParallelRepetition.FullCoordinateRevealHistory.ext {X : Type u_1} {Y : Type u_2} {n : ℕ} {D L : Finset (Fin n)} {i : Fin n} {x y : FullCoordinateRevealHistory X Y n D L i} (aliceConditioned : x.aliceConditioned = y.aliceConditioned) (bobConditioned : x.bobConditioned = y.bobConditioned) (aliceRevealed : x.aliceRevealed = y.aliceRevealed) (bobRemaining : x.bobRemaining = y.bobRemaining) :

x = y

source

@[instance_reducible]

instance QuantumParallelRepetition.instFintypeFullCoordinateRevealHistory {X✝ : Type u_1} {Y✝ : Type u_2} {n✝ : ℕ} {D✝ L✝ : Finset (Fin n✝)} {i✝ : Fin n✝} [Fintype X✝] [Fintype Y✝] :

Fintype (FullCoordinateRevealHistory X✝ Y✝ n✝ D✝ L✝ i✝)

Equations

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

source

theorem QuantumParallelRepetition.fullHistoryRemaining_insert_subset {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) :

fullHistoryRemaining n D (insert i L) ⊆ fullHistoryRemaining n D L

source

def QuantumParallelRepetition.fullCoordinateOldHistory {X : Type u_1} {Y : Type u_2} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) :

FullSubsetHistory X Y n D L

The transcript representation for full coordinate old.

Equations

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

Instances For

source

def QuantumParallelRepetition.fullCoordinateNewHistory {X : Type u_1} {Y : Type u_2} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) :

FullSubsetHistory X Y n D (insert i L)

The transcript representation for full coordinate new.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.finsetSubtype_prod_insert {ι : Type u_1} {T : Type u_2} [DecidableEq ι] [CommMonoid T] (s : Finset ι) (i : ι) (hi : i ∉ s) (f : ↥(insert i s) → T) :

∏ j : ↥(insert i s), f j = f ⟨i, ⋯⟩ * ∏ j : ↥s, f ⟨↑j, ⋯⟩

source

theorem QuantumParallelRepetition.fullHistoryRemaining_prod_split {n : ℕ} {T : Type u_1} [CommMonoid T] (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : ↥(fullHistoryRemaining n D L) → T) :

∏ j : ↥(fullHistoryRemaining n D L), f j = f ⟨i, ⋯⟩ * ∏ j : ↥(fullHistoryRemaining n D (insert i L)), f ⟨↑j, ⋯⟩

source

def QuantumParallelRepetition.fullCoordinateBaseWeight {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) :

ℝ

The probability weight for full coordinate base.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.fullCoordinateBaseWeight_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 L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) :

0 ≤ fullCoordinateBaseWeight G D L i h

source

theorem QuantumParallelRepetition.fullCoordinateOldHistory_weight {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) :

fullHistoryWeight G (fullCoordinateOldHistory D L i h y) = fullCoordinateBaseWeight G D L i h * G.marginalY y

source

theorem QuantumParallelRepetition.fullCoordinateNewHistory_weight {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) :

fullHistoryWeight G (fullCoordinateNewHistory D L i h x) = fullCoordinateBaseWeight G D L i h * G.marginalX x

source

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_difference_gram_apply {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) (i j : d) :

((finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b)) i j = ∑ r : d, inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - ensemblePurificationSubspaceEntry F M positive hM b r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - ensemblePurificationSubspaceEntry F M positive hM b r j)

source

theorem QuantumParallelRepetition.ensemblePurificationSubspaceEntry_pair_difference_inner_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) (r i j : d) :

inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - ensemblePurificationSubspaceEntry F M positive hM b r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - ensemblePurificationSubspaceEntry F M positive hM b r j) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s r i - spectralPurificationFilter (F b) ⋯ s r i) * (spectralPurificationFilter (F a) ⋯ s r j - spectralPurificationFilter (F b) ⋯ s r j)

source

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_difference_gram_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) :

(finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s) * (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s)

source

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) :

finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB = finiteLocalPurificationVector S (KA - KA') KB

source

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB KB' : Matrix eB S.Bob ℂ) :

finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB' = finiteLocalPurificationVector S KA (KB - KB')

source

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) :

‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB‖ ^ 2 = ((bornTracePairing S.state.matrix) ((KA - KA').conjTranspose * (KA - KA'))) (KB.conjTranspose * KB)

source

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB KB' : Matrix eB S.Bob ℂ) :

‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB'‖ ^ 2 = ((bornTracePairing S.state.matrix) (KA.conjTranspose * KA)) ((KB - KB').conjTranspose * (KB - KB'))

source

noncomputable def QuantumParallelRepetition.fullCoordinateAliceQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (x : X) :

Matrix S.Alice S.Alice ℂ

Alice's history filter after revealing the selected coordinate's question.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.fullCoordinateAliceMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (y : Y) :

Matrix S.Alice S.Alice ℂ

Alice's history filter before the new question is revealed.

Equations

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

Instances For

source

noncomputable def QuantumParallelRepetition.fullCoordinateBobQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (β : ↥D → B) (y : Y) :

Matrix S.Bob S.Bob ℂ

Bob's history filter for the selected question and the previously revealed history.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.matrixLogEntropy_weighted_jensen_posSemidef {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) (positive : ∀ (i : ι), (F i).PosSemidef) :

(∑ i : ι, weight i • cfc (fun (z : ℝ) => z * Real.log z) (F i) - cfc (fun (z : ℝ) => z * Real.log z) M).PosSemidef

source

theorem QuantumParallelRepetition.conditionalAlice_matrixLogEntropy_gap_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {d : Type u_5} [Fintype d] [DecidableEq d] (G : Game X Y A B) (H : X → Matrix d d ℂ) (hH : ∀ (x : X), (H x).PosSemidef) (y : Y) (hy : 0 < G.marginalY y) :

(conditionalAliceAverage G (fun (x : X) => cfc (fun (z : ℝ) => z * Real.log z) (H x)) y - cfc (fun (z : ℝ) => z * Real.log z) (conditionalAliceAverage G H y)).PosSemidef

source

noncomputable def QuantumParallelRepetition.fullCoordinateAliceEntropyIncrement {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) :

ℝ

The averaged entropy increment between Alice's question and mean filters.

Equations

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

Instances For

source

def QuantumParallelRepetition.fullCoordinateBaseWinIndicator {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) :

ℝ

The indicator function for full coordinate base win.

Equations

QuantumParallelRepetition.fullCoordinateBaseWinIndicator G D L i r α β = if ∀ (j : ↥D), G.predicate (r.aliceConditioned j) (r.bobConditioned j) (α j) (β j) = true then 1 else 0

Instances For

source

theorem QuantumParallelRepetition.fullCoordinateBaseWinIndicator_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 L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) :

0 ≤ fullCoordinateBaseWinIndicator G D L i r α β

source

theorem QuantumParallelRepetition.fullCoordinateOldHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (y : Y) (α : ↥D → A) (β : ↥D → B) :

fullHistoryWinIndicator G (fullCoordinateOldHistory D L i r y) α β = fullCoordinateBaseWinIndicator G D L i r α β

source

theorem QuantumParallelRepetition.fullCoordinateNewHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (α : ↥D → A) (β : ↥D → B) :

fullHistoryWinIndicator G (fullCoordinateNewHistory D L i r x) α β = fullCoordinateBaseWinIndicator G D L i r α β

source

theorem QuantumParallelRepetition.fullCoordinate_three_sum_rotate {I : Type u_5} {J : Type u_6} {K : Type u_7} {T : Type u_8} [Fintype I] [Fintype J] [Fintype K] [AddCommMonoid T] (f : I → J → K → T) :

∑ i : I, ∑ j : J, ∑ k : K, f i j k = ∑ j : J, ∑ k : K, ∑ i : I, f i j k

source

theorem QuantumParallelRepetition.fullCoordinateOldHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D L → T) :

∑ h : FullSubsetHistory X Y n D L, f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ y : Y, f (fullCoordinateOldHistory D L i r y)

source

theorem QuantumParallelRepetition.fullCoordinateNewHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D (insert i L) → T) :

∑ h : FullSubsetHistory X Y n D (insert i L), f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ x : X, f (fullCoordinateNewHistory D L i r x)

source

theorem QuantumParallelRepetition.fullCoordinateWeightedOldSum {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D L → (↥D → A) → (↥D → B) → ℝ) :

∑ h : FullSubsetHistory X Y n D L, ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ y : Y, G.marginalY y * value (fullCoordinateOldHistory D L i r y) α β

source

theorem QuantumParallelRepetition.fullCoordinateWeightedNewSum {X : Type u_1} {Y : Type u_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 L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D (insert i L) → (↥D → A) → (↥D → B) → ℝ) :

∑ h : FullSubsetHistory X Y n D (insert i L), ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ x : X, G.marginalX x * value (fullCoordinateNewHistory D L i r x) α β

source

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

ℝ

The information increment contributed by full coordinate alice total entropy.

Equations

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

Instances For

source

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_increment {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) :

fullHistoryAliceEntropyPotential G n S D (insert i L) - fullHistoryAliceEntropyPotential G n S D L = fullCoordinateAliceTotalEntropyIncrement G n S D L i

source

theorem QuantumParallelRepetition.fullCoordinateAliceTotalEntropyIncrement_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) :

0 ≤ fullCoordinateAliceTotalEntropyIncrement G n S D L i

Documentation

LeanPool.QuantumParallelRepetition.Part03

Quantum parallel repetition, part 03 #