Spectrum of compact operators and Existence III #
Two layers.
Generic (Evans Appendix D.5, Theorem 6: the spectrum of a compact operator K on a
real Hilbert space): 0 ∈ σ(K) when the space is infinite-dimensional; away from zero
the spectrum consists of eigenvalues (mathlib's Fredholm alternative); and the
eigenvalues cannot accumulate away from zero: for every δ > 0 only finitely many
eigenvalues have |μ| ≥ δ, so σ(K) \ {0} is countable. The accumulation argument is
the classical eigenvector chain: distinct eigenvalues give a strictly increasing chain
of spans Eₙ, Hilbert geometry provides unit vectors uₙ ∈ Eₙ₊₁ ∩ Eₙᗮ, and
(μₙ - K)Eₙ₊₁ ⊆ Eₙ forces ‖K(uₙ/μₙ) - K(uₘ/μₘ)‖ ≥ 1 for m < n, contradicting
the compactness of K on the bounded sequence uₙ/μₙ.
Elliptic (Existence III, obtained by parametrising the Fredholm alternative of
Evans §6.2.3 by the shift λ and invoking the spectral theorem of Evans Appendix D.5):
the set Σ = {λ : γ/(γ+λ) is an eigenvalue of opK} is countable with finite
intersections with every Set.Iic C (so an infinite Σ is a sequence increasing to
+∞), and λ ∉ Σ holds exactly when the weak problem Lu = λu + f is uniquely
solvable for every right-hand side. The reduction is the opK factorisation of
Fredholm.lean, shifted: opAlam = opE ∘ (1 - ((γ+λ)/γ)·opK). Eigenvalues of opK
are positive (coercivity of the shifted form), which bounds Σ inside (-γ, ∞).
Spectrum of a compact operator (Evans Appendix D.5, Theorem 6) #
Eigenvalues of a compact operator do not accumulate away from zero: for every
δ > 0 there are only finitely many eigenvalues μ with δ ≤ |μ|. The classical
eigenvector-chain argument, with the Riesz lemma replaced by Hilbert orthogonality.
The nonzero eigenvalues of a compact operator form a countable set: the union of
the finite slices {δ ≤ |μ|} over δ = 1/(n+1).
0 lies in the (real) spectrum of a compact operator on an infinite-dimensional
space: an inverse would make the identity compact (Evans Appendix D.5, Theorem 6(i)).
Away from zero the spectrum of a compact operator consists exactly of the eigenvalues (Evans Appendix D.5, Theorem 6(ii)), mathlib's Fredholm alternative as a set identity.
Spectrum of a compact operator (Evans Appendix D.5, Theorem 6). On an
infinite-dimensional real Hilbert space, a compact operator K has 0 in its real
spectrum; away from zero the spectrum consists exactly of the eigenvalues; the nonzero
spectrum is countable; and only finitely many spectral points have |μ| ≥ δ for each
δ > 0, so an enumeration of the nonzero spectrum converges to 0.
Terminal result of the library, stated in the manuscript. Nothing else consumes it.
Existence III for the elliptic problem #
The Gårding shift constant γ is strictly positive.
Set Σ of Existence III: the real λ for which γ/(γ+λ) is an
eigenvalue of the compact part opK of the reduction, equivalently (see
notMem_sigmaSet_iff_solvable), the λ for which the weak problem Lu = λu + f
fails to be uniquely solvable for every right-hand side.
Equations
Instances For
Eigenvalues of opK are positive: pairing the eigenvalue relation against the
eigenvector gives μ B_γ[x,x] = γ ‖x₀‖² with B_γ[x,x] > 0 by shifted coercivity.
The Riesz operator of the λ-shifted weak problem: ⟪opAlam u, v⟫ = B[u,v] - λ⟨u₀,v₀⟩.
Equations
Instances For
Riesz identity: ⟪Op.opAlam Ω lam u, v⟫ = B[u, v] - lam · zerothForm Ω u v.
The factorisation opAlam = opE ∘ (1 - ((γ+λ)/γ)·opK) of the λ-shifted problem.
The Riesz dictionary for the λ-shifted problem: u weakly solves
B[u,v] = λ⟨u₀,v₀⟩ + f(v) exactly when opAlam u is the Riesz representative of f.
The λ-shifted Riesz operator is bijective off Σ.
A point of Σ defeats uniqueness already for f = 0: the eigenvector of opK at
γ/(γ+λ) is a nonzero weak solution of the homogeneous λ-problem.
Off Σ, the λ-shifted weak problem is uniquely solvable for every functional.
The membership characterisation of Σ (the H⁻¹ form of Existence III(i)):
λ ∉ Σ exactly when B[u,v] = λ⟨u₀,v₀⟩ + f(v) is uniquely solvable for every f.
Bounded-above slices of Σ are finite: a λ ∈ Σ ∩ Iic C has
μ(λ) = γ/(γ+λ) ≥ γ/(γ+C) > 0 (positivity of the opK eigenvalues bounds Σ
inside (-γ, ∞)), and only finitely many such eigenvalues exist.
The exceptional set Σ is countable: finite on each bounded slice Σ ∩ (-∞, n].
Existence III. There is a set Σ ⊆ ℝ, countable and with
finite intersection with every (-∞, C] (so an infinite Σ is a nondecreasing
sequence diverging to +∞), such that for every λ ∉ Σ and every f ∈ L²(Ω) the
weak problem Lu = λu + f (B[u,v] = λ⟨u₀,v₀⟩ + ∫_Ω f v₀ for all v) has a
unique solution u ∈ H₀¹(Ω), and for λ ∈ Σ uniqueness fails.
Boundedness of the resolvent. For λ ∉ Σ there is a
constant C > 0 such that every weak solution of Lu = λu + f with f ∈ L²(Ω)
satisfies ‖u‖_{L²} ≤ C ‖f‖_{L²}. The constant is the operator norm of the
continuous inverse of the λ-shifted Riesz operator.