theorem Orthogonalization.MvN.proj_le_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {p : H →L[ℂ] H} (hp : IsStarProjection p) : p ≤ 1

A projection is ≤ 1.

def Orthogonalization.MvN.HasSelection {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (n : ℕ) : Prop

Lemma 3.1 at p as a predicate: for every POVM (aᵢ) of the corner p M p and every functional positive on M and normal, there are projections qᵢ ≤ p of M commuting with aᵢ, with ∑ E(qᵢ) = p and φ(∑ aᵢ²) ≤ φ(∑ qᵢ aᵢ).

Equations

• One or more equations did not get rendered due to their size.

Lemma 3.1 on the type II₁ part

theorem Orthogonalization.MvN.exists_selection_typeII₁ {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) (hII : ∀ (r : H →L[ℂ] H), IsAbelianProj M r → r * c = r → r = 0) (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))) : ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * c = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re

Lemma 3.1 on the type II₁ part (paper, Section 3, "The latter case is easier"): the extreme maximizer of exists_extreme_maximizer consists of projections, since a non-projection coordinate admits the perturbation of exists_perturbation.

Lemma 3.1 at p from the split p = c + (p − c)

theorem Orthogonalization.MvN.selection_of_split {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) {c : H →L[ℂ] H} (hc : IsStarProjection c) (hcc : IsCentralIn M p c) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hI : ∀ (n : ℕ) (a : Fin n → H →L[ℂ] H), (∀ (i : Fin n), a i ∈ M) → (∀ (i : Fin n), 0 ≤ a i) → ∑ i : Fin n, a i = c → ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * c = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re) (hII : ∀ (n : ℕ) (a : Fin n → H →L[ℂ] H), (∀ (i : Fin n), a i ∈ M) → (∀ (i : Fin n), 0 ≤ a i) → ∑ i : Fin n, a i = p - c → ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * (p - c) = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = p - c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re) (n : ℕ) (a : Fin n → H →L[ℂ] H) (haM : ∀ (i : Fin n), a i ∈ M) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hap : ∑ i : Fin n, a i = p) : ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * p = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = p ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re

Lemma 3.1 at p for a fixed functional φ from Lemma 3.1 on the type I part c M c (hI) and on the type II₁ part (p − c) M (p − c) (hII), for a central projection c of p M p: the two families of projections are added.

theorem Orthogonalization.MvN.hasSelection_of_split {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) {c : H →L[ℂ] H} (hc : IsStarProjection c) (hcc : IsCentralIn M p c) (hI : ∀ (n : ℕ) (a : Fin n → H →L[ℂ] H), (∀ (i : Fin n), a i ∈ M) → (∀ (i : Fin n), 0 ≤ a i) → ∑ i : Fin n, a i = c → ∀ (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ), (∀ x ∈ M, 0 ≤ φ (star x * x)) → IsNormalOn M φ → ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * c = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re) (hII : ∀ (n : ℕ) (a : Fin n → H →L[ℂ] H), (∀ (i : Fin n), a i ∈ M) → (∀ (i : Fin n), 0 ≤ a i) → ∑ i : Fin n, a i = p - c → ∀ (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ), (∀ x ∈ M, 0 ≤ φ (star x * x)) → IsNormalOn M φ → ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * (p - c) = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = p - c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re) (n : ℕ) : HasSelection M p E n

Lemma 3.1 at p (HasSelection) from Lemma 3.1 on the type I part (hI, the shape of interface field H5) and on the type II₁ part (hII).

Theorem 1.2 at a finite projection from Lemma 3.1

theorem Orthogonalization.MvN.exists_pvm_bound_of_selection {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hEp : E p = p) (hEtr : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x)) {n : ℕ} (hcomp : ∀ (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)), P ∈ matrixAlgebra M n → IsStarProjection P → P * amplify n p = P → Q ∈ matrixAlgebra M n → IsStarProjection Q → Q * amplify n p = Q → ∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q) (hpolar : ∀ x ∈ matrixAlgebra M n, ∃ u ∈ matrixAlgebra M n, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x)) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) (hφp : φ p = 1) (a : Fin n → H →L[ℂ] H) (haM : ∀ (i : Fin n), a i ∈ M) (ha0 : ∀ (i : Fin n), 0 ≤ a i) (hap : ∑ i : Fin n, a i = p) (ε : ℝ) (hε : 1 - ε < (φ (∑ i : Fin n, a i * a i)).re) (q : Fin n → H →L[ℂ] H) (hq : ∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * p = q i ∧ Commute (q i) (a i)) (hqE : ∑ i : Fin n, E (q i) = p) (hqineq : (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re) : ∃ (p' : Fin n → H →L[ℂ] H), (∀ (i : Fin n), p' i ∈ M) ∧ (∀ (i : Fin n), IsStarProjection (p' i)) ∧ (∀ (i : Fin n), p' i * p = p' i) ∧ ∑ i : Fin n, p' i = p ∧ (φ (∑ i : Fin n, star (a i - p' i) * (a i - p' i))).re < 9 * ε

Theorem 1.2 at p for a fixed functional: from the projections qᵢ of Lemma 3.1 for φ and the POVM (aᵢ), Lemma 3.2 in M_n(M) and the three-term estimate give the PVM. The hypotheses hEp, hEtr, hcomp, hpolar are instances of the interface fields (center_fixed, trace, equiv_of_eq_matrix of IsCenterValuedTrace, and H6 applied to matrixAlgebra M n).

theorem Orthogonalization.MvN.orthAtN_fin_of_hasSelection {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) (hEp : E p = p) (hEtr : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x)) (n : ℕ) (hcomp : ∀ (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)), P ∈ matrixAlgebra M n → IsStarProjection P → P * amplify n p = P → Q ∈ matrixAlgebra M n → IsStarProjection Q → Q * amplify n p = Q → ∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q) (hpolar : ∀ x ∈ matrixAlgebra M n, ∃ u ∈ matrixAlgebra M n, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x)) (hsel : HasSelection M p E n) : OrthAtN M p (Fin n)

Theorem 1.2 at a finite projection p for the functionals normal on M, from Lemma 3.1 at p (hsel).

The finite case under the interface

theorem Orthogonalization.MvN.orthAtN_fin_of_isFiniteProj {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (hS : MvNStructureTheory) (M : VonNeumannAlgebra H) {p : H →L[ℂ] H} (hp : IsFiniteProj M p) (n : ℕ) : OrthAtN M p (Fin n)

Theorem 1.2 at a finite projection p, for the functionals normal on M and the output set Fin n, under the structure-theory interface: H3 supplies the center-valued trace of p M p, H1' the split p = c + (p − c) into the type I and type II₁ parts, H5 Lemma 3.1 on the type I part, exists_selection_typeII₁ (with H0) Lemma 3.1 on the type II₁ part, and H6 (applied to M_n(M)) the polar decomposition of Lemma 3.2.