lean_workbook_plus_5936

Proved

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

Given $x,y > 0$ , find the minimum value of this expression: \n\n $\frac{1}{x^2+y^2}+\frac{x^2}{1+x^2}+\frac{y^2}{1+y^2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5936 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 1 ≤ 1 / (x ^ 2 + y ^ 2) + x ^ 2 / (1 + x ^ 2) + y ^ 2 / (1 + y ^ 2)   :=  by sorry

Source

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

View graph