lean_workbook_plus_16007
ProvedProve the inequality .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16007 : ∀ a b : ℝ, (a * b ≠ 0) → 1 / (2 * a ^ 2) + 1 / (2 * b ^ 2) ≥ 1 / |a * b| := by sorry
Source
Prove the inequality .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16007 : ∀ a b : ℝ, (a * b ≠ 0) → 1 / (2 * a ^ 2) + 1 / (2 * b ^ 2) ≥ 1 / |a * b| := by sorry