A parameterized quadratic-product inequality

Proved

WorkbookSource.base_10230

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

$M(M+2kc^2)(1-k^2) \leq (M+(k-k^2)c^2)^2,$

Source: InternLM Lean-Workbook, record lean_workbook_10230 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_10230 (M c k : ℝ) : M * (M + 2 * k * c ^ 2) * (1 - k ^ 2) ≤ (M + (k - k ^ 2) * c ^ 2) ^ 2  :=  by sorry

Source