lean_workbook_plus_1442

Proved

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

Prove that $\frac{1}{m^{2}}+\frac{1}{n^{2}}\ge \frac{16}{1+8mn}$ if $m,n\ge 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1442 (m n : ℝ) (hm : 1 ≤ m) (hn : 1 ≤ n) (hmn : 1 ≤ m * n) : 1 / m ^ 2 + 1 / n ^ 2 ≥ 16 / (1 + 8 * m * n)   :=  by sorry

Source