Cauchy–Schwarz Inequalities for Approximate Measurements

Formalizes Cauchy–Schwarz-style propositions from Section 3 (Preliminaries) of the LDT paper:

• easyApproxFromApproxDelta — Proposition prop:easy-approx-from-approx-delta
• closenessOfIP / closenessOfIPAdjoint — Proposition prop:closeness-of-ip (eq:closeness3 / eq:closeness4)
• cabApproxDelta — Proposition prop:cab-approx-delta

References

• references/ldt-paper/preliminaries.tex
• blueprint/src/chapter/ch03_preliminaries.tex

theorem MIPStarRE.LDT.Preliminaries.sum_ev_mul_le_sqrt {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (X Y : Outcome → Quantum.Op ι) : |∑ a : Outcome, ev ψ (X a * Y a)| ≤ √(∑ a : Outcome, ev ψ (X a * Matrix.conjTranspose (X a))) * √(∑ a : Outcome, ev ψ (Matrix.conjTranspose (Y a) * Y a))

theorem MIPStarRE.LDT.Preliminaries.easyApproxFromApproxDelta {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B C : IdxSubMeas Question Outcome ι) (δ : Error) (hAB : SDDRel ψ 𝒟 A B δ) : |(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((A q).outcome a * (C q).outcome a)) - avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((B q).outcome a * (C q).outcome a)| ≤ √δ

prop:easy-approx-from-approx-delta.

If A ≈_δ B (sub-measurements) and C is a sub-measurement, then |𝔼_x Σ_a ⟨ψ| A_a C_a |ψ⟩ - 𝔼_x Σ_a ⟨ψ| B_a C_a |ψ⟩| ≤ √δ.

theorem MIPStarRE.LDT.Preliminaries.closenessOfIP {Question : Type u_1} {OutcomeA : Type u_2} {OutcomeB : Type u_3} {ι : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → Quantum.Op ι) (C : Question → OutcomeA → OutcomeB → Quantum.Op ι) (γ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (A q) (B q)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b) * (∑ b : OutcomeB, C q a b).conjTranspose ≤ 1) : |(avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * A q a)) - avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * B q a)| ≤ √γ

prop:closeness-of-ip (eq:closeness3).

If A ≈_γ B (raw matrices) and Σ_a (Σ_b C_{a,b})(Σ_b C_{a,b})† ≤ I, then |𝔼_x Σ_{a,b} ⟨ψ| C_{a,b} A_a |ψ⟩ - 𝔼_x Σ_{a,b} ⟨ψ| C_{a,b} B_a |ψ⟩| ≤ √γ.

theorem MIPStarRE.LDT.Preliminaries.closenessOfIPAdjoint {Question : Type u_1} {OutcomeA : Type u_2} {OutcomeB : Type u_3} {ι : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → Quantum.Op ι) (C : Question → OutcomeA → OutcomeB → Quantum.Op ι) (γ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (fun (a : OutcomeA) => Matrix.conjTranspose (A q a)) fun (a : OutcomeA) => Matrix.conjTranspose (B q a)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b).conjTranspose * ∑ b : OutcomeB, C q a b ≤ 1) : |(avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (A q a * C q a b)) - avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (B q a * C q a b)| ≤ √γ

prop:closeness-of-ip (eq:closeness4, adjoint version).

If A† ≈_γ B† and Σ_a (Σ_b C_{a,b})†(Σ_b C_{a,b}) ≤ I, then |𝔼_x Σ_{a,b} ⟨ψ| A_a C_{a,b} |ψ⟩ - 𝔼_x Σ_{a,b} ⟨ψ| B_a C_{a,b} |ψ⟩| ≤ √γ.

theorem MIPStarRE.LDT.Preliminaries.cabApproxDelta {Question : Type u_1} {OutcomeA : Type u_2} {OutcomeB : Type u_3} {ι : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : Question → OutcomeA → Quantum.Op ι) (C : Question → OutcomeA → OutcomeB → Quantum.Op ι) (δ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (A q) (B q)) ≤ δ) (hC : ∀ (q : Question) (a : OutcomeA), ∑ b : OutcomeB, Matrix.conjTranspose (C q a b) * C q a b ≤ 1) : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (fun (ab : OutcomeA × OutcomeB) => C q ab.1 ab.2 * A q ab.1) fun (ab : OutcomeA × OutcomeB) => C q ab.1 ab.2 * B q ab.1) ≤ δ

prop:cab-approx-delta.

If A ≈_δ B and ∀ x a, Σ_b (C_{a,b})† C_{a,b} ≤ I, then C_{a,b} A_a ≈_δ C_{a,b} B_a.