A midpoint-concave real sequence that is bounded below is nondecreasing

Proved

FiniteEnergyPlane.monotone_of_add_le_two_mul_of_bddBelow

by Mazecto · Oct 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitiesreal-analysissequences

Let $(a_k)_{k\in\mathbb{N}}$ be a real sequence with $a_k\ge m$ for all $k$ , for some $m\in\mathbb{R}$ , and with $a_k+a_{k+2}\le 2a_{k+1}$ for all $k$ . Then $(a_k)$ is nondecreasing.

A discrete analogue of the fact that a concave function on $[0,\infty)$ that is bounded below is nondecreasing. It is useful for comparing optimal rates attached to successive orders.

Formalization Note The conclusion is Monotone a for a : ℕ → ℝ.

Preamble

import Mathlib

Formal statement

namespace FiniteEnergyPlane

/-- A real sequence on `ℕ` that is bounded below and satisfies `a k + a (k + 2) ≤ 2 a (k + 1)` for
all `k` is monotone. -/
theorem monotone_of_add_le_two_mul_of_bddBelow (a : ℕ → ℝ) (m : ℝ) (hm : ∀ k, m ≤ a k)
    (hc : ∀ k, a k + a (k + 2) ≤ 2 * a (k + 1)) : Monotone a := by
  sorry

end FiniteEnergyPlane

Source

Elementary real analysis; used for U. Hryniewicz, J. Symplectic Geom. 12 (2014), Theorem 2.10

View graph