The norm identity ‖x ξ‖ = ‖s ξ‖ for x* x = s* s

theorem Orthogonalization.MvN.inner_apply_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (ξ : H) : inner ℂ (x ξ) (x ξ) = inner ℂ ξ ((star x * x) ξ)

theorem Orthogonalization.MvN.norm_apply_eq_of_star_mul_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x s : H →L[ℂ] H} (h : star x * x = star s * s) (ξ : H) : ‖x ξ‖ = ‖s ξ‖

Two operators with the same modulus, x* x = s* s, have the same "length": ‖x ξ‖ = ‖s ξ‖. In particular they have the same kernel.

Range and kernel of a self-adjoint operator

theorem Orthogonalization.MvN.orthogonal_range_eq_ker {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : IsSelfAdjoint s) : (↑s).rangeᗮ = (↑s).ker

For a self-adjoint operator, (range s)ᗮ = ker s.

theorem Orthogonalization.MvN.sup_range_ker_topologicalClosure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : IsSelfAdjoint s) : ((↑s).range ⊔ (↑s).ker).topologicalClosure = ⊤

For a self-adjoint operator, range s + ker s is dense: its orthogonal complement is ker s ∩ (ker s)ᗮ = 0.

Uniformly bounded sequences converging on a dense set

theorem Orthogonalization.MvN.cauchySeq_apply_of_mem_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : ℕ → H →L[ℂ] H} {C : ℝ} (hC : ∀ (n : ℕ), ‖T n‖ ≤ C) {D : Set H} (hD : ∀ η ∈ D, ∃ (l : H), Filter.Tendsto (fun (n : ℕ) => (T n) η) Filter.atTop (nhds l)) {ξ : H} (hξ : ξ ∈ closure D) : CauchySeq fun (n : ℕ) => (T n) ξ

A uniformly bounded sequence of operators which converges pointwise on a set D has Cauchy orbits on the closure of D (the ε/3 argument).

The resolvent approximants s (s + ε)⁻¹ of a positive operator

For s ≥ 0 and ε > 0, the functions t ↦ (t + ε)⁻¹ and t ↦ t/(t + ε) are continuous on the spectrum σ(s) ⊆ [0, ∞), ‖s (s + ε)⁻¹‖ ≤ 1, and ‖s · s (s + ε)⁻¹ − s‖ ≤ ε because |t (t/(t + ε) − 1)| = ε t/(t + ε) ≤ ε for t ≥ 0.

theorem Orthogonalization.MvN.continuousOn_inv_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : ContinuousOn (fun (t : ℝ) => (t + ε)⁻¹) (spectrum ℝ s)

theorem Orthogonalization.MvN.mul_cfc_inv_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : s * cfc (fun (t : ℝ) => (t + ε)⁻¹) s = cfc (fun (t : ℝ) => t * (t + ε)⁻¹) s

theorem Orthogonalization.MvN.cfc_inv_add_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : cfc (fun (t : ℝ) => (t + ε)⁻¹) s * s = cfc (fun (t : ℝ) => t * (t + ε)⁻¹) s

theorem Orthogonalization.MvN.norm_cfc_mul_inv_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : ‖cfc (fun (t : ℝ) => t * (t + ε)⁻¹) s‖ ≤ 1

theorem Orthogonalization.MvN.mul_cfc_sub_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : s * cfc (fun (t : ℝ) => t * (t + ε)⁻¹) s - s = cfc (fun (t : ℝ) => t * (t * (t + ε)⁻¹) - t) s

theorem Orthogonalization.MvN.norm_mul_cfc_sub_self_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs : 0 ≤ s) {ε : ℝ} (hε : 0 < ε) : ‖s * cfc (fun (t : ℝ) => t * (t + ε)⁻¹) s - s‖ ≤ ε

A C⋆-algebraic cancellation

theorem Orthogonalization.MvN.mul_eq_zero_of_conj_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a s : H →L[ℂ] H} (ha : 0 ≤ a) (hs : IsSelfAdjoint s) (h : s * a * s = 0) : a * s = 0

If a ≥ 0, s = s* and s a s = 0, then a s = 0: (√a s)* (√a s) = s a s = 0.

The strong limit of the approximants

theorem Orthogonalization.MvN.exists_strong_limit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {x s : H →L[ℂ] H} (hx : x ∈ M) (hsM : s ∈ M) (hs : 0 ≤ s) (hxs : star x * x = s * s) : ∃ u ∈ M, ‖u‖ ≤ 1 ∧ u * s = x ∧ (∀ (η : H), x η = 0 → u η = 0) ∧ ∀ (ξ : H), u ξ ∈ (↑x).range.topologicalClosure

The polar partial isometry as a strong limit. For x ∈ M and s ∈ M with s ≥ 0 and x* x = s² (so s = |x|), the contractions wₙ = x (s + εₙ)⁻¹ ∈ M converge strongly to a contraction u ∈ M with u s = x, u = 0 on ker x, and u ξ ∈ closure (range x) for all ξ.

The polar decomposition

theorem Orthogonalization.MvN.exists_polar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (x : H →L[ℂ] H) (hx : x ∈ M) : ∃ u ∈ M, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x)

Polar decomposition inside a von Neumann algebra (Anantharaman–Popa 2.2.4): for x ∈ M there is u ∈ M with u* u = rightSupport x, u u* = leftSupport x and x = u √(x* x). Discharges interface field H6.