One-dimensional Poincaré inequality

For a continuously differentiable u on a compact interval [a, b] that vanishes at the left endpoint, the L² norm of u is controlled by the L² norm of its derivative: ∫ x in a..b, (u x) ^ 2 ≤ (b - a) ^ 2 / 2 * ∫ x in a..b, (u' x) ^ 2.

The argument has three steps. First, intervalIntegral_mul_sq_le is the Cauchy-Schwarz inequality for the interval integral, obtained from the nonnegativity of ∫ (f - λ g) ^ 2 read as a quadratic in λ whose discriminant is therefore nonpositive. Second, the fundamental theorem of calculus writes u x as ∫ t in a..x, u' t, which the Cauchy-Schwarz bound (with g = 1, sq_intervalIntegral_le) turns into the pointwise estimate (u x) ^ 2 ≤ M * (x - a) with M = ∫ t in a..b, (u' t) ^ 2. Third, integrating that estimate over [a, b] and evaluating ∫ x in a..b, (x - a) = (b - a) ^ 2 / 2 gives the constant.

Main results

• MeasureTheory.intervalIntegral_mul_sq_le: Cauchy-Schwarz for ∫ f g.
• MeasureTheory.sq_intervalIntegral_le: the g = 1 special case.
• MeasureTheory.poincare_1d: the one-dimensional Poincaré inequality.

theorem MeasureTheory.intervalIntegral_mul_sq_le {a b : ℝ} (hab : a ≤ b) {f g : ℝ → ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc a b)) : (∫ (t : ℝ) in a..b, f t * g t) ^ 2 ≤ (∫ (t : ℝ) in a..b, f t ^ 2) * ∫ (t : ℝ) in a..b, g t ^ 2

Cauchy-Schwarz for the interval integral: the square of ∫ f g is at most the product of ∫ f ^ 2 and ∫ g ^ 2. Proved from 0 ≤ ∫ (f - λ g) ^ 2, read as a nonnegative quadratic in λ whose discriminant must therefore be nonpositive.

theorem MeasureTheory.sq_intervalIntegral_le {a x : ℝ} (hax : a ≤ x) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.uIcc a x)) : (∫ (t : ℝ) in a..x, f t) ^ 2 ≤ (x - a) * ∫ (t : ℝ) in a..x, f t ^ 2

Cauchy-Schwarz with one factor constant: on [a, x] the square of the integral of f is at most (x - a) times the integral of f ^ 2. The g = 1 case of intervalIntegral_mul_sq_le.

theorem MeasureTheory.poincare_1d {a b : ℝ} (hab : a ≤ b) {u u' : ℝ → ℝ} (hderiv : ∀ y ∈ Set.uIcc a b, HasDerivAt u (u' y) y) (hu' : ContinuousOn u' (Set.uIcc a b)) (ha : u a = 0) : ∫ (x : ℝ) in a..b, u x ^ 2 ≤ (b - a) ^ 2 / 2 * ∫ (x : ℝ) in a..b, u' x ^ 2

One-dimensional Poincaré inequality. If u has derivative u' at every point of [a, b] with u' continuous there, and u a = 0, then ∫ x in a..b, (u x) ^ 2 ≤ (b - a) ^ 2 / 2 * ∫ x in a..b, (u' x) ^ 2.

A function compactly supported in (a, b) satisfies u a = 0, so this applies to each one-dimensional slice in the Fubini proof of the Poincaré inequality on a box, with constant (b - a) ^ 2 / 2.

theorem MeasureTheory.poincare_1d_of_tsupport {a b : ℝ} (hab : a ≤ b) {u u' : ℝ → ℝ} (hderiv : ∀ y ∈ Set.uIcc a b, HasDerivAt u (u' y) y) (hu' : ContinuousOn u' (Set.uIcc a b)) (hsupp : tsupport u ⊆ Set.Ioo a b) : ∫ (x : ℝ) in a..b, u x ^ 2 ≤ (b - a) ^ 2 / 2 * ∫ (x : ℝ) in a..b, u' x ^ 2

The one-dimensional Poincaré inequality for a function compactly supported in the open interval (a, b). Such a u vanishes at the left endpoint, so poincare_1d applies.

The compact-support companion of poincare_1d, kept for callers that have a tsupport hypothesis. The Fubini proof of the Poincaré inequality on a box takes poincare_1d directly, having the endpoint value to hand, so nothing else consumes this form.