Prove2Me

lean_workbook_plus_55702

Proved

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

Let a,b∈Ra,b\in R such that a2+b2≥4a^2+b^2\ge 4 . Then 94≥a2+(b+1)2a2+b2≥14.\frac{9}{4}\ge \frac{a^2+(b+1)^2}{a^2+b^2}\ge\frac{1}{4}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55702 (a b : ℝ) (h : a ^ 2 + b ^ 2 ≥ 4) :
  9 / 4 ≥ (a ^ 2 + (b + 1) ^ 2) / (a ^ 2 + b ^ 2) ∧ (a ^ 2 + (b + 1) ^ 2) / (a ^ 2 + b ^ 2) ≥ 1 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph