lean_workbook_plus_72948

Proved

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

Let $a\ge c \ge 0,b\ge d\ge0$ and $4a+3d=4b+3c$ . Prove that : $\sqrt{ab}\ge \frac{c+d}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72948 (a b c d : ℝ) (h1 : a ≥ c ∧ c ≥ 0 ∧ b ≥ d ∧ d ≥ 0) (h2 : 4 * a + 3 * d = 4 * b + 3 * c) : √(a * b) ≥ (c + d) / 2   :=  by sorry

Source

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

View graph