lean_workbook_plus_78108

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that there is no function $f: R^+->R^+$ such that $f^2(x) \ge f(x+y)(f(x) + y)$ for any x, y > 0.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78108    (f : ℝ → ℝ)
    (hpos : ∀ x : ℝ, 0 < x → 0 < f x)
    (hf : (∀ x y : ℝ, 0 < x ∧ 0 < y → (f (x + y)) ≤ (f x)^2 / (f x + y))) :
    False   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph