Preliminaries on the corners c M c ⊆ p M p

theorem Orthogonalization.MvN.IsCentralIn.proj_mul_self {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p c : H →L[ℂ] H} (hp : IsStarProjection p) (hcc : IsCentralIn M p c) : p * c = c

A central element c of p M p satisfies p c = c.

theorem Orthogonalization.MvN.IsCentralIn.self_mul_proj {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p c : H →L[ℂ] H} (hp : IsStarProjection p) (hcc : IsCentralIn M p c) : c * p = c

A central element c of p M p satisfies c p = c.

theorem Orthogonalization.MvN.corner_of_corner {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {p c x : H →L[ℂ] H} (hpc : p * c = c) (hcp : c * p = c) (hx : c * x * c = x) : p * x * p = x

An element of the corner c M c lies in the corner p M p when p c = c = c p.

theorem Orthogonalization.MvN.corner_of_sum_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {a : Fin n → H →L[ℂ] H} {c : H →L[ℂ] H} (hc : IsStarProjection c) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hac : ∑ i : Fin n, a i = c) (i : Fin n) : c * a i * c = a i

Each term of a POVM summing to the projection c lies in the corner c M c.

theorem Orthogonalization.MvN.le_one_of_sum_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} {a : Fin n → H →L[ℂ] H} {c : H →L[ℂ] H} (hc : IsStarProjection c) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hac : ∑ i : Fin n, a i = c) (i : Fin n) : a i ≤ 1

Each term of a POVM summing to a projection is ≤ 1.

Normal functionals along bounded weak-operator convergent nets

theorem Orthogonalization.MvN.tendsto_of_tendstoWeakBdd_of_tsum {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {g : ℕ → H} (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) (hφg : ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) {κ : Type u_1} {l : Filter κ} {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (k : κ), T k ∈ M) (hL : L ∈ M) (h : TendstoWeakBdd l T L) : Filter.Tendsto (fun (k : κ) => φ (T k)) l (nhds (φ L))

A functional of the form x ↦ ∑ₖ ⟪gₖ, x gₖ⟫ on M, with ∑ ‖gₖ‖² < ∞, is continuous along bounded weak-operator convergent nets of M (Tannery's theorem).

theorem Orthogonalization.MvN.tendsto_of_tendstoWeakBdd {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hH0 : ∀ (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ), (∀ x ∈ M, 0 ≤ φ (star x * x)) → IsNormalOn M φ → ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) (hφn : IsNormalOn M φ) {κ : Type u_1} {l : Filter κ} {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (k : κ), T k ∈ M) (hL : L ∈ M) (h : TendstoWeakBdd l T L) : Filter.Tendsto (fun (k : κ) => φ (T k)) l (nhds (φ L))

Bounded weak-operator continuity of a normal functional. Under the representation hypothesis hH0 (a functional positive and normal on M is ∑ₖ ⟪gₖ, · gₖ⟫ on M with ∑ ‖gₖ‖² < ∞), such a functional is continuous along bounded weak-operator convergent nets of M, indexed by any type.

The constraint set C

def Orthogonalization.MvN.coordSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c a : H →L[ℂ] H) : Set (H →WOT[ℂ] H)

The one-coordinate constraint: T ∈ c M c, 0 ≤ T ≤ 1, T commuting with a, as a set of operators with the weak operator topology.

Equations

• Orthogonalization.MvN.coordSet M c a = {T : H →WOT[ℂ] H | T.toCLM ∈ M ∧ c * T.toCLM * c = T.toCLM ∧ 0 ≤ T.toCLM ∧ T.toCLM ≤ 1 ∧ Commute T.toCLM a}

theorem Orthogonalization.MvN.mem_coordSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c a : H →L[ℂ] H} {T : H →WOT[ℂ] H} : T ∈ coordSet M c a ↔ T.toCLM ∈ M ∧ c * T.toCLM * c = T.toCLM ∧ 0 ≤ T.toCLM ∧ T.toCLM ≤ 1 ∧ Commute T.toCLM a

theorem Orthogonalization.MvN.norm_le_one_of_mem_coordSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c a : H →L[ℂ] H} {T : H →WOT[ℂ] H} (h : T ∈ coordSet M c a) : ‖T.toCLM‖ ≤ 1

0 ≤ T ≤ 1 forces ‖T‖ ≤ 1.

theorem Orthogonalization.MvN.isClosed_coordSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c a : H →L[ℂ] H) : IsClosed (coordSet M c a)

The one-coordinate constraint set is weak-operator closed.

theorem Orthogonalization.MvN.convex_coordSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c a : H →L[ℂ] H) : Convex ℝ (coordSet M c a)

The one-coordinate constraint set is convex.

def Orthogonalization.MvN.coordBox {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : H →L[ℂ] H) {n : ℕ} (a : Fin n → H →L[ℂ] H) : Set (Fin n → H →WOT[ℂ] H)

The box of tuples with every coordinate in the one-coordinate constraint set.

Equations

• Orthogonalization.MvN.coordBox M c a = Set.univ.pi fun (i : Fin n) => Orthogonalization.MvN.coordSet M c (a i)

theorem Orthogonalization.MvN.mem_coordBox {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} {n : ℕ} {a : Fin n → H →L[ℂ] H} {x : Fin n → H →WOT[ℂ] H} : x ∈ coordBox M c a ↔ ∀ (i : Fin n), x i ∈ coordSet M c (a i)

theorem Orthogonalization.MvN.isClosed_coordBox {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : H →L[ℂ] H) {n : ℕ} (a : Fin n → H →L[ℂ] H) : IsClosed (coordBox M c a)

def Orthogonalization.MvN.selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : H →L[ℂ] H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) {n : ℕ} (a : Fin n → H →L[ℂ] H) : Set (Fin n → H →WOT[ℂ] H)

The set C of Lemma 3.1: tuples of the corner c M c with 0 ≤ xᵢ ≤ 1, xᵢ commuting with aᵢ, and ∑ᵢ E(xᵢ) = c, as a subset of the product of weak-operator topologies.

Equations

• Orthogonalization.MvN.selectionSet M c E a = Orthogonalization.MvN.coordBox M c a ∩ {x : Fin n → H →WOT[ℂ] H | ∑ i : Fin n, E (x i).toCLM = c}

theorem Orthogonalization.MvN.mem_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} {n : ℕ} {a : Fin n → H →L[ℂ] H} {x : Fin n → H →WOT[ℂ] H} : x ∈ selectionSet M c E a ↔ x ∈ coordBox M c a ∧ ∑ i : Fin n, E (x i).toCLM = c

theorem Orthogonalization.MvN.selectionSet_subset_pi_norm_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : H →L[ℂ] H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) {n : ℕ} (a : Fin n → H →L[ℂ] H) : selectionSet M c E a ⊆ Set.univ.pi fun (x : Fin n) => {T : H →WOT[ℂ] H | ‖T.toCLM‖ ≤ 1}

C lies in the unit ball of the product.

theorem Orthogonalization.MvN.ofCLM_mem_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p c : H →L[ℂ] H} (hc : IsStarProjection c) (hcc : IsCentralIn M p c) {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterValuedTrace M p E) {n : ℕ} {a : Fin n → H →L[ℂ] H} (haM : ∀ (i : Fin n), a i ∈ M) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hac : ∑ i : Fin n, a i = c) : (fun (i : Fin n) => ContinuousLinearMapWOT.ofCLM (a i)) ∈ selectionSet M c E a

(a₁, …, aₙ) belongs to C.

theorem Orthogonalization.MvN.convex_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : H →L[ℂ] H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) {n : ℕ} (a : Fin n → H →L[ℂ] H) : Convex ℝ (selectionSet M c E a)

C is convex.

theorem Orthogonalization.MvN.isClosed_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) {c : H →L[ℂ] H} (hcc : IsCentralIn M p c) {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterValuedTrace M p E) {n : ℕ} (a : Fin n → H →L[ℂ] H) : IsClosed (selectionSet M c E a)

C is weak-operator closed. For x in the closure of C, the truncated coordinate nets y ↦ yᵢ (along the trace of 𝓝 x on C) are bounded and weak-operator convergent to xᵢ, so by normality of E the nets E(yᵢ) converge weakly to E(xᵢ); summing, the constant value c of ∑ᵢ E(yᵢ) on C is the weak limit ∑ᵢ E(xᵢ).

theorem Orthogonalization.MvN.isCompact_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) {c : H →L[ℂ] H} (hcc : IsCentralIn M p c) {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterValuedTrace M p E) {n : ℕ} (a : Fin n → H →L[ℂ] H) : IsCompact (selectionSet M c E a)

C is weak-operator compact: closed and contained in the unit ball of the product, which is compact by isCompact_setOf_norm_le.

The objective x ↦ Re φ(∑ᵢ xᵢ aᵢ)

def Orthogonalization.MvN.objective {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) {n : ℕ} (a : Fin n → H →L[ℂ] H) (x : Fin n → H →WOT[ℂ] H) : ℝ

The objective functional of Lemma 3.1 on the product of weak-operator topologies.

Equations

• Orthogonalization.MvN.objective φ a x = (φ (∑ i : Fin n, (x i).toCLM * a i)).re

theorem Orthogonalization.MvN.objective_affine {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) {n : ℕ} (a : Fin n → H →L[ℂ] H) (x y : Fin n → H →WOT[ℂ] H) (s t : ℝ) : objective φ a (s • x + t • y) = s * objective φ a x + t * objective φ a y

The objective is affine.

theorem Orthogonalization.MvN.continuousOn_objective {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} {n : ℕ} {a : Fin n → H →L[ℂ] H} (haM : ∀ (i : Fin n), a i ∈ M) {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) : ContinuousOn (objective φ a) (selectionSet M c E a)

The objective is continuous on C for a normal φ: along the trace of 𝓝 x on C, the net ∑ᵢ yᵢ aᵢ is bounded, in M, and weak-operator convergent to ∑ᵢ xᵢ aᵢ.

Perturbing one coordinate

def Orthogonalization.MvN.perturb {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (e : Fin n → H →WOT[ℂ] H) (i : Fin n) (b : H →L[ℂ] H) (t : ℝ) : Fin n → H →WOT[ℂ] H

The tuple e with its i-th coordinate replaced by eᵢ + t b.

Equations

• Orthogonalization.MvN.perturb e i b t = Function.update e i (ContinuousLinearMapWOT.ofCLM ((e i).toCLM + ↑t • b))

theorem Orthogonalization.MvN.perturb_apply_self {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (e : Fin n → H →WOT[ℂ] H) (i : Fin n) (b : H →L[ℂ] H) (t : ℝ) : perturb e i b t i = ContinuousLinearMapWOT.ofCLM ((e i).toCLM + ↑t • b)

theorem Orthogonalization.MvN.perturb_apply_of_ne {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (e : Fin n → H →WOT[ℂ] H) {i j : Fin n} (hji : j ≠ i) (b : H →L[ℂ] H) (t : ℝ) : perturb e i b t j = e j

theorem Orthogonalization.MvN.midpoint_perturb {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (e : Fin n → H →WOT[ℂ] H) (i : Fin n) (b : H →L[ℂ] H) (t : ℝ) : (1 / 2) • perturb e i b (-t) + (1 / 2) • perturb e i b t = e

e is the midpoint of its two perturbations e ± t b.

theorem Orthogonalization.MvN.sum_map_update {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (e : Fin n → H →WOT[ℂ] H) (i : Fin n) (v : H →WOT[ℂ] H) : ∑ j : Fin n, E (Function.update e i v j).toCLM = ∑ j : Fin n, E (e j).toCLM + (E v.toCLM - E (e i).toCLM)

Sums over a tuple with one coordinate replaced.

theorem Orthogonalization.MvN.perturb_mem_selectionSet {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} {n : ℕ} {a : Fin n → H →L[ℂ] H} {e : Fin n → H →WOT[ℂ] H} (he : e ∈ selectionSet M c E a) (i : Fin n) {b : H →L[ℂ] H} (hbM : b ∈ M) (hbc : c * b * c = b) (hba : Commute b (a i)) (hEb : E b = 0) (t : ℝ) (h0 : 0 ≤ (e i).toCLM + ↑t • b) (h1 : (e i).toCLM + ↑t • b ≤ 1) : perturb e i b t ∈ selectionSet M c E a

A perturbation e + t b along a self-adjoint b ∈ c M c commuting with aᵢ, with E b = 0 and keeping the i-th coordinate in [0, 1], stays in C.

The Krein–Milman step

theorem Orthogonalization.MvN.exists_extreme_maximizer {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) {c : H →L[ℂ] H} (hc : IsStarProjection c) (hcc : IsCentralIn M p c) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hE : IsCenterValuedTrace M p E) {n : ℕ} (a : Fin n → H →L[ℂ] H) (haM : ∀ (i : Fin n), a i ∈ M) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hac : ∑ i : Fin n, a i = c) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) : ∃ (x : Fin n → H →L[ℂ] H), (∀ (i : Fin n), x i ∈ M ∧ c * x i * c = x i ∧ 0 ≤ x i ∧ x i ≤ 1 ∧ Commute (x i) (a i)) ∧ ∑ i : Fin n, E (x i) = c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, x i * a i)).re ∧ ∀ (i : Fin n), ∀ b ∈ M, c * b * c = b → IsSelfAdjoint b → Commute b (a i) → E b = 0 → (∃ (t₀ : ℝ), 0 < t₀ ∧ ∀ (t : ℝ), |t| ≤ t₀ → 0 ≤ x i + ↑t • b ∧ x i + ↑t • b ≤ 1) → b = 0

The Krein–Milman step of Lemma 3.1 (paper, Section 3): on the corner c M c of the finite corner p M p with center-valued trace E, the set C of tuples (xᵢ) of c M c with 0 ≤ xᵢ ≤ 1, xᵢ commuting with aᵢ and ∑ E(xᵢ) = c is weak-operator compact and convex, the functional x ↦ φ(∑ xᵢ aᵢ) is continuous on it, and an extreme point of the maximizing face exists; extremality is recorded coordinatewise: no nonzero self-adjoint b ∈ c M c commuting with aᵢ with E b = 0 keeps xᵢ ± t b in [0, 1] for small t.