Inequalities

Classical inequalities for sums, sequences, means and integrals of real or complex numbers: Hardy, Hilbert, Carleman, Wirtinger, Opial, Landau–Kolmogorov, Hermite–Hadamard, Kantorovich and Popoviciu, power-sum and elementary log/exp bounds; inequalities stated with Sobolev norms go to Function spaces, eigenvalue inequalities to Operator theory.

TheoremA bound on a difference of reciprocals#●ready to prove

For all real numbers \(a > 1\) and \(x \ge 1\),

\[ \frac{1}{1+x}-\frac{1}{1+ax}\le \frac{\sqrt{a}-1}{\sqrt{a}+1}. \]

public theorem_wanted one_div_one_add_sub_one_div_one_add_mul_le
    {a x : ℝ} (ha : 1 < a) (hx : 1 ≤ x) :
    (1 / (1 + x) - 1 / (1 + a * x)) ≤ (Real.sqrt a - 1) / (Real.sqrt a + 1)

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Inequalities in real analysis), problem ma_proofbench_l1_01.

TheoremHardy's inequality#✓fully proved

Let \(p > 1\) be a real number and let \((a_n)_{n \ge 0}\) be a sequence of nonnegative real numbers such that \(\sum_n a_n^p\) converges. Write \(A_n = \frac{1}{n+1} \sum_{i=0}^{n} a_i\) for the average of \(a_0, \dots, a_n\). Then \(\sum_n A_n^p\) converges and

\[\sum_{n=0}^{\infty} A_n^p \le \left(\frac{p}{p-1}\right)^p \sum_{n=0}^{\infty} a_n^p.\]

Proof: Elliott's finite telescoping argument is combined with Young's and Hölder's inequalities, following E. B. Elliott (1926) as presented in Hardy--Littlewood--Pólya, Inequalities, Theorem 326.

theorem hardy_inequality {a : ℕ → ℝ} {p : ℝ} (hp : 1 < p)
    (hnonneg : ∀ n, 0 ≤ a n)
    (hsumm : Summable fun n => (a n).rpow p) :
    Summable (fun n => ((Finset.sum (Finset.range (n + 1)) a / ((n : ℝ) + 1)).rpow p)) ∧
    ∑' n, ((Finset.sum (Finset.range (n + 1)) a / ((n : ℝ) + 1)).rpow p) ≤
      (p / (p - 1)).rpow p * ∑' n, (a n).rpow p

Sources

G. H. Hardy, Note on a theorem of Hilbert, Mathematische Zeitschrift 6 (1920), 314-317: the discrete series form with constant (p / (p - 1)) ^ p for p > 1.

Used by 2

Used byThe Cesàro operator is bounded by 2 · Cesàro means of square-summable sequences are square-summable

TheoremHermite–Hadamard inequality#✓fully proved

Let \(a < b\) be real numbers and let \(f \colon \mathbb{R} \to \mathbb{R}\) be convex on \([a, b]\). Then \(f\left(\frac{a+b}{2}\right) \le \frac{1}{b-a} \int_a^b f(x)\,dx\) and \(\frac{1}{b-a} \int_a^b f(x)\,dx \le \frac{f(a) + f(b)}{2}\).

theorem hermite_hadamard {f : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hf : ConvexOn ℝ (Set.Icc a b) f) :
    f ((a + b) / 2) ≤ (1 / (b - a)) * ∫ x in a..b, f x ∧
    (1 / (b - a)) * ∫ x in a..b, f x ≤ (f a + f b) / 2

Sources

https://en.wikipedia.org/wiki/Hermite%E2%80%93Hadamard_inequality.

TheoremInequality for square-summable complex sequences#●ready to prove

Let \((\alpha_n)_{n \ge 1}\) be complex numbers with \(\sum_{n \ge 1} |\alpha_n|^2 < \infty\), and for \(k \ge 0\) put \(\beta_k = \sum_{l \ge 0} \alpha_{2^k(2l+1)} / (l+1)\). Then each series defining \(\beta_k\) converges absolutely, \(\sum_{k \ge 0} |\beta_k|^2 < \infty\), and

\[\sum_{n \ge 1} |\alpha_n|^2 \ge \frac{6}{\pi^2} \sum_{k \ge 0} |\beta_k|^2.\]

The inequality follows from the Cauchy–Schwarz inequality.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∀ α : ℕ → ℂ, Summable (fun n => ‖α (n + 1)‖ ^ 2) →
    (∀ k : ℕ, Summable (fun l => α (2 ^ k * (2 * l + 1)) / (l + 1 : ℂ))) ∧
    Summable (fun k => ‖∑' l, α (2 ^ k * (2 * l + 1)) / (l + 1 : ℂ)‖ ^ 2) ∧
      ∑' n, ‖α (n + 1)‖ ^ 2 ≥
        6 / Real.pi ^ 2 * ∑' k, ‖∑' l, α (2 ^ k * (2 * l + 1)) / (l + 1 : ℂ)‖ ^ 2

WantedExt/Analysis/SquareSummableComplexInequalityWanted.lean:36

Sources

Open Problem Garden solution comment 73221, https://www.openproblemgarden.org/op/inequality_for_square_summable_complex_series#comment-73221.

TheoremOpial's inequality with one boundary condition#●ready to prove

Let \(\alpha \le \beta\) be real numbers and let \(f : \mathbb{R} \to \mathbb{R}\) be continuously differentiable on \([\alpha, \beta]\) with \(f(\alpha) = 0\). Then

\[\int_\alpha^\beta |f(x) f'(x)|\,dx \le \frac{\beta - \alpha}{2} \int_\alpha^\beta |f'(x)|^2\,dx.\]

public theorem_wanted integral_abs_mul_deriv_le_of_eq_zero_left {α β : ℝ} (hαβ : α ≤ β) {f : ℝ → ℝ}
    (hf : ContDiffOn ℝ 1 f (Set.Icc α β))
    (hfa : f α = 0) :
    (∫ x in α..β, |f x * deriv f x|)
      ≤ ((β - α) / 2) * ∫ x in α..β, (|deriv f x| ^ 2)

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Inequalities in real analysis), problem ma_proofbench_l1_76.

TheoremWirtinger's inequality#✓fully proved

Let \(f, f' : \mathbb{R} \to \mathbb{R}\) be functions such that for every \(x \in [0, \pi]\) the function \(f\) has derivative \(f'(x)\) at \(x\) within \([0, \pi]\), \(f'\) is continuous on \([0, \pi]\), and \(f(0) = f(\pi) = 0\). Then \(\int_0^\pi f(x)^2 \, dx \le \int_0^\pi f'(x)^2 \, dx\).

Proof: A Picone-type comparison. For 0 < c < 1 the weight h x = -c * tan (c * (x - π / 2)) is smooth on [0, π] with h' + h ^ 2 = -c ^ 2, so integrating f' ^ 2 = (f' - h * f) ^ 2 + (h * f ^ 2)' + c ^ 2 * f ^ 2 gives c ^ 2 * ∫ f ^ 2 ≤ ∫ f' ^ 2; then let c tend to one.

public theorem wirtinger_inequality (f f' : ℝ → ℝ)
    (hf_deriv : ∀ x ∈ Set.Icc (0 : ℝ) Real.pi,
      HasDerivWithinAt f (f' x) (Set.Icc 0 Real.pi) x)
    (hf_deriv_cont : ContinuousOn f' (Set.Icc 0 Real.pi))
    (h0 : f 0 = 0) (hpi : f Real.pi = 0) :
    intervalIntegral (fun x => (f x) ^ 2) 0 Real.pi MeasureTheory.volume ≤
      intervalIntegral (fun x => (f' x) ^ 2) 0 Real.pi MeasureTheory.volume

Sources

G. H. Hardy, J. E. Littlewood, and G. Pólya, Inequalities, second edition, Cambridge University Press, 1952, §7.7 (the endpoint-zero form on [0, L]).

Used by 1

Used byWirtinger's inequality on an interval

3 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.