Documentation

MIPRE.Background.Repetition.CommutingRepetition.OTQCS.Assembly

Transport along a tracial extension #

theorem CommutingRepetition.TracialExtension.tracialPairLaw_map {N : StdTracialAlgebra} (ext : TracialExtension N) {S T A B : Type} (u : STN.H) (E : SAN.A) (F : TBN.A) (s : S) (t : T) (a : A) (b : B) :
tracialPairLaw ext.N' (fun (s : S) (t : T) => ext.U (u s t)) (fun (s : S) (a : A) => ext.emb (E s a)) (fun (t : T) (b : B) => ext.emb (F t b)) s t a b = tracialPairLaw N u E F s t a b

The pair law is invariant under the spatial extension: U intertwines the left and right actions and preserves inner products.

theorem CommutingRepetition.TracialExtension.piAlignment_map {N : StdTracialAlgebra} (ext : TracialExtension N) {S T : Type} [Fintype S] [Fintype T] (π : ST) (u : STN.H) (xv : SN.H) (yv : TN.H) :
(piAlignment π (fun (s : S) (t : T) => ext.U (u s t)) (fun (s : S) => ext.U (xv s)) fun (t : T) => ext.U (yv t)) = piAlignment π u xv yv

The alignment defect is invariant under the isometry U.

theorem CommutingRepetition.TracialExtension.emb_sum_eq_one {N : StdTracialAlgebra} (ext : TracialExtension N) {A : Type u_1} [Fintype A] (E : AN.A) (hE : a : A, E a = 1) :
a : A, ext.emb (E a) = 1

ℓ¹ toolkit #

theorem CommutingRepetition.l1_le_two {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p q : AB) (hp : ∀ (a : A) (b : B), 0 p a b) (hq : ∀ (a : A) (b : B), 0 q a b) (hpsum : a : A, b : B, p a b = 1) (hqsum : a : A, b : B, q a b = 1) :
a : A, b : B, |p a b - q a b| 2

Two probability laws on a finite product are at unhalved ℓ¹ distance at most 2.

theorem CommutingRepetition.l1_le_of_decomposition {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (qhat qz q r : AB) (cm : ) (hcm0 : 0 cm) (hr : ∀ (a : A) (b : B), 0 r a b) (hrsum : a : A, b : B, r a b = 1 - cm) (hq : ∀ (a : A) (b : B), 0 q a b) (hqsum : a : A, b : B, q a b = 1) (hdec : ∀ (a : A) (b : B), qhat a b = cm * qz a b + r a b) :
a : A, b : B, |qhat a b - q a b| a : A, b : B, |qz a b - q a b| + 2 * (1 - cm)

ℓ¹ conversion of a branch decomposition q̂ = cm · q_z + r with nonnegative remainder of mass 1 − cm against a probability law q: ‖q̂ − q‖₁ ≤ ‖q_z − q‖₁ + 2(1 − cm) (06_otqcs.tex, the display deriving eq otqcs-main: "on a bad branch the unhalved ℓ¹ cost is at most 2").

theorem CommutingRepetition.sum_abs_tracialPairLaw_sub_le (N : StdTracialAlgebra) {S T A B : Type} [Fintype A] [Fintype B] (E : SAN.A) (F : TBN.A) (hE : ∀ (s : S) (a : A), IsPosElem (E s a)) (hF : ∀ (t : T) (b : B), IsPosElem (F t b)) (hEs : ∀ (s : S), a : A, E s a = 1) (hFs : ∀ (t : T), b : B, F t b = 1) (s : S) (t : T) {z w : N.H} (hz : z = 1) (hw : w = 1) :
a : A, b : B, |tracialPairLaw N (fun (x : S) (x_1 : T) => z) E F s t a b - tracialPairLaw N (fun (x : S) (x_1 : T) => w) E F s t a b| 2 * z - w

Vector-to-ℓ¹ for pair laws (06_otqcs.tex, eq vector-to-l1): two unit vectors' pair laws under one pair of full POVMs differ in unhalved ℓ¹ by at most 2‖z − w‖₂ — the ℓ¹-POVM estimate sum_abs_re_inner_effect_sub_le applied to the commuting product effects L(A_s^a) R(B_t^b).

The finite bad bound at the chosen trial count #

theorem CommutingRepetition.commonMass_nonneg (a b c Z : ) (R : ) (hZ : 0 < Z) (hc : 0 c) (hle : a + b - c Z) :
0 commonMass a b c Z R
theorem CommutingRepetition.two_exp_ceil_le (Z ξ : ) (hZ : 0 < Z) ( : 0 < ξ) :
2 * Real.exp (-2 * Z * Real.log (2 / ξ ^ 2)⌉₊ / (2 * Z)) ξ ^ 2

The trial count R = ⌈2 Z log(2/ξ²)⌉ makes the exhaustion tail 2 e^{−R/(2Z)} ≤ ξ² (06_otqcs.tex, eq R-choice).

theorem CommutingRepetition.one_sub_commonMass_le (a b c Z ξ : ) (hZ : 0 < Z) ( : 0 < ξ) (ha : 1 / 2 a) (hb : 1 / 2 b) (hc : 0 c) (hca : c a) (hcb : c b) (hle : a + b - c Z) :
1 - commonMass a b c Z 2 * Z * Real.log (2 / ξ ^ 2)⌉₊ 2 * (a + b - 2 * c) + ξ ^ 2

1 − cm ≤ 2Γ + ξ² at R = ⌈2 Z log(2/ξ²)⌉ (eq finite-bad + eq R-choice).

The selected-state chain (eq selected-state-preopt) #

theorem CommutingRepetition.selSharp_normSq {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : } (B : Fin mSet ) (t : Fin m) (hB : IsBandFamily B t) :
N.ι (selSharp dB B t) ^ 2 = pairMassB dB B t

‖k♯‖₂² = b (06_otqcs.tex, eq rounded-y: the normalization of ).

theorem CommutingRepetition.selSharp_norm {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : } (B : Fin mSet ) (t : Fin m) (hB : IsBandFamily B t) :
N.ι (selSharp dB B t) = (pairMassB dB B t)
theorem CommutingRepetition.selYTilde_sub_le {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : } (B : Fin mSet ) (t : Fin m) (hB : IsBandFamily B t) (hy : y = 1) (hb : 0 < pairMassB dB B t) :
selYTilde dB B t - y 2 * N.ι (selSharp dB B t) - dB.hvec

The normalization inequality for the rounded polar vector: ‖ỹ_t − y_t‖₂ ≤ 2 ‖k_t^♯ − k_t‖₂ (06_otqcs.tex, eq normalization-inequality applied to ỹ = b^{−1/2} k♯ v, y = k v, with v a right isometry on the relevant vectors — Rop_v_norm).

theorem CommutingRepetition.hvec_sub_selCutVec_le {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : } (B : Fin mSet ) (t : Fin m) (hB : IsBandFamily B t) (hy : y = 1) {L H ρ : } (hL : 0 < L) (hLH : L < H) (hU : ⋃ (j : Fin m), B j = Set.Icc L H) (htail : (b : ) in Set.Ioi H, b ^ 2 dB.μ ρ) :
dB.hvec - selCutVec dB B (ρ + L ^ 2)

‖k − k^{cut}‖₂ ≤ √(ρ + L²) when the bands cover [L, H] and the high tail beyond H is at most ρ (06_otqcs.tex, eq rounding-tails).

theorem CommutingRepetition.selState_sub_le {N : StdTracialAlgebra} {x y : N.H} (dA : SpectralData N x) (dB : SpectralData N y) (Jd : JointSpectralData dA dB) {m : } (B : Fin mSet ) (t : Fin m) (hB : IsBandFamily B t) (hy : y = 1) (ha : 1 / 2 pairMassA dA B t) (hb : 1 / 2 pairMassB dB B t) (r : ) (hr : 1 r) (hband : ∀ (j : Fin m), B jSet.Icc (t j / r) (t j)) (κ : ) (hcut : dB.hvec - selCutVec dB B κ) (u : N.H) :
selState dA dB Jd B t - u 2 * (pairMassA dA B t + pairMassB dB B t - 2 * pairCross dA dB Jd B t) + 2 * (r - 1 + κ) + y - u

The selected-state chain (06_otqcs.tex, eq selected-state-preopt): ‖z_{st} − u_{st}‖₂ ≤ 2√Γ_{st} + 2((r − 1) + κ) + ‖y_t − u_{st}‖₂, where r − 1 = α bounds the rounding ‖k♯ − k^{cut}‖ and κ the cut ‖k^{cut} − k‖.

Hypotheses of the grid slab read off a joint spectral package #

theorem CommutingRepetition.JointSpectralData.ae_nonneg {N : StdTracialAlgebra} {x y : N.H} {dA : SpectralData N x} {dB : SpectralData N y} (Jd : JointSpectralData dA dB) :
∀ᵐ (p : × ) Jd.ν, 0 p.1 0 p.2
theorem CommutingRepetition.JointSpectralData.setIntegral_fst_sq_tail {N : StdTracialAlgebra} {x y : N.H} {dA : SpectralData N x} {dB : SpectralData N y} (Jd : JointSpectralData dA dB) (H : ) :
(p : × ) in {q : × | H < q.1}, p.1 ^ 2 Jd.ν = (b : ) in Set.Ioi H, b ^ 2 dA.μ
theorem CommutingRepetition.JointSpectralData.setIntegral_snd_sq_tail {N : StdTracialAlgebra} {x y : N.H} {dA : SpectralData N x} {dB : SpectralData N y} (Jd : JointSpectralData dA dB) (H : ) :
(p : × ) in {q : × | H < q.2}, p.2 ^ 2 Jd.ν = (b : ) in Set.Ioi H, b ^ 2 dB.μ

Averaging and the parameter arithmetic #

theorem CommutingRepetition.sum_mul_sqrt_le_sqrt {ι : Type u_1} [Fintype ι] (π g : ι) ( : ∀ (i : ι), 0 π i) (hπ1 : i : ι, π i = 1) (hg : ∀ (i : ι), 0 g i) :
i : ι, π i * (g i) (∑ i : ι, π i * g i)

Jensen for the square root under a probability weight: ∑ πᵢ √gᵢ ≤ √(∑ πᵢ gᵢ) ("this is the sole square-root conversion in the proof").

theorem CommutingRepetition.norm_sub_sq_le_two_mul {E : Type u_1} [SeminormedAddCommGroup E] (x y u : E) :
x - y ^ 2 2 * u - x ^ 2 + 2 * u - y ^ 2

‖x − y‖² ≤ 2‖u − x‖² + 2‖u − y‖² (the step behind eq Dbar-Delta).

theorem CommutingRepetition.rpow_sixth_pow (Δ : ) ( : 0 Δ) :
(Δ ^ (1 / 6)) ^ 6 = Δ

(Δ^{1/6})^6 = Δ.

theorem CommutingRepetition.final_arith (C₀ δ ξ Γbar Ybar Dbar : ) (hC₀ : 0 < C₀) ( : 0 δ) ( : 0 < ξ) ( : δ + ξ 1 / 2) ( : Γbar C₀ * (Dbar + Dbar / (δ + ξ) + ξ ^ 2 / 32 + (ξ / 8) ^ 2)) (hD : Dbar 4 * δ ^ 6) (hY : Ybar δ ^ 6) :
4 * Γbar + 4 * (δ + ξ) + 4 * (ξ ^ 2 / 32 + (ξ / 8) ^ 2) + 2 * Ybar + 4 * Γbar + 2 * ξ ^ 2 (4 * (6 * C₀) + 24 * C₀ + 8) * (δ + ξ)

The final constant bookkeeping in the nontrivial range δ + ξ ≤ 1/2, with δ = Δ^{1/6}, ρ = ξ²/32, L = ξ/8, α = δ + ξ (06_otqcs.tex, eqs cutoff-choice, alpha-choice, alpha-optimization, Dbar-Delta): the averaged per-pair bound is at most a universal multiple of δ + ξ.

theorem CommutingRepetition.average_bound {ι : Type u_1} [Fintype ι] (π Γ Y : ι) (C₀ δ ξ Dbar : ) ( : ∀ (i : ι), 0 π i) (hπ1 : i : ι, π i = 1) ( : ∀ (i : ι), 0 Γ i) (hY : ∀ (i : ι), 0 Y i) (hℓ : ∀ (i : ι), i 4 * (Γ i) + 4 * (δ + ξ) + 4 * (ξ ^ 2 / 32 + (ξ / 8) ^ 2) + 2 * (Y i) + 4 * Γ i + 2 * ξ ^ 2) (hC₀ : 0 < C₀) ( : 0 δ) ( : 0 < ξ) ( : δ + ξ 1 / 2) (hΓavg : i : ι, π i * Γ i C₀ * (Dbar + Dbar / (δ + ξ) + ξ ^ 2 / 32 + (ξ / 8) ^ 2)) (hD : Dbar 4 * δ ^ 6) (hYavg : i : ι, π i * Y i δ ^ 6) :
i : ι, π i * i (4 * (6 * C₀) + 24 * C₀ + 8) * (δ + ξ)

Averaging the per-pair bound (06_otqcs.tex, the final display of the proof of thm otqcs): if every pair obeys the selected-state/bad-branch bound in terms of its grid disagreement Γᵢ and its alignment Yᵢ = ‖y − u‖², and the π-averages obey eqs common-shift and Dbar-Delta, then the π-average of the ℓ¹ errors is at most a universal multiple of δ + ξ, δ = Δ^{1/6}.

The trivial resource (degenerate range) #

noncomputable def CommutingRepetition.trivialResource (S T A B : Type) [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (N : StdTracialAlgebra) :

The trivial sampling resource of the degenerate range α₀ > 1/2 (06_otqcs.tex, proof of thm otqcs: "take explicitly N̂ = N, Ω = 1, Â_s^{a₀} = B̂_t^{b₀} = 1 and set all other output effects to zero").

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