Poincare

Auxiliary lemmas

M1: Poincaré inequality on intervals (weak version)

theorem FockSPR.MissingMathlib.poincare_interval {h : ℝ} (hh : 0 < h) {f f' : ℝ → ℂ} (hf : ∀ x ∈ Set.Icc 0 h, HasDerivAt f (f' x) x) (hf_cont : ContinuousOn f (Set.Icc 0 h)) (hf'_cont : ContinuousOn f' (Set.Icc 0 h)) : have f_bar := (1 / h) • ∫ (x : ℝ) in 0..h, f x; ∫ (x : ℝ) in 0..h, ‖f x - f_bar‖ ^ 2 ≤ h ^ 2 * ∫ (x : ℝ) in 0..h, ‖f' x‖ ^ 2

Weak Poincaré inequality on [0, h]: for an absolutely continuous function f, ∫_0^h ‖f(x) − f_bar‖² dx ≤ h² ∫_0^h ‖f'(x)‖² dx where f_bar = (1/h) ∫_0^h f(x) dx.