lean_workbook_plus_55770

Proved

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

For the first part , \n\n $a^2b^2+b^2c^2+c^2a^2\ge (ab)(bc)+(bc)(ca)+(ca)(ab)$ \n\n $\implies \sum_{cyc} a^2b^2\ge abc(a+b+c)$ \n\n $\implies \frac{\sum_{cyc} a^2b^2}{a^2b^2c^2}\ge \frac{abc(a+b+c)}{a^2b^2c^2}$ \n\n $\implies \frac{1}{a^2} + \frac{1}{b^2}+\frac{1}{c^2} \ge \frac{1}{ab}+\frac{1}{bc}+\frac{1}{ca}$ \n\nOr simply, \n\n $\frac{1}{a^2} + \frac{1}{b^2}+\frac{1}{c^2} \ge (\frac{1}{a})(\frac{1}{b})+(\frac{1}{b})(\frac{1}{c})+(\frac{1}{c})(\frac{1}{a})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55770  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  1 / a^2 + 1 / b^2 + 1 / c^2 ≥ 1 / (a * b) + 1 / (b * c) + 1 / (c * a)   :=  by sorry

Source

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

View graph