Scalar multiples of the identity

noncomputable def Orthogonalization.MvN.scalarTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H

The scalar-valued center-valued trace x ↦ τ(x) • 1.

Equations

• Orthogonalization.MvN.scalarTrace τ = τ.smulRight 1

theorem Orthogonalization.MvN.scalarTrace_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (x : H →L[ℂ] H) : (scalarTrace τ) x = τ x • 1

theorem Orthogonalization.MvN.smul_one_nonneg_of_nonneg {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {z : ℂ} (hz : 0 ≤ z) : 0 ≤ z • 1

theorem Orthogonalization.MvN.isCentralIn_smul_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : ℂ) : IsCentralIn M 1 (z • 1)

theorem Orthogonalization.MvN.eq_smul_one_of_isCentralIn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) {c : H →L[ℂ] H} (hc : IsCentralIn M 1 c) : ∃ (l : ℂ), c = l • 1

theorem Orthogonalization.MvN.norm_map_le_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))) {x : H →L[ℂ] H} (hx : x ∈ M) : ‖τ x‖ ≤ (∑' (k : ℕ), ‖g k‖ ^ 2) * ‖x‖

A functional of trace-class form is bounded on M: ‖τ x‖ ≤ (∑ ‖gₖ‖²) ‖x‖.

The scalar trace is a center-valued trace of M = 1 M 1

theorem Orthogonalization.MvN.isCenterValuedTrace_scalarTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (hτtr : ∀ x ∈ M, ∀ y ∈ M, τ (x * y) = τ (y * x)) (hτf : ∀ x ∈ M, τ (star x * x) = 0 → x = 0) (hτg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, τ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) : IsCenterValuedTrace M 1 (scalarTrace τ)

H3 for a factor with a faithful tracial trace-class state: x ↦ τ(x) • 1 is a center-valued trace of M (at the finite projection 1); the comparison clauses are mvNEquiv_of_trace_eq for M and for M_n(M).

Lemma 3.1 at 1 and the theorem

theorem Orthogonalization.povm_orthogonalization_II₁Factor {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) (hII : ∀ (r : H →L[ℂ] H), MvN.IsAbelianProj M r → r = 0) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ1 : τ 1 = 1) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (hτtr : ∀ x ∈ M, ∀ y ∈ M, τ (x * y) = τ (y * x)) (hτf : ∀ x ∈ M, τ (star x * x) = 0 → x = 0) (hτg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, τ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) (φ : NormalState M) (hφg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ.toLinearMap x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : IsPOVM M a) (ε : ℝ) (hε : 1 - ε < (φ.toLinearMap (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), IsPVM M p ∧ (φ.toLinearMap (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 for II₁ factors with a trace-class trace and trace-class states: an instance of the signed statement povm_orthogonalization (tier T4a). M has trivial center (hfactor), no nonzero abelian projection (hII), and a faithful tracial state τ of trace-class form; φ is a normal state of trace-class form.