Derivative of the L^q functional along a line

For u and v in L^q(μ) with q > 1, the map t ↦ ∫ |u + tv|^q is differentiable at 0, with derivative q ∫ |u|^{q-2} u v. This is the constraint derivative of the direct method: the subcritical minimiser of EllipticPdes.Embedding.exists_minimiser_of_lt lives on the unit sphere of L^q, and its Euler-Lagrange equation is this derivative set against the derivative of the H₀¹ norm.

The proof is differentiation under the integral sign. hasDerivAt_integral_of_dominated_loc_of_deriv_le asks for a dominating function on a neighbourhood of 0, and Hölder's inequality supplies one: the integrand's t-derivative is bounded on |t| < 1 by q(|u| + |v|)^{q-1}|v|, whose first factor lies in L^{q/(q-1)} and whose second lies in L^q. Mathlib's hasDerivAt_abs_rpow supplies the pointwise derivative, including at the origin, where q > 1 makes |·|^q differentiable with derivative zero.

Main declarations

• EllipticPdes.Analysis.integrable_abs_rpow_sub_one_mul: the dominating function is integrable.
• EllipticPdes.Analysis.hasDerivAt_integral_abs_rpow: the derivative at 0.

References

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

theorem EllipticPdes.Analysis.integrable_abs_rpow_sub_one_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hptop : p ≠ ⊤) (hp1 : 1 < p.toReal) {u v : α → ℝ} (hu : MeasureTheory.MemLp u p μ) (hv : MeasureTheory.MemLp v p μ) : MeasureTheory.Integrable (fun (x : α) => (‖u x‖ + ‖v x‖) ^ (p.toReal - 1) * ‖v x‖) μ

Integrability of the dominating function. With u and v in L^q, the product (|u| + |v|)^{q-1}|v| is integrable: the first factor lies in L^{q/(q-1)} and the second in L^q, whose reciprocals sum to one.

theorem EllipticPdes.Analysis.hasDerivAt_integral_abs_rpow {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (hp1 : 1 < p.toReal) {u v : α → ℝ} (hu : MeasureTheory.MemLp u p μ) (hv : MeasureTheory.MemLp v p μ) : HasDerivAt (fun (t : ℝ) => ∫ (x : α), |u x + t * v x| ^ p.toReal ∂μ) (∫ (x : α), p.toReal * |u x| ^ (p.toReal - 2) * u x * v x ∂μ) 0

Derivative of the L^q functional along a line. For u and v in L^q(μ) with q > 1, the map t ↦ ∫ |u + tv|^q is differentiable at 0 with derivative q ∫ |u|^{q-2} u v.