Skip to content

Erdős problem 1125

Let f:R→Rf:\mathbb{R}\to \mathbb{R} be such that 2f(x)≤f(x+h)+f(x+2h)2f(x) \leq f(x+h)+f(x+2h) for every x∈Rx\in \mathbb{R} and h>0h>0. Must ff be monotonic?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1125.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1125.leanErdos1125.erdos_11251 lineExact file
True ↔ ∀ (f : ℝ → ℝ), (∀ (x h : ℝ), h > 0 → 2 * f x ≤ f (x + h) + f (x + 2 * h)) → Monotone f
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1125
  • PLBY Lean proofsErdosProblems.Erdos1125

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page