Prove2Me

lean_workbook_plus_47413

Proved

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

Note that \n\n (1+a4)(1+b4)=(1+a4)(1+b4)(a4+1)(1+b4)≥(1+a2b2)(a2+b2)=a2(1+b4)+b2(1+a4).(1+a^4)(1+b^4)=\sqrt{(1+a^4)(1+b^4)}\sqrt{(a^4+1)(1+b^4)}\geq (1+a^2b^2)(a^2+b^2)=a^2(1+b^4)+b^2(1+a^4). \n\n Equality holds iff a2=b2=1  ⟹  (a,b)⊂{(±1,±1)}.□a^2=b^2=1\implies (a,b)\subset \{(\pm 1, \pm 1)\}.\Box

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

View graph