Direct method for a coercive symmetric form

A symmetric coercive form B on a real Hilbert space H attains its minimum on the set {U : ‖T U‖ = 1}, for any compact T : H →L[ℝ] E into a normed space whose unit sphere the image meets. This is the abstract direct method of the calculus of variations, where compactness of the constraint map is what takes the constraint to a weak limit.

Three ingredients. Coercivity bounds a minimising sequence in H, so EllipticPdes.Analysis.exists_weakLimit supplies a weak limit w. Compactness of T takes a further subsequence to a strong limit z in E, and duality identifies z with T w, whence ‖T w‖ = 1. Weak lower semicontinuity of B, which is the expansion of 0 ≤ B[uₖ - w, uₖ - w] against B[uₖ, w] → B[w, w], gives B[w, w] ≤ inf.

The identification of z needs no adjoint, and so asks nothing of E beyond a norm: for a functional g on E the composite g ∘ T is a functional on H, Riesz names the vector it pairs against, and the weak convergence in H gives g (T uₖ) → g (T w). Two elements of E on which every functional agrees are equal.

Taking E = L²(Ω) and T the Rellich embedding recovers the Rayleigh problem of EllipticPdes.Sobolev.exists_rayleigh_minimiser, where the constraint is quadratic and the minimiser satisfies a linear equation. Taking E = L^q(Ω) for a subcritical q gives the semilinear problem, where the constraint is not quadratic and the equation is -Δu = λ|u|^{q-2}u.

Main declarations

• EllipticPdes.Analysis.bilin_self_nonneg: a coercive form is positive semidefinite.
• EllipticPdes.Analysis.bilin_le_of_weakLimit: weak lower semicontinuity.
• EllipticPdes.Analysis.exists_bilin_minimiser: the minimum is attained.

References

James Guo, Partial Differential Equations, Section IX.1; L. C. Evans, Partial Differential Equations (2nd ed.), §8.2.

theorem EllipticPdes.Analysis.bilin_self_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : H →L[ℝ] H →L[ℝ] ℝ} (hco : IsCoercive B) (U : H) : 0 ≤ (B U) U

A coercive form is positive semidefinite.

theorem EllipticPdes.Analysis.bilin_sub_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : H →L[ℝ] H →L[ℝ] ℝ} (hsymm : ∀ (U V : H), (B U) V = (B V) U) (U V : H) : (B (U - V)) (U - V) = (B U) U - 2 * (B U) V + (B V) V

The form on a difference, expanded by symmetry.

theorem EllipticPdes.Analysis.bilin_le_of_weakLimit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : H →L[ℝ] H →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : H), (B U) V = (B V) U) {u : ℕ → H} {w : H} {L : ℝ} (hweak : ∀ (v : H), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ w v))) (hlim : Filter.Tendsto (fun (k : ℕ) => (B (u k)) (u k)) Filter.atTop (nhds L)) : (B w) w ≤ L

Weak lower semicontinuity of a symmetric coercive form. If uₖ converges weakly to w and B[uₖ, uₖ] converges to L, then B[w, w] ≤ L. Positive semidefiniteness applied to uₖ - w is the whole argument; no Cauchy-Schwarz for B is needed.

theorem EllipticPdes.Analysis.exists_bilin_minimiser {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : H →L[ℝ] H →L[ℝ] ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (hco : IsCoercive B) (hsymm : ∀ (U V : H), (B U) V = (B V) U) (T : H →L[ℝ] E) (hT : IsCompactOperator ⇑↑T) (hne : ∃ (V : H), ‖T V‖ = 1) : ∃ (U : H), ‖T U‖ = 1 ∧ ∀ (V : H), ‖T V‖ = 1 → (B U) U ≤ (B V) V

Direct method for a coercive symmetric form. With T compact and its image meeting the unit sphere of E, the form attains its minimum on {U : ‖T U‖ = 1}.