Exact attained minimum of a sum of squares under a reciprocal constraint
ProvedWorkbookCorrected.plus_27694corrected-formalizationlean-workbooksource-checked
For positive real numbers a,b satisfying2/a+3/b=1, the minimum of a²+b² is(2^(2/3)+3^(2/3))³. Writing u=∛2,v=∛3 and S=u²+v², it is attained at a=uS,b=vS.
Formalization Note: The source asks to find the minimum; its original formalization only asserted the weak lower bound6. This correction gives the exact universal lower bound and an attaining positive feasible pair. The cube roots are represented by positive real u,v satisfying u³=2,v³=3.
Source: InternLM Lean-Workbook, record lean_workbook_plus_27694 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_27694 (u v : ℝ) (hu : 0<u) (hv : 0<v) (hu3 : u^3=2) (hv3 : v^3=3) :
(∀ a b : ℝ, 0<a → 0<b → 2/a+3/b=1 → (u^2+v^2)^3 ≤ a^2+b^2) ∧
(∃ a b : ℝ, 0<a ∧ 0<b ∧ 2/a+3/b=1 ∧ a^2+b^2=(u^2+v^2)^3) := by sorrySource