One-dimensional Poincaré inequality

Upstreamed to Mathlib as EllipticPdes.Analysis.PoincareInequality.

This file re-exports the Mathlib declarations under the EllipticPdes.Poincare namespace for backward compatibility.

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

theorem EllipticPdes.Poincare.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

Alias of MeasureTheory.intervalIntegral_mul_sq_le.

theorem EllipticPdes.Poincare.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

Alias of MeasureTheory.sq_intervalIntegral_le.

theorem EllipticPdes.Poincare.poincare_oneDim {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

Alias of MeasureTheory.poincare_1d.