Prove2Me

lean_workbook_plus_60642

Proved

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

Let a,b>0.a,b>0 . Prove that \n

ab+ba+kaba2+b2≥k+42\frac{a}{b} + \frac{b}{a} + \frac{kab}{a^2 +b^2} \geq \frac{k+4}{2}

Where 0≤k≤40\leq k\leq 4

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60642 (a b : ℝ) (hab : 0 < a ∧ 0 < b) (k : ℝ) (hk : 0 ≤ k ∧ k ≤ 4) : a / b + b / a + k * a * b / (a ^ 2 + b ^ 2) ≥ (k + 4) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph