The Hilbert--Schmidt closeness calculus

Every soundness argument in the pipeline compares two families of operators in the state-dependent distance ∑_a ‖(M_a - N_a)|ψ⟩‖² and then passes from closeness of the families to closeness of the values, losing a square root. For a synchronous strategy the state is the normalized trace itself, so that distance is the normalized Hilbert--Schmidt distance of MIPRE/Foundations/Distances.lean, and the whole calculus follows from Cauchy--Schwarz for MIPRE.hsInner.

This file is that calculus, and nothing about games.

• MIPRE.ntr — the real part of the normalized trace Tr(M)/d, with the identities the arguments use: additive, tracial (ntr_mul_comm), ntr 1 = 1;
• hsNormSq_add, hsNormSq_sub — the parallelogram expansion, which is where the cross term 2⟨A, B⟩ that Cauchy--Schwarz then bounds comes from;
• re_hsInner_le, abs_re_hsInner_le — Cauchy--Schwarz for the normalized Hilbert--Schmidt inner product;
• sum_abs_re_hsInner_le — Cauchy--Schwarz once more, over a finite index set: the form the arguments actually use, with the two sums of squared norms on the right;
• sum_mul_sqrt_le — the averaging step 𝔼 √f ≤ √(𝔼 f), again Cauchy--Schwarz.

Implementation notes

hsInner A B = τ(Aᴴ B) is the inner product of a genuine inner product space (Mathlib's Matrix.toMatrixInnerProductSpace at the identity), but that structure is a noncomputable def rather than an instance, so using it would mean carrying letI through every statement. Cauchy--Schwarz is instead proved here from the entrywise formula and Real.sum_sqrt_mul_sqrt_le, which is the same proof and costs one lemma.

The normalized trace as a real number

noncomputable def MIPRE.ntr {n : Type u_1} [Fintype n] (M : Matrix n n ℂ) : ℝ

The real part of the dimension-normalized trace, τ(M) = Tr(M)/d. Outcome probabilities of a synchronous strategy are values of this, and so is every quantity the closeness calculus manipulates.

Equations

• MIPRE.ntr M = M.trace.re / ↑(Fintype.card n)

@[simp]

theorem MIPRE.ntr_zero {n : Type u_1} [Fintype n] : ntr 0 = 0

theorem MIPRE.ntr_fin (d : ℕ) (M : Matrix (Fin d) (Fin d) ℂ) : ntr M = M.trace.re / ↑d

theorem MIPRE.ntr_add {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : ntr (A + B) = ntr A + ntr B

theorem MIPRE.ntr_sub {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : ntr (A - B) = ntr A - ntr B

theorem MIPRE.ntr_neg {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : ntr (-A) = -ntr A

theorem MIPRE.ntr_sum {n : Type u_1} [Fintype n] {ι : Type u_2} (s : Finset ι) (f : ι → Matrix n n ℂ) : ntr (∑ i ∈ s, f i) = ∑ i ∈ s, ntr (f i)

theorem MIPRE.ntr_mul_comm {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : ntr (A * B) = ntr (B * A)

theorem MIPRE.ntr_conjTranspose {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : ntr A.conjTranspose = ntr A

theorem MIPRE.ntr_one {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] : ntr 1 = 1

The Hilbert--Schmidt inner product, in terms of ntr

theorem MIPRE.re_hsInner_eq {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (hsInner A B).re = ntr (A.conjTranspose * B)

theorem MIPRE.hsNormSq_eq {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : hsNormSq A = ntr (A.conjTranspose * A)

theorem MIPRE.re_hsInner_comm {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (hsInner B A).re = (hsInner A B).re

theorem MIPRE.hsNormSq_neg {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : hsNormSq (-A) = hsNormSq A

theorem MIPRE.re_hsInner_neg_right {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (hsInner A (-B)).re = -(hsInner A B).re

theorem MIPRE.re_hsInner_neg_left {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (hsInner (-A) B).re = -(hsInner A B).re

theorem MIPRE.re_hsInner_sub_left {n : Type u_1} [Fintype n] (A B C : Matrix n n ℂ) : (hsInner (A - B) C).re = (hsInner A C).re - (hsInner B C).re

theorem MIPRE.re_hsInner_sub_right {n : Type u_1} [Fintype n] (A B C : Matrix n n ℂ) : (hsInner A (B - C)).re = (hsInner A B).re - (hsInner A C).re

theorem MIPRE.hsNormSq_eq_re_hsInner_self {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : hsNormSq A = (hsInner A A).re

theorem MIPRE.hsNormSq_add {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : hsNormSq (A + B) = hsNormSq A + 2 * (hsInner A B).re + hsNormSq B

The parallelogram expansion: the cross term is what Cauchy--Schwarz then bounds.

theorem MIPRE.hsNormSq_sub {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : hsNormSq (A - B) = hsNormSq A - 2 * (hsInner A B).re + hsNormSq B

Cauchy--Schwarz

theorem MIPRE.trace_conjTranspose_mul_eq {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (A.conjTranspose * B).trace = ∑ p : n × n, star (A p.1 p.2) * B p.1 p.2

The trace of Aᴴ B, entrywise.

theorem MIPRE.re_trace_self_eq {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : (A.conjTranspose * A).trace.re = ∑ p : n × n, ‖A p.1 p.2‖ ^ 2

theorem MIPRE.re_trace_self_nonneg {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : 0 ≤ (A.conjTranspose * A).trace.re

theorem MIPRE.re_trace_mul_le {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (A.conjTranspose * B).trace.re ≤ √(A.conjTranspose * A).trace.re * √(B.conjTranspose * B).trace.re

theorem MIPRE.re_hsInner_le {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : (hsInner A B).re ≤ √(hsNormSq A) * √(hsNormSq B)

Cauchy--Schwarz for the normalized Hilbert--Schmidt inner product.

theorem MIPRE.abs_re_hsInner_le {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : |(hsInner A B).re| ≤ √(hsNormSq A) * √(hsNormSq B)

Cauchy--Schwarz, both signs.

theorem MIPRE.sum_abs_re_hsInner_le {n : Type u_1} [Fintype n] {ι : Type u_2} (s : Finset ι) (M N : ι → Matrix n n ℂ) : |∑ i ∈ s, (hsInner (M i) (N i)).re| ≤ √(∑ i ∈ s, hsNormSq (M i)) * √(∑ i ∈ s, hsNormSq (N i))

Cauchy--Schwarz over a finite index set, the form the soundness arguments use.

Projections

A projection here is what a projective measurement's operators are: self-adjoint and idempotent. Under the normalized trace the squared Hilbert--Schmidt norm of a projection, and of a product of two projections, collapses to a normalized trace, which is what turns the closeness calculus into statements about outcome probabilities.

theorem MIPRE.hsNormSq_of_proj {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} (hsa : star P = P) (hid : P * P = P) : hsNormSq P = ntr P

A projection's squared Hilbert--Schmidt norm is its normalized trace.

theorem MIPRE.hsNormSq_mul_of_proj {n : Type u_1} [Fintype n] {P Q : Matrix n n ℂ} (hP : star P = P) (hPid : P * P = P) (hQ : star Q = Q) (hQid : Q * Q = Q) : hsNormSq (P * Q) = ntr (P * Q)

The squared Hilbert--Schmidt norm of a product of two projections is the normalized trace of the product -- the very quantity a synchronous strategy's value is built from.

theorem MIPRE.re_hsInner_mul_mul_of_proj {n : Type u_1} [Fintype n] {E P Q : Matrix n n ℂ} (hE : star E = E) (hEid : E * E = E) (hP : star P = P) : (hsInner (P * E) (Q * E)).re = ntr (E * P * Q)

⟨P E, Q E⟩ = τ(E P Q) when E is a projection: how the arguments move a projection from one side of the inner product to the other.

theorem MIPRE.re_hsInner_self_mul_of_proj {n : Type u_1} [Fintype n] {E P : Matrix n n ℂ} (hE : star E = E) (hEid : E * E = E) : (hsInner E (P * E)).re = ntr (E * P)

⟨E, P E⟩ = τ(E P) when E is a projection.

theorem MIPRE.re_hsInner_mul_self_of_proj {n : Type u_1} [Fintype n] {E P : Matrix n n ℂ} (hE : star E = E) (hEid : E * E = E) (hP : star P = P) : (hsInner (P * E) E).re = ntr (E * P)

⟨P E, E⟩ = τ(E P) when E and P are projections.

theorem MIPRE.re_hsInner_mul_of_proj {n : Type u_1} [Fintype n] {P Q E : Matrix n n ℂ} (hP : star P = P) (hQ : star Q = Q) : (hsInner (P * Q) E).re = ntr (E * Q * P)

⟨P Q, E⟩ = τ(E Q P) for self-adjoint P and Q.

theorem MIPRE.star_one_sub {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : star P = P) : star (1 - P) = 1 - P

theorem MIPRE.one_sub_mul_one_sub {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hPid : P * P = P) : (1 - P) * (1 - P) = 1 - P

The closeness estimate

The one inequality the soundness argument needs, and the only place a Cauchy--Schwarz is spent before the value comparison. Three families of projections: O a measurement, and C, D such that the products C D are a measurement too. Then the squared distance between C_i D_i and O_i is bounded by three times the two disagreements τ(O_i(1 - D_i)) and τ(O_i(1 - C_i)) --- linearly, with no square root. Writing C_i O_i = O_i - X_i and D_i O_i = O_i - Y_i, the two disagreements are exactly ∑ ‖X_i‖² and ∑ ‖Y_i‖², and the only term that is not one of them is ∑ ⟨Y_i, X_i⟩, which Cauchy--Schwarz and the arithmetic-geometric mean inequality bound by half their sum.

theorem MIPRE.sum_hsNormSq_sub_le {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (O C D : ι → Matrix n n ℂ) (hO : ∀ (i : ι), star (O i) = O i) (hOid : ∀ (i : ι), O i * O i = O i) (hC : ∀ (i : ι), star (C i) = C i) (hCid : ∀ (i : ι), C i * C i = C i) (hD : ∀ (i : ι), star (D i) = D i) (hDid : ∀ (i : ι), D i * D i = D i) (hOsum : ∑ i : ι, ntr (O i) = 1) (hCDsum : ∑ i : ι, ntr (C i * D i) = 1) : ∑ i : ι, hsNormSq (C i * D i - O i) ≤ 3 * (∑ i : ι, ntr (O i * (1 - D i)) + ∑ i : ι, ntr (O i * (1 - C i)))

theorem MIPRE.sum_ntr_mul_ge {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (O C D : ι → Matrix n n ℂ) (acc : Finset ι) (hO : ∀ (i : ι), star (O i) = O i) (hOid : ∀ (i : ι), O i * O i = O i) (hC : ∀ (i : ι), star (C i) = C i) (hCid : ∀ (i : ι), C i * C i = C i) (hD : ∀ (i : ι), star (D i) = D i) (hDid : ∀ (i : ι), D i * D i = D i) (hOsum : ∑ i : ι, ntr (O i) = 1) : ∑ i ∈ acc, ntr (O i) - 2 * √(∑ i : ι, hsNormSq (C i * D i - O i)) ≤ ∑ i ∈ acc, ntr (C i * D i)

Close measurements have close values: the measurement-level statement of fact:approx-implies-close-value (from [NW19, Fact 4.31]), in the one direction the soundness argument needs and in the synchronous setting, where the products C_i D_i are automatically a measurement. The square root is spent here, and only here.

The averaging step

theorem MIPRE.sum_mul_sqrt_le {ι : Type u_2} (s : Finset ι) (μ f : ι → ℝ) (hμ : ∀ (i : ι), 0 ≤ μ i) (hf : ∀ (i : ι), 0 ≤ f i) : ∑ i ∈ s, μ i * √(f i) ≤ √(∑ i ∈ s, μ i) * √(∑ i ∈ s, μ i * f i)

𝔼_μ √f ≤ √(𝔼_μ 1) · √(𝔼_μ f), which for a probability distribution is Jensen's inequality for the square root. It is Cauchy--Schwarz applied to √μ and √(μ f).

theorem MIPRE.sq_sum_le_card_mul_sum_sq {ι : Type u_2} [Fintype ι] (t : ι → ℝ) (ht : ∀ (i : ι), 0 ≤ t i) : (∑ i : ι, t i) ^ 2 ≤ ↑(Fintype.card ι) * ∑ i : ι, t i ^ 2

(∑ t)² ≤ n ∑ t², Cauchy--Schwarz against the constant 1. This is the form the outcome-set steps use: a sum over the answers costs a factor |𝒜| when squared.