A quadratic bound under two ratio constraints
ProvedWorkbookSource.problem_10948lean-workbooksource-checked
Let and be two positive real numbers with Prove that .
Source: InternLM Lean-Workbook, record lean_workbook_10948 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_10948 (a b : ℝ) (h1 : 0 < a ∧ 0 < b) (h2 : a ≤ 3 * b) (h3 : 3 * b ≤ 5 * a) : a^2 + b^2 ≤ (10/3) * a * b := by sorry
Source