Physicslib4.Spectral.Spectrum

The spectrum of a bounded operator

The blueprint's resolvent set ρ(A) and spectrum σ(A) are Mathlib's resolventSet ℂ A and spectrum ℂ A; Mathlib's resolvent operator resolvent A z is (z • 1 - A)⁻¹, the negative of the blueprint's (A - λ 1)⁻¹, which flips the sign in the Neumann expansion below but describes the same resolvent set and spectrum.

Main statements

• Physicslib4.Spectral.isUnit_one_sub, Physicslib4.Spectral.hasSum_geometric_inverse_one_sub — invertibility of 1 - X and the Neumann series for (1 - X)⁻¹ when ‖X‖ < 1.
• Physicslib4.Spectral.isCompact_spectrum, Physicslib4.Spectral.spectrum_nonempty — σ(A) is compact, and (for H ≠ {0}) non-empty.
• Physicslib4.Spectral.mem_resolventSet_of_norm_lt — |λ| > ‖A‖ puts λ in the resolvent set.
• Physicslib4.Spectral.isOpen_resolventSet, Physicslib4.Spectral.exists_hasSum_resolvent, Physicslib4.Spectral.hasSum_resolvent_of_norm_lt — the resolvent set is open, the resolvent is locally given by a power series, and the Neumann expansion holds outside the disc of radius ‖A‖.
• Physicslib4.Spectral.sq_norm_sub_smul_apply_le — the b² inequality for a self-adjoint operator.
• Physicslib4.Spectral.spectrum_subset_real — a self-adjoint operator has real spectrum.
• Physicslib4.Spectral.not_isUnit_mul_of_commute — a commuting multiple of a non-invertible operator is non-invertible.
• Physicslib4.Spectral.isSelfAdjoint_aeval_real — real polynomials of a self-adjoint operator are self-adjoint.

Blueprint nodes that are literally Mathlib declarations

The spectral-radius block of the blueprint is Mathlib verbatim, so those nodes are cited rather than restated here. Where the Mathlib spelling is not a literal transcription of the blueprint, the divergence is recorded.

• thrm:heine-borel-theorem — Metric.isCompact_iff_isClosed_bounded, together with the one-directional Metric.isCompact_of_isClosed_isBounded used for σ(A). The blueprint states it for ℂⁿ with n ≥ 1; Mathlib has no dimension hypothesis, because what the proof uses is that the space is proper and Hausdorff, which ℂⁿ is.
• def:spectral-radius — spectralRadius. Caveat: spectralRadius ℂ A is ℝ≥0∞-valued, being ⨆ z ∈ spectrum ℂ A, ‖z‖₊, whereas the blueprint's R(A) is a real number. The identification is R(A) = (spectralRadius ℂ A).toReal. It is faithful because for H ≠ {0} the supremum is attained (spectrum.exists_nnnorm_eq_spectralRadius), hence finite, which is the blueprint's own remark that R(A) is a finite real; note also that Mathlib's ⨆ over the empty set is 0, so on the zero space the two sides read 0 rather than -∞.
• crllr:crllr-1 — spectrum.spectralRadius_le_nnnorm. Two caveats. It is the ℝ≥0∞ inequality spectralRadius ℂ A ≤ ‖A‖₊, which is the blueprint's R(A) ≤ ‖A‖ under the toReal identification above. And it carries a NormOneClass hypothesis, which for 𝓑(H) amounts to ‖1‖ = 1, i.e. to the blueprint's standing H ≠ {0} (Nontrivial H); the blueprint's inequality does still hold on the zero space, where σ(A) = ∅ and both sides are 0, but not by this lemma.
• lmm:hall-8.1 — IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, the real-valued form (spectralRadius ℂ A).toReal = ‖A‖ matching the blueprint's real-valued R(A); the ℝ≥0∞ form is IsSelfAdjoint.spectralRadius_eq_nnnorm. It is stated for an arbitrary CStarAlgebra, and CStarAlgebra (H →L[ℂ] H) is an instance. Like the blueprint, Mathlib derives it from Gelfand's formula for the spectral radius.
• thrm:gelfand-formula — spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, the statement that ‖A ^ n‖₊ ^ (1 / n), read in ℝ≥0∞, tends to spectralRadius ℂ A. It is the blueprint's real-valued limit under the toReal identification above (all terms and the limit are finite). Mathlib's version holds in any complex Banach algebra with no H ≠ {0} hypothesis; the blueprint keeps that hypothesis because its real-valued R(A), a supremum over σ(A) = ∅, is not 0 on the zero space, whereas the limit is.

theorem Physicslib4.Spectral.isUnit_one_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : H →L[ℂ] H} (hX : ‖X‖ < 1) : IsUnit (1 - X)

If ‖X‖ < 1 then 1 - X has a bounded inverse in 𝓑(H).

Blueprint reference: lmm:hall-7.6 (first half).

theorem Physicslib4.Spectral.hasSum_geometric_inverse_one_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X : H →L[ℂ] H} (hX : ‖X‖ < 1) : HasSum (fun (n : ℕ) => X ^ n) (Ring.inverse (1 - X))

If ‖X‖ < 1 then (1 - X)⁻¹ is given by the operator-norm convergent Neumann series ∑ Xⁿ.

Blueprint reference: lmm:hall-7.6 (second half).

theorem Physicslib4.Spectral.isCompact_spectrum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : IsCompact (spectrum ℂ A)

The spectrum σ(A) of a bounded operator A is a compact subset of ℂ.

By the Heine–Borel theorem this says that σ(A) is closed and bounded, the first two claims of part (1) of prpstn:hall-7.5; they follow from this theorem by IsCompact.isClosed and IsCompact.isBounded. Compactness is what makes the continuous functions on σ(A) a good algebra for the functional calculus: they are bounded, and polynomials are dense among them (Stone–Weierstrass). No hypothesis H ≠ {0} is needed.

Implementation note: the proof is Mathlib's spectrum.isCompact. Parts (3) and (4) of the blueprint lemma, that σ(A) is a metric space with the metric of ℂ and a measurable space with its Borel σ-algebra, are the subtype instances Subtype.instMetricSpace, Subtype.instMeasurableSpace and Subtype.borelSpace, so they carry no propositional content.

Blueprint: lmm:spectrum-is-compact-metric-measurable

theorem Physicslib4.Spectral.spectrum_nonempty {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (A : H →L[ℂ] H) : (spectrum ℂ A).Nonempty

On a nonzero Hilbert space the spectrum of every bounded operator is non-empty.

In finite dimensions this is the existence of an eigenvalue (the fundamental theorem of algebra); the general proof applies Liouville's theorem to the resolvent λ ↦ (A − λ𝟙)⁻¹. It fails on the zero space, where σ(A) = ∅.

Implementation note: the proof is Mathlib's spectrum.nonempty. The blueprint's standing convention H ≠ {0} appears here, and only where it is used, as the hypothesis Nontrivial H.

Blueprint: lmm:spectrum-is-compact-metric-measurable

theorem Physicslib4.Spectral.mem_resolventSet_of_norm_lt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (A : H →L[ℂ] H) {z : ℂ} (hz : ‖A‖ < ‖z‖) : z ∈ resolventSet ℂ A

Every λ with ‖A‖ < |λ| lies in the resolvent set of A; equivalently, σ(A) is contained in the closed disc of radius ‖A‖.

This is the only part of prpstn:hall-7.5 that is not already isCompact_spectrum or spectrum_nonempty.

Nontrivial H is carried because the bound ‖z‖ ≤ ‖A‖ on σ(A) is stated in Mathlib for a NormOneClass ring, and ‖1‖ = 1 in 𝓑(H) needs H ≠ {0}. (On the zero space 𝓑(H) is the zero ring, so resolventSet ℂ A = ℂ and the conclusion holds vacuously; the hypothesis is an artefact of the proof, not of the statement.)

Blueprint reference: prpstn:hall-7.5.

theorem Physicslib4.Spectral.isOpen_resolventSet {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : IsOpen (resolventSet ℂ A)

The resolvent set of a bounded operator is open.

Blueprint reference: prpstn:resolvent-holomorphy-and-neumann-series (part 1, openness).

theorem Physicslib4.Spectral.exists_hasSum_resolvent {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) {z₀ : ℂ} (hz₀ : z₀ ∈ resolventSet ℂ A) : ∃ (c : ℕ → H →L[ℂ] H) (r : ℝ), 0 < r ∧ ∀ (z : ℂ), ‖z - z₀‖ < r → HasSum (fun (n : ℕ) => (z - z₀) ^ n • c n) (resolvent A z)

Near every point of the resolvent set, the resolvent is given by an operator-norm convergent power series in z - z₀ with coefficients in 𝓑(H).

Blueprint reference: prpstn:resolvent-holomorphy-and-neumann-series (part 1, local power series).

theorem Physicslib4.Spectral.hasSum_resolvent_of_norm_lt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) {z : ℂ} (hz : ‖A‖ < ‖z‖) : HasSum (fun (m : ℕ) => (z ^ (m + 1))⁻¹ • A ^ m) (resolvent A z)

Outside the closed disc of radius ‖A‖ the resolvent is given by the Neumann expansion ∑ Aᵐ / z^{m+1}.

Note that Mathlib's resolvent A z = (z • 1 - A)⁻¹ is the negative of the blueprint's (A - z 1)⁻¹, which accounts for the sign of the series relative to the blueprint.

Blueprint reference: prpstn:resolvent-holomorphy-and-neumann-series (part 2).

theorem Physicslib4.Spectral.sq_norm_sub_smul_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (a b : ℝ) (ψ : H) : b ^ 2 * ‖ψ‖ ^ 2 ≤ ‖(A - (↑a + ↑b * Complex.I) • 1) ψ‖ ^ 2

For a self-adjoint A and λ = a + i b with a, b real, b² ‖ψ‖² ≤ ‖(A - λ 1) ψ‖² for every ψ.

Blueprint reference: lmm:hall-7.8.

theorem Physicslib4.Spectral.spectrum_subset_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) : spectrum ℂ A ⊆ {z : ℂ | z.im = 0}

The spectrum of a self-adjoint bounded operator is contained in the real line.

Every λ ∈ σ(A) has imaginary part 0. This is the bounded-operator form of the physicist's statement that observables have real eigenvalues, extended to the whole spectrum, continuous part included. It is why the functional calculus of a self-adjoint operator uses functions on σ(A) ⊆ ℝ.

Implementation note: the proof uses Mathlib's IsSelfAdjoint.spectrumRestricts, which says that every z in the complex spectrum equals its real part.

Blueprint: prpstn:hall-7.7

theorem Physicslib4.Spectral.not_isUnit_mul_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {A B : H →L[ℂ] H} (h : Commute A B) (hA : ¬IsUnit A) : ¬IsUnit (A * B)

If A and B commute and A is not invertible, then A * B is not invertible.

Blueprint reference: lmm:hall-ex-8.3.1.

theorem Physicslib4.Spectral.isSelfAdjoint_aeval_real {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (p : Polynomial ℝ) : IsSelfAdjoint ((Polynomial.aeval A) p)

A polynomial with real coefficients evaluated at a self-adjoint operator is self-adjoint.

Blueprint reference: lmm:real-polynomial-self-adjoint.