Monotone convergence of positive operators (analytic core)

Why this file is needed: the complex spectral projection in Projection is a strong-operator limit of an antitone sequence of positive operators; this file provides the analytic foundation that makes that limit exist and be a bounded operator.

The key inequality is, for a positive operator A on a complex Hilbert space, ‖A x‖² ≤ ‖A‖ · re⟪A x, x⟫. It comes from the operator inequality A² ≤ ‖A‖ • A (true because t² ≤ ‖A‖·t on the spectrum [0, ‖A‖]) together with ‖A x‖² = re⟪A² x, x⟫.

theorem SpectralRepresentation.sq_le_norm_smul_of_isPositive {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →L[ℂ] H} (hA : A.IsPositive) : A ^ 2 ≤ ‖A‖ • A

For a positive operator A, A² ≤ ‖A‖ • A. On the spectrum [0, ‖A‖] one has t² ≤ ‖A‖ · t, and the continuous functional calculus transfers this pointwise inequality to the operator order.

theorem SpectralRepresentation.norm_apply_sq_le_of_isPositive {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →L[ℂ] H} (hA : A.IsPositive) (x : H) : ‖A x‖ ^ 2 ≤ ‖A‖ * RCLike.re (inner ℂ (A x) x)

Cauchy estimate for positive operators. For A positive, ‖A x‖² ≤ ‖A‖ · re⟪A x, x⟫. This powers the strong-operator monotone convergence of positive operators.

theorem SpectralRepresentation.reApplyInnerSelf_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {B C : H →L[ℂ] H} (h : B ≤ C) (x : H) : B.reApplyInnerSelf x ≤ C.reApplyInnerSelf x

The map B ↦ re⟪B x, x⟫ is monotone for the Loewner order.

theorem SpectralRepresentation.exists_tendsto_of_antitone_isPositive {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {T : ℕ → H →L[ℂ] H} (hpos : ∀ (n : ℕ), (T n).IsPositive) (hanti : Antitone T) (x : H) : ∃ (y : H), Filter.Tendsto (fun (n : ℕ) => (T n) x) Filter.atTop (nhds y)

Strong-operator monotone convergence. A pointwise-antitone sequence of positive operators converges in the strong operator topology: for every x, fun n => T n x converges. The proof shows the sequence is Cauchy, controlling ‖T n x - T m x‖² by 2‖T 0‖ · (re⟪T n x,x⟫ - re⟪T m x,x⟫) (the Cauchy estimate norm_apply_sq_le_of_isPositive), the latter being Cauchy as a bounded antitone real sequence.

theorem SpectralRepresentation.exists_continuousLinearMap_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {T : ℕ → H →L[ℂ] H} (hpos : ∀ (n : ℕ), (T n).IsPositive) (hanti : Antitone T) : ∃ (E : H →L[ℂ] H), ∀ (x : H), Filter.Tendsto (fun (n : ℕ) => (T n) x) Filter.atTop (nhds (E x))

The strong limit as a bounded operator. A pointwise-antitone sequence of positive operators has a continuous-linear strong limit E: T n x → E x for every x, with ‖E‖ ≤ ‖T 0‖.

The continuity of the limit is established here by hand, via the uniform bound ‖T k‖ ≤ ‖T 0‖ and LinearMap.mkContinuous. Mathlib's continuousLinearMapOfTendsto proves the same thing in general — a pointwise limit of continuous linear maps along a countably generated filter is again continuous — but it rests on Banach–Steinhaus, so using it would pull Mathlib.Analysis.LocallyConvex.Barrelled into this file. Since the uniform bound is available for free here, the elementary route is kept.

Properties preserved by the strong limit

If E is a strong limit of T n (T n x → E x for all x), then E inherits self-adjointness, positivity, and commutation with a fixed operator. These transfer the per-n facts to the limit by continuity of the inner product and of operator application.

theorem SpectralRepresentation.isSymmetric_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : ℕ → H →L[ℂ] H} {E : H →L[ℂ] H} (hsymm : ∀ (n : ℕ), (↑(T n)).IsSymmetric) (hE : ∀ (x : H), Filter.Tendsto (fun (n : ℕ) => (T n) x) Filter.atTop (nhds (E x))) : (↑E).IsSymmetric

A strong limit of symmetric operators is symmetric (⟪E x, y⟫ = ⟪x, E y⟫).

theorem SpectralRepresentation.isPositive_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : ℕ → H →L[ℂ] H} {E : H →L[ℂ] H} (hpos : ∀ (n : ℕ), (T n).IsPositive) (hE : ∀ (x : H), Filter.Tendsto (fun (n : ℕ) => (T n) x) Filter.atTop (nhds (E x))) : E.IsPositive

A strong limit of positive operators is positive.

theorem SpectralRepresentation.commute_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : ℕ → H →L[ℂ] H} {E P : H →L[ℂ] H} (hcomm : ∀ (n : ℕ), T n ∘SL P = P ∘SL T n) (hE : ∀ (x : H), Filter.Tendsto (fun (n : ℕ) => (T n) x) Filter.atTop (nhds (E x))) : E ∘SL P = P ∘SL E

If every T n commutes with P, so does the strong limit E.