Euler-Lagrange equation under an L^q constraint

A vector U minimising a nonnegative quadratic Q over {W : ‖T W‖_{L^q} = 1}, for a continuous linear T into L^q(μ) with q > 1, satisfies

L = Q U ∫ |TU|^{q-2} (TU) (TV),

where L is the coefficient of 2t in Q (U + tV). The multiplier is the minimum itself, so no unknown constant survives.

Two instances follow. At Q W = ‖W‖² the coefficient is ⟪U, V⟫ and the equation reads ⟪U, V⟫ = ‖U‖² ∫ |TU|^{q-2} (TU) (TV). At Q W = B[W, W] for a symmetric positive semidefinite B it is B[U, V] = B[U, U] ∫ |TU|^{q-2} (TU) (TV). On H₀¹(Ω) the first gives -Δu + u = λ|u|^{q-2}u, since the graph inner product is ∫uv + ∫∇u·∇v, and the second at the bilinear form of the Laplacian gives -Δu = λ|u|^{q-2}u, which is the equation of Guo's Section IX.1.

The argument is Fermat's theorem applied to g(t) = Q (U + tV) - Q U ‖T(U + tV)‖²_{L^q}, which vanishes at t = 0 and is nonnegative everywhere: rescaling U + tV to the constraint set is admissible whenever its image is nonzero, and where the image vanishes the second term does too. EllipticPdes.Analysis.hasDerivAt_integral_abs_rpow differentiates the constraint, and the chain rule through x ↦ x^{2/q} turns that into the derivative of the squared L^q norm.

Main declarations

• EllipticPdes.Analysis.norm_lp_rpow_eq_integral: ‖f‖^q = ∫ |f|^q.
• EllipticPdes.Analysis.euler_lagrange_of_quadratic_min: the equation for a quadratic.
• EllipticPdes.Analysis.euler_lagrange_of_bilin_min: the equation for a bilinear form.
• EllipticPdes.Analysis.euler_lagrange_of_norm_min: the equation for the norm.

References

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

theorem EllipticPdes.Analysis.norm_lp_rpow_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (f : ↥(MeasureTheory.Lp ℝ p μ)) : ‖f‖ ^ p.toReal = ∫ (x : α), ‖↑↑f x‖ ^ p.toReal ∂μ

L^q norm to the q-th power as an integral.

The equation for a quadratic

theorem EllipticPdes.Analysis.euler_lagrange_of_quadratic_min {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] {p : ENNReal} [Fact (1 ≤ p)] (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (hp1 : 1 < p.toReal) (T : H →L[ℝ] ↥(MeasureTheory.Lp ℝ p μ)) {Q : H → ℝ} (hQnonneg : ∀ (W : H), 0 ≤ Q W) (hQsmul : ∀ (c : ℝ) (W : H), Q (c • W) = c ^ 2 * Q W) {U V : H} {L S : ℝ} (hexp : ∀ (t : ℝ), Q (U + t • V) = Q U + 2 * t * L + t ^ 2 * S) (hU : ‖T U‖ = 1) (hmin : ∀ (W : H), ‖T W‖ = 1 → Q U ≤ Q W) : L = Q U * ∫ (x : α), |↑↑(T U) x| ^ (p.toReal - 2) * ↑↑(T U) x * ↑↑(T V) x ∂μ

Euler-Lagrange equation of a quadratic minimiser under an L^q constraint. Let Q be nonnegative and homogeneous of degree two, and let U minimise Q over the vectors whose image has unit L^q norm. If Q (U + tV) = Q U + 2tL + t²S, then

L = Q U ∫ |TU|^{q-2} (TU) (TV).

The two hypotheses on Q are exactly what the rescaling argument uses: homogeneity returns U + tV to the constraint set, and nonnegativity covers the vectors the constraint map kills.

theorem EllipticPdes.Analysis.euler_lagrange_of_bilin_min {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] {p : ENNReal} [Fact (1 ≤ p)] (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (hp1 : 1 < p.toReal) (T : H →L[ℝ] ↥(MeasureTheory.Lp ℝ p μ)) (B : H →L[ℝ] H →L[ℝ] ℝ) (hsymm : ∀ (W Z : H), (B W) Z = (B Z) W) (hpsd : ∀ (W : H), 0 ≤ (B W) W) {U : H} (hU : ‖T U‖ = 1) (hmin : ∀ (W : H), ‖T W‖ = 1 → (B U) U ≤ (B W) W) (V : H) : (B U) V = (B U) U * ∫ (x : α), |↑↑(T U) x| ^ (p.toReal - 2) * ↑↑(T U) x * ↑↑(T V) x ∂μ

Euler-Lagrange equation of a bilinear minimiser under an L^q constraint. For a symmetric positive semidefinite B, a minimiser of B[·, ·] on the unit L^q sphere satisfies

B[U, V] = B[U, U] ∫ |TU|^{q-2} (TU) (TV).

At the bilinear form of the Laplacian on H₀¹(Ω) this is the weak form of -Δu = λ|u|^{q-2}u, with λ = ∫ |∇u|².

The equation for the norm

theorem EllipticPdes.Analysis.euler_lagrange_of_norm_min {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {p : ENNReal} [Fact (1 ≤ p)] (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (hp1 : 1 < p.toReal) (T : H →L[ℝ] ↥(MeasureTheory.Lp ℝ p μ)) {U : H} (hU : ‖T U‖ = 1) (hmin : ∀ (W : H), ‖T W‖ = 1 → ‖U‖ ≤ ‖W‖) (V : H) : inner ℝ U V = ‖U‖ ^ 2 * ∫ (x : α), |↑↑(T U) x| ^ (p.toReal - 2) * ↑↑(T U) x * ↑↑(T V) x ∂μ

Euler-Lagrange equation of a norm minimiser under an L^q constraint. If U minimises ‖·‖ over the vectors whose image has unit L^q norm, then for every V

⟪U, V⟫ = ‖U‖² ∫ |TU|^{q-2} (TU) (TV).

The multiplier is the square of the minimum, so the equation names its own constant.