The clauses of a centre-valued trace, from the centre-valued expectation

The algebraic, analytic and order clauses of the vendored IsCenterValuedTrace M 1 E for a centre-valued expectation E (IsCenterExpectation, MIPRE/Background/Orthonormalization/CenterTrace.lean) of a von Neumann algebra with a faithful tracial vector functional. Each algebraic clause is an identity between central elements with the same pairings with the centre, hence an equality by eq_of_isCentralIn_of_pairing; normality is a weak-operator cluster-point argument (every cluster point of E (T k) is central with the pairings of L); division in the centre takes a weak-operator cluster point of a (c + ε)⁻¹. The two comparison clauses are MIPRE/Background/Orthonormalization/CenterComparison.lean.

Two facts about the centre Z(M) itself come first: it is closed in the weak operator topology (isClosed_setOf_isCentralIn_one), and for central 0 ≤ a ≤ c there is a central 0 ≤ z ≤ 1 with a = z c (exists_isCentralIn_eq_mul_of_le), the functional calculus of the abelian algebra Z(M) carried out inside M; neither uses the vector functional.

The centre of M

theorem MIPRE.Orthonormalization.isClosed_setOf_isCentralIn_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed {A : H →WOT[ℂ] H | Orthogonalization.MvN.IsCentralIn M 1 A.toCLM}

The centre of M is weak-operator closed: at p = 1, IsCentralIn M 1 c says c ∈ M and c commutes with every element of M, two closed conditions (isClosed_setOf_mem, isClosed_setOf_commute).

theorem MIPRE.Orthonormalization.exists_isCentralIn_norm_mul_sub_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {a c : H →L[ℂ] H} (ha : Orthogonalization.MvN.IsCentralIn M 1 a) (hc : Orthogonalization.MvN.IsCentralIn M 1 c) (ha0 : 0 ≤ a) (hac : a ≤ c) {ε : ℝ} (hε : 0 < ε) : ∃ (z : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 z ∧ 0 ≤ z ∧ z ≤ 1 ∧ ‖z * c - a‖ ≤ ε

Approximate division in the centre: for central 0 ≤ a ≤ c and ε > 0, the central element z = a (c + ε)⁻¹ satisfies 0 ≤ z ≤ 1 and ‖z c - a‖ ≤ ε, since z c - a = -ε z.

theorem MIPRE.Orthonormalization.exists_isCentralIn_eq_mul_of_le {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {a c : H →L[ℂ] H} (ha : Orthogonalization.MvN.IsCentralIn M 1 a) (hc : Orthogonalization.MvN.IsCentralIn M 1 c) (ha0 : 0 ≤ a) (hac : a ≤ c) : ∃ (z : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 z ∧ 0 ≤ z ∧ z ≤ 1 ∧ a = z * c

Division in the centre: for central 0 ≤ a ≤ c, a = z c for a central 0 ≤ z ≤ 1. The approximate quotients zⱼ with ‖zⱼ c - a‖ ≤ 1/(j+1) have a weak-operator cluster point z, which is central with 0 ≤ z ≤ 1 (closed conditions); z c is a cluster point of zⱼ c, since right multiplication by c is weak-operator continuous, and zⱼ c → a.

The clauses of IsCenterValuedTrace M 1 E

theorem MIPRE.Orthonormalization.IsCenterExpectation.vecFunctional_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (x : H →L[ℂ] H) : x ∈ M → (vecFunctional g) (E x) = (vecFunctional g) x

E preserves the vector functional on M (the pairing with the central element 1).

theorem MIPRE.Orthonormalization.IsCenterExpectation.trace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (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) : x ∈ M → ∀ y ∈ M, E (x * y) = E (y * x)

The trace property of E on M.

theorem MIPRE.Orthonormalization.IsCenterExpectation.center_fixed {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) (c : H →L[ℂ] H) : Orthogonalization.MvN.IsCentralIn M 1 c → E c = c

E is the identity on the centre.

theorem MIPRE.Orthonormalization.IsCenterExpectation.center_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) (c : H →L[ℂ] H) : Orthogonalization.MvN.IsCentralIn M 1 c → ∀ x ∈ M, E (c * x) = c * E x

E is linear over the centre.

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

E is faithful on M.

theorem MIPRE.Orthonormalization.IsCenterExpectation.normal {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) {κ : Type u} (l : Filter κ) (T : κ → H →L[ℂ] H) (L : H →L[ℂ] H) : (∀ (k : κ), T k ∈ M) → L ∈ M → Orthogonalization.MvN.TendstoWeakBdd l T L → Orthogonalization.MvN.TendstoWeakBdd l (fun (k : κ) => E (T k)) (E L)

Normality: E is continuous along bounded weak-operator convergent nets of M.

theorem MIPRE.Orthonormalization.IsCenterExpectation.div {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (r : H →L[ℂ] H) : IsStarProjection r → r ∈ M → ∀ b ∈ M, 0 ≤ b → b ≤ r → ∃ (z : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 z ∧ 0 ≤ z ∧ z ≤ 1 ∧ E b = z * E r

Division in the centre: for 0 ≤ b ≤ r with r a projection of M, E b = z * E r for a central 0 ≤ z ≤ 1. It does not use the vector functional.