Positivity and derivative of the integral of |u| ^ p

For a continuous function u ≠ 0 on a compact space with a finite measure that is positive on nonempty open sets, the integral ∫ |u| ^ p dμ is positive for every p > 0.

For p > 1 the function s ↦ |s| ^ p is differentiable with derivative p |s| ^ (p - 2) s (hasDerivAt_abs_rpow). This file differentiates the integral t ↦ ∫ |u + t v| ^ p dμ under the integral sign, for continuous u and v on a compact space with a finite measure:

d/dt ∫ |u + t v| ^ p dμ |_(t = 0) = p ∫ |u| ^ (p - 2) u v dμ.

This is the directional derivative of the p-th power of the Lᵖ norm at u in the direction v. It is the derivative of the denominator in the first variation of a Rayleigh-type quotient (∫ (energy of u) dμ) / (∫ |u| ^ p dμ) ^ (2 / p), such as the Yamabe quotient.

Main declarations

• TauCeti.integral_abs_rpow_pos: positivity of ∫ |u| ^ p dμ for a continuous u ≠ 0.
• TauCeti.hasDerivAt_integral_abs_add_mul_rpow: the derivative of t ↦ ∫ |u + t v| ^ p dμ at t = 0.

theorem TauCeti.integral_abs_rpow_pos {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.IsOpenPosMeasure] {u : X → ℝ} (hu : Continuous u) (hu0 : u ≠ 0) {p : ℝ} (hp : 0 < p) : 0 < ∫ (x : X), |u x| ^ p ∂μ

The integral ∫ |u| ^ p dμ of a continuous function u ≠ 0 on a compact space is positive for p > 0, when the finite measure μ is positive on nonempty open sets.

theorem TauCeti.hasDerivAt_integral_abs_add_mul_rpow {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {u v : X → ℝ} (hu : Continuous u) (hv : Continuous v) {p : ℝ} (hp : 1 < p) : HasDerivAt (fun (t : ℝ) => ∫ (x : X), |u x + t * v x| ^ p ∂μ) (p * ∫ (x : X), |u x| ^ (p - 2) * u x * v x ∂μ) 0

Differentiating ∫ |u + t v| ^ p dμ. For continuous u and v on a compact space with a finite measure and p > 1, the derivative of t ↦ ∫ |u + t v| ^ p dμ at t = 0 is p ∫ |u| ^ (p - 2) u v dμ.