theorem Orthogonalization.Blocks.smul_mem_vn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (c : ℂ) {z : H →L[ℂ] H} (hz : z ∈ M) : c • z ∈ M

Scalar multiples of elements of M lie in M.

theorem Orthogonalization.Blocks.sqrt_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {y : H →L[ℂ] H} (hy : y ∈ M) (hy0 : 0 ≤ y) : CFC.sqrt y ∈ M

The square root of a positive element of M lies in M (functional calculus).

theorem Orthogonalization.Blocks.map_nonneg_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {y : H →L[ℂ] H} (hy : y ∈ M) (hy0 : 0 ≤ y) : 0 ≤ φ y

A functional positive on M is nonnegative on the positive elements of M.

theorem Orthogonalization.Blocks.re_map_nonneg_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {y : H →L[ℂ] H} (hy : y ∈ M) (hy0 : 0 ≤ y) : 0 ≤ (φ y).re

theorem Orthogonalization.Blocks.im_map_eq_zero_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {y : H →L[ℂ] H} (hy : y ∈ M) (hy0 : 0 ≤ y) : (φ y).im = 0

theorem Orthogonalization.Blocks.map_eq_ofReal_re_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {y : H →L[ℂ] H} (hy : y ∈ M) (hy0 : 0 ≤ y) : φ y = ↑(φ y).re

On positive elements of M, φ is its real part.

theorem Orthogonalization.Blocks.re_map_le_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {x y : H →L[ℂ] H} (hx : x ∈ M) (hy : y ∈ M) (hxy : x ≤ y) : (φ x).re ≤ (φ y).re

A functional positive on M is monotone on M (real parts).

theorem Orthogonalization.Blocks.re_map_star_mul_self_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) {z b : H →L[ℂ] H} (hz : IsStarProjection z) (hzM : z ∈ M) (hb : b ∈ M) (hbz : b * z = b) (h0 : (φ z).re = 0) : (φ (star b * b)).re = 0

Zero-mass lemma. If b ∈ M is supported in a projection z ∈ M (b z = b) and φ z has real part 0, then φ (b* b) = 0 (real part).