Complete Fredholm theory #
Evans §6.2.3, Theorem 4.
Fredholm.lean reduces the weak problem Lu = f to the compact-operator equation
(1 - opK)u = h through the factorisation opA = opE ∘ (1 - opK) and derives the
dichotomy. This module completes the quantitative part of Evans's Theorem 4(ii)
(§6.2.3): the space
N = {u ∈ H₀¹(Ω) : B[u, v] = 0 for all v}
of weak solutions of the homogeneous problem is finite-dimensional. Since opE is a
continuous linear equivalence, N = ker(opA) = ker(1 - opK) is the eigenspace of the
compact operator opK at the eigenvalue 1, and eigenspaces of compact operators at
nonzero eigenvalues are finite-dimensional
(ContinuousLinearMap.finite_dimensional_eigenspace, the Riesz theory input).
It also proves closed range of 1 - opK, formulates the adjoint problem via the
transpose form B(·, v), and derives the solvability criterion
Lu = f solvable ↔ f ⊥ N* and dim N = dim N*.
Riesz theory for 1 - K with K compact on a real Hilbert space #
The kernel of 1 - K is the eigenspace of K at the eigenvalue 1.
Finite-dimensionality of ker(1 - K) for a compact operator K (Riesz
theory): the kernel is the eigenspace of K at the nonzero eigenvalue 1.
1 - K is bounded below on the orthogonal complement of its kernel: the main step of
the Riesz closed-range theorem, by the standard compactness contradiction. If not, normalised
xₙ ∈ (ker(1-K))ᗮ have (1-K)xₙ → 0; compactness of K extracts Kx_{φ(n)} → z, so x_{φ(n)} → z with ‖z‖ = 1, z ∈ ker(1-K), and z ∈ (ker(1-K))ᗮ, forcing z = 0 against ‖z‖ = 1.
Closed range (Riesz theory). For a compact operator K on a real Hilbert
space the range of 1 - K is closed: 1 - K is bounded below (hence antilipschitzWith
with closed range) on the orthogonal complement of its finite-dimensional kernel, and
the full range is the image of that complement. This is the geometric half towards
Evans's Theorem 4(ii) (§6.2.3).
A closed-range operator on a real Hilbert space has range exactly the orthogonal
complement of the kernel of its adjoint: range A = (ker A†)ᗮ. With
isClosed_range_one_sub this yields the solvability half of the Fredholm
alternative.
Schauder's theorem on a real Hilbert space: the adjoint of a compact operator
is compact. The Hilbert-space proof:
‖K†x - K†y‖² = ⟪x - y, KK†(x - y)⟫ ≤ ‖x - y‖ ‖KK†x - KK†y‖, so an ε²/8-net for
the relatively compact image KK†(B) of the unit ball pulls back to an ε-net for
K†(B), making K†(B) totally bounded.
The adjoint of 1 - K is 1 - K†.
Equal (finite) dimension of the two kernels, one inequality. If
dim ker(1-K) < dim ker(1-K†) then an injective, non-surjective linear map
Λ : ker(1-K) → ker(1-K†) composed with the orthogonal projection gives a finite-rank
perturbation S = K + Λ∘P with 1 - S injective; the Fredholm alternative makes
1 - S surjective, yet nothing outside range Λ is attained, a contradiction
(Brezis Thm 6.6 adapted to the Hilbert setting).
dim ker(1 - K) = dim ker(1 - K†) for a compact operator on a real Hilbert
space (the abstract form of Evans §6.2.3, Theorem 4(ii)): the index of 1 - K is
zero. Both inequalities are
finrank_ker_one_sub_adjoint_le, the reverse one applied to K† through Schauder's
theorem and K†† = K.
The adjoint of (the underlying map of) a continuous linear equivalence is bijective: the adjoint of the inverse is a two-sided inverse.
Fredholm alternative (Evans Appendix D Theorem 5, Guo Theorem VII.4.4) for a compact
operator K on a real Hilbert space: the kernel of 1 - K is finite dimensional, the range of
1 - K is closed and is the orthogonal complement of the kernel of 1 - K†, 1 - K is
injective exactly when it is surjective, and the kernels of 1 - K and 1 - K† have the same
dimension.
Fredholm dichotomy (Evans Appendix D Theorem 5, the remark following it; Guo Theorem
VII.4.4): either (1 - K) u = h has exactly one solution for every h, or the homogeneous
equation has a nonzero solution.
The space N of weak solutions of the homogeneous problem Lu = 0: the kernel of
the Riesz representative opA of the full divergence form.
Instances For
Membership in solSpace is exactly being a weak solution of the homogeneous
problem: B[u, v] = 0 against every v ∈ H₀¹(Ω). The proofs below reach solSpace
through solSpace_eq_eigenspace instead.
The homogeneous solution space is the eigenspace of the compact part opK at the
eigenvalue 1: since opA = opE ∘ (1 - opK) with opE an equivalence,
opA u = 0 ↔ opK u = u.
Finite-dimensionality of the homogeneous solution space (the finite-dimensionality
half of Evans §6.2.3, Theorem 4(ii)).
Under the Rellich-Kondrachov input (opK compact), the space of weak solutions of the
homogeneous problem Lu = 0 is finite-dimensional: it is the eigenspace of the compact
operator opK at the nonzero eigenvalue 1, and Riesz theory makes such eigenspaces
finite-dimensional.
Terminal result of the library, stated in the manuscript. Nothing else consumes it.
Closed range of the elliptic operator (towards Evans §6.2.3, Theorem
4(ii)-(iii)). Under
the Rellich-Kondrachov input the range of opA (the set of Riesz representatives of
solvable right-hand sides) is closed: opA = opE ∘ (1 - opK) with opE a
homeomorphism, and 1 - opK has closed range by Riesz theory. This is the geometric
input for the solvability criterion Lu = f solvable ↔ f ⊥ N*.
The adjoint solution space N*: the kernel of the Hilbert adjoint of opA,
which is exactly the space of weak solutions of the transpose problem
B[v, u] = 0 for all v (the adjoint bilinear form and adjoint problem defined ahead
of Evans §6.2.3, Theorem 4: the adjoint problem is the transpose form, with no
differentiability demanded of the coefficients).
Equations
- Op.solSpaceStar Ω = (↑(ContinuousLinearMap.adjoint (Op.opA Ω))).ker
Instances For
Membership in solSpaceStar is exactly being a weak solution of the transpose
problem: B[v, u] = 0 against every v ∈ H₀¹(Ω), the transpose counterpart of
mem_solSpace_iff.
Solvability criterion (Evans §6.2.3, Theorem 4(iii)). Under the
Rellich-Kondrachov input, the weak problem Lu = f is solvable exactly when f
annihilates the adjoint solution space: ∃u ∀v, B[u, v] = f(v) iff f(w) = 0 for
every weak solution w of the transpose problem B[v, w] = 0. The proof is closed
range (isClosed_range_opA) plus the Hilbert-space duality
range A = (ker A†)ᗮ.
dim N = dim N* for the elliptic problem (Evans §6.2.3, Theorem 4(ii)). The
space of weak
solutions of the homogeneous problem and the space of weak solutions of the transpose
problem have the same (finite) dimension. The factorisation opA = opE ∘ (1 - opK)
maps solSpaceStar = ker(opA†) onto ker(1 - opK†) along the bijection (opE)†,
and the abstract index theorem finrank_ker_one_sub_adjoint_eq applies.
Terminal result of the library, stated in the manuscript. Nothing else consumes it.