The centre-valued expectation of a von Neumann algebra with a vector trace

The vendored orthonormalization theorem (de la Salle's Theorem 1.2, MIPRE/Background/Orthonormalization/Orthogonalization/) is unconditional for II₁ factors only: its finite case needs a centre-valued trace with comparison (IsCenterValuedTrace, field H3 of the structure-theory interface), and for a factor that trace is the scalar x ↦ τ(x) • 1 (MvN/II1Factor.lean). The II₁ tier of C6b (planning/mipco-track.md, Phase 6) needs it for the algebras of a finite pair, which are not factors. This file constructs the centre-valued expectation E of a von Neumann algebra M with a faithful tracial vector functional τ(a) = ∑ₖ ⟪gₖ, a gₖ⟫ of finitely many vectors, with no factor, type or separability hypothesis, from which MIPRE/Background/Orthonormalization/CenterTraceClauses.lean derives every clause of IsCenterValuedTrace M 1 E except the two comparison clauses, which are MIPRE/Background/Orthonormalization/CenterComparison.lean.

• Construction. For x ∈ M, E x is the point of minimal 2-norm ∑ₖ ‖y gₖ‖² of the set of y ∈ M with ‖y‖ ≤ ‖x‖ and the same pairings τ(y c) = τ(x c) with the central elements c. That set is compact and convex in the weak operator topology, the 2-norm is lower semicontinuous there (lowerSemicontinuous_sum_norm_sq), and the minimizer is unique by the parallelogram law and faithfulness. Conjugation by a unitary of M preserves the set and, by traciality, the 2-norm, so it fixes the minimizer, which therefore commutes with every unitary of M, hence with M (commute_of_forall_unitary): it is central (exists_isCentralIn_mem_of_conj_invariant). The central element with given pairings is unique (eq_of_isCentralIn_of_pairing), which gives linearity; E is extended to B(H) arbitrarily, since only its values on M are constrained.
• Positivity. The same minimization inside the positive cone, which is closed, convex and invariant under unitary conjugation, gives a positive central element with the pairings of a positive x, which is E x by uniqueness.

No bicommutant theorem is used: M is a Mathlib VonNeumannAlgebra, which carries M″ = M as a field, and every closedness statement is the vendored weak-operator toolkit (MvN/WOTCompact.lean). The mathematics is reports/c6b-paper-proofs.md, section "The centre-valued trace", Lemmas 1–16.

noncomputable def MIPRE.Orthonormalization.vecFunctional {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {d : ℕ} (g : Fin d → H) : (H →L[ℂ] H) →ₗ[ℂ] ℂ

The vector functional τ(a) = ∑ₖ ⟪gₖ, a gₖ⟫ of finitely many vectors, on all of B(H).

Equations

• MIPRE.Orthonormalization.vecFunctional g = { toFun := fun (a : H →L[ℂ] H) => ∑ k : Fin d, inner ℂ (g k) (a (g k)), map_add' := ⋯, map_smul' := ⋯ }

theorem MIPRE.Orthonormalization.vecFunctional_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {d : ℕ} (g : Fin d → H) (a : H →L[ℂ] H) : (vecFunctional g) a = ∑ k : Fin d, inner ℂ (g k) (a (g k))

structure MIPRE.Orthonormalization.IsCenterExpectation {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {d : ℕ} (g : Fin d → H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) : Prop

A centre-valued expectation of M for the vector functional of g: a linear map on B(H) which on M takes values in the centre, preserves the pairings x ↦ τ(x c) with the central elements c, is contractive and is positive. Only its values on M are constrained.

• mem_center (x : H →L[ℂ] H) : x ∈ M → Orthogonalization.MvN.IsCentralIn M 1 (E x)

  Values in the centre.

• pairing (x : H →L[ℂ] H) : x ∈ M → ∀ (c : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 c → (vecFunctional g) (E x * c) = (vecFunctional g) (x * c)

  The pairings with the centre are preserved.

• norm_le (x : H →L[ℂ] H) : x ∈ M → ‖E x‖ ≤ ‖x‖

  Contractivity.

• nonneg (x : H →L[ℂ] H) : x ∈ M → 0 ≤ x → 0 ≤ E x

  Positivity.

The centre and the 2-norm

theorem MIPRE.Orthonormalization.isCentralIn_one_iff {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} : Orthogonalization.MvN.IsCentralIn M 1 c ↔ c ∈ M ∧ ∀ y ∈ M, Commute c y

At the projection 1, IsCentralIn says that c is an element of M commuting with M.

theorem MIPRE.Orthonormalization.isCentralIn_one_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} : Orthogonalization.MvN.IsCentralIn M 1 1

1 is central.

theorem MIPRE.Orthonormalization.isCentralIn_one_add {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c c' : H →L[ℂ] H} (hc : Orthogonalization.MvN.IsCentralIn M 1 c) (hc' : Orthogonalization.MvN.IsCentralIn M 1 c') : Orthogonalization.MvN.IsCentralIn M 1 (c + c')

The centre is closed under addition.

theorem MIPRE.Orthonormalization.isCentralIn_one_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c c' : H →L[ℂ] H} (hc : Orthogonalization.MvN.IsCentralIn M 1 c) (hc' : Orthogonalization.MvN.IsCentralIn M 1 c') : Orthogonalization.MvN.IsCentralIn M 1 (c * c')

The centre is closed under multiplication.

theorem MIPRE.Orthonormalization.isCentralIn_one_star {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {c : H →L[ℂ] H} (hc : Orthogonalization.MvN.IsCentralIn M 1 c) : Orthogonalization.MvN.IsCentralIn M 1 (star c)

The centre is closed under the adjoint, since M is.

theorem MIPRE.Orthonormalization.vecFunctional_star_mul_self {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {d : ℕ} {g : Fin d → H} (y : H →L[ℂ] H) : (vecFunctional g) (star y * y) = ↑(∑ k : Fin d, ‖y (g k)‖ ^ 2)

τ(y* y) is the 2-norm ∑ₖ ‖y gₖ‖².

theorem MIPRE.Orthonormalization.vecFunctional_star_mul_self_nonneg {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {d : ℕ} {g : Fin d → H} (y : H →L[ℂ] H) : 0 ≤ (vecFunctional g) (star y * y)

The vector functional is positive.

theorem MIPRE.Orthonormalization.eq_zero_of_sum_norm_sq_eq_zero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) {y : H →L[ℂ] H} (hy : y ∈ M) (h : ∑ k : Fin d, ‖y (g k)‖ ^ 2 = 0) : y = 0

The 2-norm is faithful on M: an element of M of 2-norm 0 vanishes at every gₖ.

theorem MIPRE.Orthonormalization.eq_zero_of_vecFunctional_star_mul_self_eq_zero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) {y : H →L[ℂ] H} (hy : y ∈ M) (h : (vecFunctional g) (star y * y) = 0) : y = 0

The vector functional of a family separating M is faithful on M.

theorem MIPRE.Orthonormalization.eq_of_isCentralIn_of_pairing {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) {z z' : H →L[ℂ] H} (hz : Orthogonalization.MvN.IsCentralIn M 1 z) (hz' : Orthogonalization.MvN.IsCentralIn M 1 z') (h : ∀ (c : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 c → (vecFunctional g) (z * c) = (vecFunctional g) (z' * c)) : z = z'

A central element is determined by its pairings with the centre, for a faithful vector functional: τ((z - z') (z - z')*) = 0 forces z = z'.

Lower semicontinuity of the 2-norm

theorem MIPRE.Orthonormalization.lowerSemicontinuous_sum_norm_sq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {d : ℕ} (g : Fin d → H) : LowerSemicontinuous fun (A : H →WOT[ℂ] H) => ∑ k : Fin d, ‖A (g k)‖ ^ 2

The 2-norm ∑ₖ ‖A gₖ‖² is lower semicontinuous in the weak operator topology: at each A it is touched from below by the continuous A' ↦ ∑ₖ (2 Re ⟪A gₖ, A' gₖ⟫ - ‖A gₖ‖²), a minorant since ‖A' gₖ - A gₖ‖² ≥ 0.

Commuting with the unitaries of M

theorem MIPRE.Orthonormalization.commute_of_forall_unitary {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} (hz : ∀ u ∈ unitary (H →L[ℂ] H), u ∈ M → Commute z u) {x : H →L[ℂ] H} (hx : x ∈ M) : Commute z x

An operator commuting with every unitary of M commutes with M: a self-adjoint element of M is a multiple of a self-adjoint contraction, which is the real part of a unitary of M, and every element of M is ℜ x + i ℑ x.

The central point of minimal 2-norm

theorem MIPRE.Orthonormalization.continuous_vecFunctional_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {d : ℕ} (g : Fin d → H) (c : H →L[ℂ] H) : Continuous fun (A : H →WOT[ℂ] H) => (vecFunctional g) (A.toCLM * c)

The pairing A ↦ τ(A c) with a fixed operator is continuous in the weak operator topology: it is a finite sum of matrix coefficients ⟪gₖ, A (c gₖ)⟫.

theorem MIPRE.Orthonormalization.exists_isCentralIn_mem_of_conj_invariant {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) {x : H →L[ℂ] H} (hx : x ∈ M) {D : Set (H →L[ℂ] H)} (hxD : x ∈ D) (hDc : IsClosed {A : H →WOT[ℂ] H | A.toCLM ∈ D}) (hDm : ∀ a ∈ D, ∀ b ∈ D, 2⁻¹ • (a + b) ∈ D) (hDu : ∀ y ∈ D, y ∈ M → ∀ u ∈ unitary (H →L[ℂ] H), u ∈ M → u * y * star u ∈ D) : ∃ z ∈ D, Orthogonalization.MvN.IsCentralIn M 1 z ∧ ‖z‖ ≤ ‖x‖ ∧ ∀ (c : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 c → (vecFunctional g) (z * c) = (vecFunctional g) (x * c)

A central point of minimal 2-norm: for x ∈ M and a set D ∋ x of operators that is closed in the weak operator topology, closed under midpoints and invariant under conjugation of its elements of M by the unitaries of M, some central z ∈ D has ‖z‖ ≤ ‖x‖ and the pairings τ(z c) = τ(x c) with the centre. It is the minimizer of the 2-norm over the weak-operator compact set C of the y ∈ M ∩ D with ‖y‖ ≤ ‖x‖ and the pairings of x: the minimizer is unique by the parallelogram law, and conjugation by a unitary u of M preserves C and the 2-norm, so it fixes the minimizer, which therefore commutes with u.

The centre-valued expectation

theorem MIPRE.Orthonormalization.exists_isCenterExpectation {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {d : ℕ} (M : VonNeumannAlgebra H) (g : Fin d → H) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) : ∃ (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H), IsCenterExpectation M g E

Existence of the centre-valued expectation for a von Neumann algebra whose vector functional is tracial and faithful: the point of minimal 2-norm, among the elements of M of norm at most ‖x‖ with the pairings of x, is central.