Direct method under a subcritical constraint

Minimising the H₀¹ norm over the functions of unit L^q(Ω) norm has a solution when q < 2⋆. This is the direct method of the calculus of variations, and it is where the two halves of the compactness chapter meet: EllipticPdes.Analysis.exists_weakLimit supplies a weak limit of a minimising sequence, and EllipticPdes.Embedding.rellichEmbL_isCompact_of_lt supplies the strong L^q convergence that takes the constraint to that limit.

At q = 2⋆ the second half fails, which EllipticPdes.Embedding.not_isCompactOperator_critEmb records, and the minimum need not be attained. That is the exponent restriction Guo writes as p + 1 < 2⋆ for the semilinear problem -Δu = u^p, whose Euler-Lagrange equation this minimiser solves once the constraint is differentiated.

Main declarations

• EllipticPdes.Embedding.exists_minimiser_of_lt: the minimiser exists.
• EllipticPdes.Embedding.exists_weakSolution_semilinear_of_lt: it solves the equation.

References

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

theorem EllipticPdes.Embedding.exists_minimiser_of_lt {d : ℕ} {p' q : NNReal} [Fact (1 ≤ ↑q)] (hΩb : Bornology.IsBounded (Metric.ball 0 1)) (hd : 2 < d) (hq : (↑2)⁻¹ - (↑d)⁻¹ ≤ (↑q)⁻¹) (hq0 : q ≠ 0) (hp' : (↑p')⁻¹ = (↑2)⁻¹ - (↑d)⁻¹) (hp'0 : p' ≠ 0) (hqlt : q < p') (hq2 : 2 ≤ q) (hne : ∃ (V : ↥(Sobolev.H01 (Metric.ball 0 1))), ‖(rellichEmbL ⋯ hΩb hd hq) V‖ = 1) : ∃ (U : ↥(Sobolev.H01 (Metric.ball 0 1))), ‖(rellichEmbL ⋯ hΩb hd hq) U‖ = 1 ∧ ∀ (V : ↥(Sobolev.H01 (Metric.ball 0 1))), ‖(rellichEmbL ⋯ hΩb hd hq) V‖ = 1 → ‖U‖ ≤ ‖V‖

Direct method. Below the critical exponent the H₀¹ norm attains its minimum on the functions of unit L^q norm.

theorem EllipticPdes.Embedding.exists_norm_rellichEmbL_eq_one {d : ℕ} {q : NNReal} [Fact (1 ≤ ↑q)] (hΩb : Bornology.IsBounded (Metric.ball 0 1)) (hd : 2 < d) (hq0 : q ≠ 0) (hq : (↑2)⁻¹ - (↑d)⁻¹ ≤ (↑q)⁻¹) : ∃ (V : ↥(Sobolev.H01 (Metric.ball 0 1))), ‖(rellichEmbL ⋯ hΩb hd hq) V‖ = 1

The constraint set is inhabited: a renormalised bump sits on it.

theorem EllipticPdes.Embedding.exists_weakSolution_semilinear_of_lt {d : ℕ} {p' q : NNReal} [Fact (1 ≤ ↑q)] (hΩb : Bornology.IsBounded (Metric.ball 0 1)) (hd : 2 < d) (hq : (↑2)⁻¹ - (↑d)⁻¹ ≤ (↑q)⁻¹) (hq0 : q ≠ 0) (hp' : (↑p')⁻¹ = (↑2)⁻¹ - (↑d)⁻¹) (hp'0 : p' ≠ 0) (hqlt : q < p') (hq2 : 2 ≤ q) : ∃ (U : ↥(Sobolev.H01 (Metric.ball 0 1))), ‖(rellichEmbL ⋯ hΩb hd hq) U‖ = 1 ∧ ∀ (V : ↥(Sobolev.H01 (Metric.ball 0 1))), inner ℝ U V = ‖U‖ ^ 2 * ∫ (x : EuclideanSpace ℝ (Fin d)) in Metric.ball 0 1, |↑↑((rellichEmbL ⋯ hΩb hd hq) U) x| ^ (↑q - 2) * ↑↑((rellichEmbL ⋯ hΩb hd hq) U) x * ↑↑((rellichEmbL ⋯ hΩb hd hq) V) x

Minimiser as a weak solution. Differentiating the constraint through EllipticPdes.Analysis.euler_lagrange_of_norm_min turns the subcritical minimiser into a weak solution of -Δu + u = λ|u|^{q-2}u on the unit ball, with λ = ‖u‖²_{H₀¹}: the graph inner product ⟪U, V⟫ is ∫ uv + ∫ ∇u · ∇v, so the identity below is the weak form of that equation. The multiplier is the square of the minimum, so no unknown constant survives.