Two shifted square-root squared reciprocals have a sum lower bound
ProvedWorkbookSource.base_19966lean-workbooksource-checked
Prove that for ,
Source: InternLM Lean-Workbook, record lean_workbook_19966 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_19966 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (1 / (1 + Real.sqrt x) ^ 2 + 1 / (1 + Real.sqrt y) ^ 2) ≥ 2 / (x + y + 2) := by sorry
Source