lean_workbook_plus_81357
DisprovedBy Cauchy–Schwarz inequality,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81357 : ∀ a : ℝ, (a + 1) ^ 2 / (a ^ 2 + 1) ^ 2 ≤ 1 / (a ^ 2 - a + 1) := by sorry
Source
By Cauchy–Schwarz inequality,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_81357 : ∀ a : ℝ, (a + 1) ^ 2 / (a ^ 2 + 1) ^ 2 ≤ 1 / (a ^ 2 - a + 1) := by sorry