Bridge lemmas for prop:switch-sandwich

theorem MIPStarRE.LDT.Preliminaries.weightedFinsetCauchySchwarz {Question : Type u_1} {Outcome : Type u_2} [Fintype Outcome] (𝒟 : Distribution Question) (t x y : Question → Outcome → Error) (ht : ∀ (q : Question) (a : Outcome), |t q a| ≤ √(x q a) * √(y q a)) (hx : ∀ (q : Question) (a : Outcome), 0 ≤ x q a) (hy : ∀ (q : Question) (a : Outcome), 0 ≤ y q a) : |avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, t q a| ≤ √(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, x q a) * √(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, y q a)

theorem MIPStarRE.LDT.Preliminaries.weightedFinsetCauchySchwarz_on_selectedSupport {Question : Type u_1} {Outcome : Type u_2} [Fintype Outcome] (𝒟 : Distribution Question) (selected : Question → Outcome → Prop) [(q : Question) → (a : Outcome) → Decidable (selected q a)] (t x y : Question → Outcome → Error) (ht : ∀ (q : Question) (a : Outcome), selected q a → |t q a| ≤ √(x q a) * √(y q a)) (hx : ∀ (q : Question) (a : Outcome), selected q a → 0 ≤ x q a) (hy : ∀ (q : Question) (a : Outcome), selected q a → 0 ≤ y q a) : |avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, if selected q a then t q a else 0| ≤ √(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, if selected q a then x q a else 0) * √(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, if selected q a then y q a else 0)

Weighted finite Cauchy--Schwarz with the summand restricted to a selected support.

The statement is the ordinary weighted finite Cauchy--Schwarz inequality applied to the zero-extension of t, x, and y away from selected.

theorem MIPStarRE.LDT.Preliminaries.subMeas_diagMass_le_mass {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : SubMeas Outcome ι) : ∑ a : Outcome, ev ψ (A.outcome a * A.outcome a) ≤ ev ψ A.total

The diagonal mass of a sub-measurement is bounded by its total mass.

theorem MIPStarRE.LDT.Preliminaries.subMeas_diagMass_le_one {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (A : SubMeas Outcome ι) : ∑ a : Outcome, ev ψ (A.outcome a * A.outcome a) ≤ 1

The diagonal mass of a sub-measurement is at most 1 on a normalized state.

theorem MIPStarRE.LDT.Preliminaries.projSubMeas_diagMass_eq_mass {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : ProjSubMeas Outcome ι) : ∑ a : Outcome, ev ψ (A.outcome a * A.outcome a) = ev ψ A.total

Projective outcomes satisfy P_a^2 = P_a, so diagonal mass equals total mass.

theorem MIPStarRE.LDT.Preliminaries.projSubMeas_outcome_mul_total_eq_outcome {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (A : ProjSubMeas Outcome ι) (a : Outcome) : A.outcome a * A.total = A.outcome a

Each projective outcome is absorbed by the total projector.

theorem MIPStarRE.LDT.Preliminaries.projSubMeas_total_proj {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (A : ProjSubMeas Outcome ι) : A.total * A.total = A.total

The total operator of a projective sub-measurement is itself a projector.

theorem MIPStarRE.LDT.Preliminaries.opBounded01_hermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {B : Quantum.Op ι} (hB : OpBounded01 B) : Matrix.conjTranspose B = B

Any OpBounded01 operator is Hermitian.

theorem MIPStarRE.LDT.Preliminaries.opBounded01_sq_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {B : Quantum.Op ι} (hB : OpBounded01 B) : B * B ≤ 1

Any OpBounded01 operator satisfies B * B ≤ 1.

theorem MIPStarRE.LDT.Preliminaries.leftTensor_opBounded01 {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {B : Quantum.Op ι₁} (hB : OpBounded01 B) : OpBounded01 (leftTensor B)

Left tensoring preserves the 0 ≤ B ≤ 1 bounds.