Documentation

MIPRE.Background.LIDT.Co.Preliminaries.CauchySchwarz

Cauchy–Schwarz inequalities for approximate measurements #

Cauchy–Schwarz-style propositions from Section 3 (Preliminaries) of the LDT paper: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/CauchySchwarz.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

Every statement uses a single state and joint operators, so it takes a vector state V : VecState K (a symmetric model is accepted through its coercion) and families in K →L[ℂ] K, and drops the vendored normalization hypothesis hψ : ψ.IsNormalized, a theorem of the vector state (V.ev_one_of_isNormalized). SDDRel ψ is V.SDDRel, qSDDCore ψ is V.qSDDCore, ᴴ is star.

The proofs are those of the earlier ported files: question_easyApproxFromApproxDelta is question_overlap_gap_aux (SwitchSandwichPrep/ApproxDelta.lean) after splitting the sum, closenessOfIP and closenessOfIPAdjoint are closenessOfInnerProduct_left and _right (SwitchSandwichPrep/InnerProduct.lean), and cabApproxDelta is cabApproxDelta_raw (Preliminaries/DistanceBounds.lean) on the raw families.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
theorem MIPRE.LIDT.Co.Preliminaries.sum_ev_mul_le_sqrt {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (X Y : Outcome → K →L[ℂ] K) :
|∑ a : Outcome, V.ev (X a * Y a)| ≤ √(∑ a : Outcome, V.ev (X a * star (X a))) * √(∑ a : Outcome, V.ev (star (Y a) * Y a))

Cauchy–Schwarz for a sum of expectations: |∑_a ev (X_a Y_a)| ≤ √(∑_a ev (X_a X_a†)) · √(∑_a ev (Y_a† Y_a)).

source
theorem MIPRE.LIDT.Co.Preliminaries.question_easyApproxFromApproxDelta {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B C : SubMeas Outcome (K →L[ℂ] K)) :
|∑ a : Outcome, V.ev (A.outcome a * C.outcome a) - ∑ a : Outcome, V.ev (B.outcome a * C.outcome a)| ≤ √(V.qSDD A B)

Questionwise form of prop:easy-approx-from-approx-delta: |∑_a ev (A_a C_a) - ∑_a ev (B_a C_a)| ≤ √(qSDD A B) for submeasurements A, B, C.

source
theorem MIPRE.LIDT.Co.Preliminaries.easyApproxFromApproxDelta {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B C : IdxSubMeas Question Outcome (K →L[ℂ] K)) (δ : ℝ) (hAB : V.SDDRel 𝒟 A B δ) :
|(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.ev ((A q).outcome a * (C q).outcome a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.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 |ψ⟩| ≤ √δ.

source
theorem MIPRE.LIDT.Co.Preliminaries.closenessOfIP {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (γ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (A q) (B q)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b) * star (∑ b : OutcomeB, C q a b) ≤ 1) :
|(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * A q a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * B q a)| ≤ √γ

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

If A ≈_γ B (raw operators) 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 |ψ⟩| ≤ √γ.

source
theorem MIPRE.LIDT.Co.Preliminaries.closenessOfIPAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (γ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (fun (a : OutcomeA) => star (A q a)) fun (a : OutcomeA) => star (B q a)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, star (∑ b : OutcomeB, C q a b) * ∑ b : OutcomeB, C q a b ≤ 1) :
|(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (A q a * C q a b)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.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} |ψ⟩| ≤ √γ.

source
theorem MIPRE.LIDT.Co.Preliminaries.cabApproxDelta {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (δ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (A q) (B q)) ≤ δ) (hC : ∀ (q : Question) (a : OutcomeA), ∑ b : OutcomeB, star (C q a b) * C q a b ≤ 1) :
(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.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.