The combinatorial selection lemma

theorem Orthogonalization.FinDim.exists_dominating_finset {α : Type u_1} [Fintype α] [DecidableEq α] (c : α → ℝ) (n : ℕ) : n ≤ Fintype.card α → ∃ (S : Finset α), S.card = n ∧ ∀ x ∈ S, ∀ y ∉ S, c y ≤ c x

Top-n selection. For every n ≤ card α there is a set of n indices on which c dominates its values on the complement.

theorem Orthogonalization.FinDim.sum_le_sum_dominating {α : Type u_1} [Fintype α] [DecidableEq α] (c w : α → ℝ) (hw0 : ∀ (x : α), 0 ≤ w x) (hw1 : ∀ (x : α), w x ≤ 1) (S : Finset α) (hdom : ∀ x ∈ S, ∀ y ∉ S, c y ≤ c x) (hsum : ∑ x : α, w x = ↑S.card) : ∑ x : α, w x * c x ≤ ∑ x ∈ S, c x

A weighted sum with weights in [0,1] summing to card S is dominated by the plain sum over a set S on which c dominates its values off S.

theorem Orthogonalization.FinDim.exists_finset_sum_ge {α : Type u_1} [Fintype α] [DecidableEq α] (c w : α → ℝ) (hw0 : ∀ (x : α), 0 ≤ w x) (hw1 : ∀ (x : α), w x ≤ 1) (n : ℕ) (hsum : ∑ x : α, w x = ↑n) : ∃ (S : Finset α), S.card = n ∧ ∑ x : α, w x * c x ≤ ∑ x ∈ S, c x

The vertices of the hypersimplex. If w : α → [0,1] sums to a natural number n, the weighted sum ∑ w x * c x is dominated by the sum of c over some set of exactly n indices.

Sums of rank-one spectral projections

theorem Orthogonalization.FinDim.JointEigenbasis.mul_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : x * J.P k = ↑(J.lam k) • J.P k

x P k = λ_k P k.

theorem Orthogonalization.FinDim.JointEigenbasis.P_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : J.P k * x = ↑(J.lam k) • J.P k

P k x = λ_k P k.

theorem Orthogonalization.FinDim.JointEigenbasis.P_mul_P' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) : J.P k * J.P l = if k = l then J.P k else 0

theorem Orthogonalization.FinDim.JointEigenbasis.isStarProjection_sum_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (T : Finset (Fin (Module.finrank ℂ H))) : IsStarProjection (∑ k ∈ T, J.P k)

A sum of distinct rank-one spectral projections is a projection.

theorem Orthogonalization.FinDim.JointEigenbasis.commute_sum_P_snd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (T : Finset (Fin (Module.finrank ℂ H))) : Commute (∑ k ∈ T, J.P k) a

A sum of rank-one spectral projections commutes with the second operator.

theorem Orthogonalization.FinDim.JointEigenbasis.trace_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : (LinearMap.trace ℂ H) ↑(J.P k) = 1

Each rank-one spectral projection has trace 1.

theorem Orthogonalization.FinDim.JointEigenbasis.trace_sum_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (T : Finset (Fin (Module.finrank ℂ H))) : (LinearMap.trace ℂ H) ↑(∑ k ∈ T, J.P k) = ↑T.card

The trace of a sum of distinct rank-one spectral projections is their number.

theorem Orthogonalization.FinDim.JointEigenbasis.mul_self_eq_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : x * x = ∑ k : Fin (Module.finrank ℂ H), ↑(J.lam k) • ↑(J.lam k) • J.P k

x * x in the joint eigenbasis.

Lemma 3.1 in finite dimension

theorem Orthogonalization.FinDim.exists_commuting_projections {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (a : ι → H →L[ℂ] H) (ha0 : ∀ (i : ι), 0 ≤ a i) (ha1 : ∑ i : ι, a i = 1) : ∃ (q : ι → H →L[ℂ] H), (∀ (i : ι), IsStarProjection (q i)) ∧ (∀ (i : ι), Commute (q i) (a i)) ∧ ∑ i : ι, (LinearMap.trace ℂ H) ↑(q i) = ↑(Module.finrank ℂ H) ∧ (φ (∑ i : ι, a i * a i)).re ≤ (φ (∑ i : ι, q i * a i)).re

Lemma 3.1 for B(H), H finite-dimensional. For a POVM (a i) and any linear functional φ on B(H) there are projections q i commuting with a i, of total trace dim H, with φ(∑ a i a i) ≤ φ(∑ q i a i) (real parts). The q i are sums of rank-one spectral projections of a i, selected by exists_finset_sum_ge.