The spectrum of a coercive variational problem

Let B be a bounded coercive bilinear form on a real Hilbert space V and let J : V →L[ℝ] H be a continuous linear map into a second real Hilbert space. The variational eigenvalue problem attached to this pair asks for κ : ℝ and u ≠ 0 with

B u v = κ ⟪J u, J v⟫ for every v : V.

This file studies that problem through the solution operator on H. For h : H, Lax--Milgram produces the unique u : V with B u v = ⟪h, J v⟫ for all v; the map h ↦ u is IsCoercive.formSolutionMap, and composing it with J gives IsCoercive.formSolutionOperator, an operator S : H →L[ℝ] H.

S is the right object to spectralize. It is compact as soon as J is, it is symmetric as soon as B is, and its nonzero eigenvalues are exactly the reciprocals of the variational eigenvalues: S has eigenvalue κ⁻¹ at κ • J u precisely when u solves the variational eigenvalue problem for κ. Mathlib's spectral theorem for compact symmetric operators then applies verbatim, giving eigenvectors with dense span and finite-dimensional eigenspaces at the nonzero eigenvalues. The eigenspace at 0 is the kernel of S, which is (range J)ᗮ and so can be infinite dimensional; it vanishes exactly when J has dense range.

Coercivity forces every variational eigenvalue to be positive, and quantitatively to be at least the coercivity constant whenever J is a contraction; this is the abstract form of the statement that the first eigenvalue of a Dirichlet problem is bounded below by the constant in the corresponding Poincaré inequality.

The kernel of S is the orthogonal complement of the range of J (IsCoercive.ker_formSolutionOperator), so S is injective exactly when J has dense range; that is the hypothesis under which every eigenvector of S comes from a variational eigenfunction.

Main declarations

• IsCoercive.formSolutionMap: the Lax--Milgram solution map H →L[ℝ] V of the forcing v ↦ ⟪h, J v⟫, characterized by IsCoercive.apply_formSolutionMap.
• IsCoercive.formSolutionOperator: the induced solution operator S : H →L[ℝ] H, with IsCoercive.isCompactOperator_formSolutionOperator, IsCoercive.isSymmetric_formSolutionOperator and IsCoercive.inner_formSolutionOperator_self_nonneg.
• IsCoercive.ker_formSolutionOperator: the kernel of S is (range J)ᗮ.
• IsCoercive.hasEigenvalue_formSolutionOperator_iff: the reciprocal correspondence between the nonzero eigenvalues of S and the variational eigenvalues.
• IsCoercive.exists_ne_zero_forall_apply_eq_smul_inner: existence of a variational eigenvalue.
• IsCoercive.exists_ne_zero_forall_apply_eq_inv_norm_smul_inner: the reciprocal of the norm of the solution operator is a variational eigenvalue.
• IsCoercive.pos_of_forall_apply_eq_smul_inner and IsCoercive.le_of_forall_apply_eq_smul_inner: positivity of a variational eigenvalue, and the lower bound by the coercivity constant.
• IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot and IsCoercive.orthogonalComplement_iSup_eigenspaces_ne_zero_formSolutionOperator_eq_bot: the eigenvectors of S span a dense subspace, and only the nonzero eigenvalues are needed when J has dense range.
• IsCoercive.exists_hilbertBasis_forall_apply_eq_smul_inner: the variational eigenfunctions form an orthonormal basis of H.

References

L. C. Evans, Partial Differential Equations, Section 6.5 (eigenvalues of symmetric elliptic operators); H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Section 6.4.

The solution map and the solution operator

noncomputable def IsCoercive.formSolutionMap {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) : H →L[ℝ] V

The Lax--Milgram solution map of a coercive form B along J : V →L[ℝ] H: it sends h : H to the unique u : V solving B u v = ⟪h, J v⟫ for every v : V. It is characterized by IsCoercive.apply_formSolutionMap together with IsCoercive.eq_formSolutionMap.

Equations

• hB.formSolutionMap J = ↑hB.continuousLinearEquivOfBilin.symm ∘SL ContinuousLinearMap.adjoint J

theorem IsCoercive.formSolutionMap_apply {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) : (hB.formSolutionMap J) h = hB.solutionOfInner ((ContinuousLinearMap.adjoint J) h)

The solution map is the inverse Lax--Milgram operator applied to the adjoint of J.

@[simp]

theorem IsCoercive.apply_formSolutionMap {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) (v : V) : (B ((hB.formSolutionMap J) h)) v = inner ℝ h (J v)

The variational equation solved by the solution map.

theorem IsCoercive.eq_formSolutionMap {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {h : H} {u : V} (hu : ∀ (v : V), (B u) v = inner ℝ h (J v)) : u = (hB.formSolutionMap J) h

A vector solving the variational equation of h is the solution map's value at h.

theorem IsCoercive.formPerturbationOperator_eq_comp {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) : hB.formPerturbationOperator J = hB.formSolutionMap J ∘SL J

The form perturbation operator on V is the solution map precomposed with J, where the solution operator on H is the same pair of maps composed in the other order.

noncomputable def IsCoercive.formSolutionOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) : H →L[ℝ] H

The solution operator of a coercive form B along J : V →L[ℝ] H: it sends h : H to J u, where u is the solution of B u v = ⟪h, J v⟫. For a coercive elliptic form and the inclusion of a Sobolev space into L² it is the operator inverting the elliptic problem, whose spectrum is that of the corresponding eigenvalue problem.

Equations

• hB.formSolutionOperator J = J ∘SL hB.formSolutionMap J

@[simp]

theorem IsCoercive.formSolutionOperator_apply {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) : (hB.formSolutionOperator J) h = J ((hB.formSolutionMap J) h)

The solution operator is J applied to the solution of the variational equation.

Compactness, symmetry, positivity

theorem IsCoercive.isCompactOperator_formSolutionOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) : IsCompactOperator ⇑(hB.formSolutionOperator J)

The solution operator is compact as soon as J is.

theorem IsCoercive.isSymmetric_formSolutionOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (hsymm : ∀ (u v : V), (B u) v = (B v) u) : (↑(hB.formSolutionOperator J)).IsSymmetric

The solution operator is symmetric as soon as the form is.

theorem IsCoercive.inner_formSolutionOperator_self {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) : inner ℝ h ((hB.formSolutionOperator J) h) = (B ((hB.formSolutionMap J) h)) ((hB.formSolutionMap J) h)

The quadratic form of the solution operator is the energy of the solution.

theorem IsCoercive.inner_formSolutionOperator_self_nonneg {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) : 0 ≤ inner ℝ h ((hB.formSolutionOperator J) h)

The solution operator is positive semidefinite: its quadratic form is the energy of the solution, which coercivity keeps nonnegative.

The kernel of the solution operator

theorem IsCoercive.formSolutionOperator_apply_eq_zero_iff {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (h : H) : (hB.formSolutionOperator J) h = 0 ↔ ∀ (v : V), inner ℝ h (J v) = 0

The solution operator kills exactly the vectors orthogonal to the range of J.

theorem IsCoercive.formSolutionOperator_ne_zero {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : J ≠ 0) : hB.formSolutionOperator J ≠ 0

The solution operator is nonzero whenever the map defining it is nonzero.

theorem IsCoercive.ker_formSolutionOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) : (↑(hB.formSolutionOperator J)).ker = (↑J).rangeᗮ

The kernel of the solution operator is the orthogonal complement of the range of J; IsCoercive.eigenspace_formSolutionOperator_zero_eq_bot draws the consequence for a J with dense range.

theorem IsCoercive.eigenspace_formSolutionOperator_zero_eq_bot {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : DenseRange ⇑J) : Module.End.eigenspace (↑(hB.formSolutionOperator J)) 0 = ⊥

With J of dense range, 0 is not an eigenvalue of the solution operator.

Variational eigenvalues

theorem IsCoercive.pos_of_forall_apply_eq_smul_inner {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {kappa : ℝ} {u : V} (hu : u ≠ 0) (heq : ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)) : 0 < kappa

A variational eigenvalue is positive: coercivity bounds the energy of an eigenfunction below by a positive multiple of its squared norm.

theorem IsCoercive.le_of_forall_apply_eq_smul_inner {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} {C : ℝ} (hlower : ∀ (w : V), C * ‖w‖ ^ 2 ≤ (B w) w) (hJ : ∀ (w : V), ‖J w‖ ≤ ‖w‖) {kappa : ℝ} {u : V} (hu : u ≠ 0) (heq : ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)) : C ≤ kappa

A variational eigenvalue is at least the coercivity constant, when J is a contraction. For the Dirichlet problem this is the statement that the first eigenvalue is bounded below by the constant appearing in the Poincaré inequality.

theorem IsCoercive.apply_ne_zero_of_forall_apply_eq_smul_inner {V : Type u_3} {H : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {kappa : ℝ} {u : V} (hu : u ≠ 0) (heq : ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)) : J u ≠ 0

A variational eigenfunction has nonzero image in H. If J u vanished, the eigenvalue equation would make the energy of u vanish too, which coercivity forbids for u ≠ 0.

theorem IsCoercive.hasEigenvector_formSolutionOperator {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {kappa : ℝ} (hkappa : kappa ≠ 0) {u : V} (hu : u ≠ 0) (heq : ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)) : Module.End.HasEigenvector (↑(hB.formSolutionOperator J)) kappa⁻¹ (kappa • J u)

A variational eigenfunction for κ ≠ 0 produces an eigenvector of the solution operator with eigenvalue κ⁻¹.

theorem IsCoercive.exists_forall_apply_eq_smul_inner {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {mu : ℝ} (hmu : mu ≠ 0) (h : Module.End.HasEigenvalue (↑(hB.formSolutionOperator J)) mu) : ∃ (u : V), u ≠ 0 ∧ ∀ (v : V), (B u) v = mu⁻¹ * inner ℝ (J u) (J v)

An eigenvector of the solution operator with nonzero eigenvalue produces a variational eigenfunction for the reciprocal eigenvalue.

theorem IsCoercive.exists_ne_zero_forall_apply_eq_smul_inner {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) (hJne : J ≠ 0) : ∃ (kappa : ℝ), kappa ≠ 0 ∧ ∃ (u : V), u ≠ 0 ∧ ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)

Existence of a variational eigenvalue. For a symmetric form and a nonzero compact J, the variational eigenvalue problem has a nonzero eigenvalue with an eigenfunction.

theorem IsCoercive.hasEigenvalue_formSolutionOperator_iff {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) {kappa : ℝ} (hkappa : kappa ≠ 0) : Module.End.HasEigenvalue (↑(hB.formSolutionOperator J)) kappa⁻¹ ↔ ∃ (u : V), u ≠ 0 ∧ ∀ (v : V), (B u) v = kappa * inner ℝ (J u) (J v)

The variational eigenvalues are the reciprocals of the nonzero eigenvalues of the solution operator.

theorem IsCoercive.exists_ne_zero_forall_apply_eq_inv_norm_smul_inner {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) (hJne : J ≠ 0) : ∃ (u : V), u ≠ 0 ∧ ∀ (v : V), (B u) v = ‖hB.formSolutionOperator J‖⁻¹ * inner ℝ (J u) (J v)

The reciprocal of the norm of the solution operator is a variational eigenvalue. Compactness of J is what makes ‖S‖ itself an eigenvalue of S, and positivity of S is what excludes -‖S‖.

The spectral theorem for the solution operator

theorem IsCoercive.finiteDimensional_eigenspace_formSolutionOperator {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) {mu : ℝ} (hmu : mu ≠ 0) : FiniteDimensional ℝ ↥(Module.End.eigenspace (↑(hB.formSolutionOperator J)) mu)

Eigenspaces of the solution operator at nonzero eigenvalues are finite dimensional.

theorem IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) : (⨆ (mu : ℝ), Module.End.eigenspace (↑(hB.formSolutionOperator J)) mu)ᗮ = ⊥

The spectral theorem for the solution operator: its eigenvectors span a dense subspace of H.

theorem IsCoercive.orthogonalComplement_iSup_eigenspaces_ne_zero_formSolutionOperator_eq_bot {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hJdense : DenseRange ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) : (⨆ (mu : ℝ), ⨆ (_ : mu ≠ 0), Module.End.eigenspace (↑(hB.formSolutionOperator J)) mu)ᗮ = ⊥

The eigenfunctions of the variational eigenvalue problem span a dense subspace of H: when J is compact with dense range and the form is symmetric, the eigenspaces of the solution operator at its nonzero eigenvalues already have trivial orthogonal complement.

theorem IsCoercive.exists_hilbertBasis_forall_apply_eq_smul_inner {V : Type u_5} {H : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hJdense : DenseRange ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) : ∃ (s : Set H) (b : HilbertBasis ↑s ℝ H) (kappa : ↑s → ℝ) (u : ↑s → V), ⇑b = Subtype.val ∧ (∀ (x : ↑s), 0 < kappa x) ∧ (∀ (x : ↑s), u x ≠ 0) ∧ (∀ (x : ↑s), J (u x) = ↑x) ∧ (∀ (x : ↑s) (v : V), (B (u x)) v = kappa x * inner ℝ (J (u x)) (J v)) ∧ ∀ (h : H), HasSum (fun (x : ↑s) => (kappa x)⁻¹ • ↑(b.repr h) x • b x) ((hB.formSolutionOperator J) h)

The variational eigenfunctions form an orthonormal basis of H. For a symmetric form and a compact J of dense range, H has an orthonormal basis b each of whose vectors is J u for an eigenfunction u of the variational problem at a positive eigenvalue κ, and the solution operator is diagonal in that basis: its value, equivalently the J-image of the solution of B u v = ⟪h, J v⟫, is the eigenfunction expansion ∑ κ⁻¹ ⟪b i, h⟫ b i. This is the abstract form of the eigenfunction expansion of a symmetric elliptic operator; H is not assumed separable, so the basis is indexed by a set of vectors of H as in exists_hilbertBasis.