The Rayleigh principle for a coercive variational problem

Let B be a bounded coercive symmetric 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. When J is nonzero and compact, the variational eigenvalues of the pair are the reciprocals of the nonzero eigenvalues of the solution operator S = IsCoercive.formSolutionOperator, and the least variational eigenvalue ‖S‖⁻¹ is the minimum of the Rayleigh quotient

B v v / ‖J v‖²,

taken over the v : V with J v ≠ 0. Without compactness, this file proves that ‖S‖⁻¹ is still the largest constant C for which C ‖J v‖² ≤ B v v holds for every v : V, provided J ≠ 0.

For the Dirichlet problem of a divergence-form elliptic operator, with V = H¹₀(Ω), H = L²(Ω) and J the inclusion, this says that the first eigenvalue is the minimum of the energy over the L²-unit sphere, and that it is exactly the optimal constant in the Poincaré inequality C‖u‖²_{L²} ≤ a(u, u).

The two halves of the argument

The lower bound ‖S‖⁻¹ ‖J v‖² ≤ B v v needs no compactness and no attainment. It comes from Cauchy--Schwarz in the energy form: solving B w u = ⟪J v, J u⟫ for w gives ‖J v‖² = B w v and B w w = ⟪J v, S (J v)⟫ ≤ ‖S‖ ‖J v‖², and (B w v)² ≤ B w w · B v v closes the loop. Coercivity supplies the solution operator through Lax--Milgram and the nonnegativity of the diagonal, which is what makes the energy form obey Cauchy--Schwarz; that inequality is LinearMap.BilinForm.apply_sq_le_of_symm, applied to the continuous form's underlying bilinear form.

The attainment is where compactness enters: ‖S‖ is an eigenvalue of the compact symmetric positive operator S (IsCoercive.exists_ne_zero_forall_apply_eq_inv_norm_smul_inner), and its eigenfunction realizes the quotient. Without compactness the infimum can fail to be attained, so the IsLeast statement carries IsCompactOperator J; the optimal-constant IsGreatest statement does not require attainment.

Main declarations

• IsCoercive.norm_apply_sq_le_norm_formSolutionOperator_mul: the estimate ‖J v‖² ≤ ‖S‖ B v v, and IsCoercive.inv_norm_formSolutionOperator_mul_norm_apply_sq_le its reciprocal form ‖S‖⁻¹ ‖J v‖² ≤ B v v.
• IsCoercive.exists_ne_zero_forall_apply_eq_inv_norm_smul_inner: ‖S‖⁻¹ is a variational eigenvalue, the least one.
• IsCoercive.isLeast_rayleighQuotient: the Rayleigh principle, ‖S‖⁻¹ is the minimum of the Rayleigh quotient.
• IsCoercive.isGreatest_inv_norm_formSolutionOperator: ‖S‖⁻¹ is the optimal constant in the inequality C ‖J v‖² ≤ B v v.

References

L. C. Evans, Partial Differential Equations, Section 6.5.1, Theorem 2 (the variational principle for the principal eigenvalue); H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Section 6.4.

The Rayleigh lower bound

theorem IsCoercive.norm_apply_sq_le_norm_formSolutionOperator_mul {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) (v : V) : ‖J v‖ ^ 2 ≤ ‖hB.formSolutionOperator J‖ * (B v) v

The energy form dominates the H-norm, with constant the norm of the solution operator: ‖J v‖² ≤ ‖S‖ · B v v. This is Cauchy--Schwarz in the energy form, applied to v and to the solution w of B w u = ⟪J v, J u⟫; no compactness of J is used.

theorem IsCoercive.inv_norm_formSolutionOperator_mul_norm_apply_sq_le {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) (v : V) : ‖hB.formSolutionOperator J‖⁻¹ * ‖J v‖ ^ 2 ≤ (B v) v

The Rayleigh lower bound: ‖S‖⁻¹ ‖J v‖² ≤ B v v for every v : V. For the Dirichlet problem this is the Poincaré inequality with the reciprocal solution-operator norm as its constant. Beyond coercivity, only symmetry is needed: when S = 0 the left-hand side vanishes and the bound is the nonnegativity of the energy.

The Rayleigh principle

theorem IsCoercive.isLeast_rayleighQuotient {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) (hsymm : ∀ (u v : V), (B u) v = (B v) u) (hJne : J ≠ 0) : IsLeast {r : ℝ | ∃ (v : V), J v ≠ 0 ∧ (B v) v / ‖J v‖ ^ 2 = r} ‖hB.formSolutionOperator J‖⁻¹

The Rayleigh principle: the least variational eigenvalue ‖S‖⁻¹ is the minimum of the Rayleigh quotient B v v / ‖J v‖² over the vectors with J v ≠ 0. The minimum is attained at an eigenfunction, which is why compactness of J is assumed.

theorem IsCoercive.isGreatest_inv_norm_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) (hJne : J ≠ 0) : IsGreatest {C : ℝ | ∀ (v : V), C * ‖J v‖ ^ 2 ≤ (B v) v} ‖hB.formSolutionOperator J‖⁻¹

The reciprocal solution-operator norm is the optimal constant in the inequality C ‖J v‖² ≤ B v v: it satisfies the inequality, and no larger constant does. For the Dirichlet problem this identifies the quantity defined as firstDirichletEigenvalue with the best Poincaré constant. Unlike attainment of the Rayleigh minimum, this characterization does not require compactness of J.