An asymmetric sum of linear squared and cubed ratios is at least three
ProvedWorkbookSource.plus_81823lean-workbooksource-checked
Let Prove that: \begin{align*} \frac{a}{b}+ \left( \frac{3b+c}{3c+b} \right)^2 + \left( \frac{2c+a}{2a+c} \right)^3 \ge 3 .\end{align*}
Source: InternLM Lean-Workbook, record lean_workbook_plus_81823 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_81823 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b + (3 * b + c) ^ 2 / (3 * c + b) ^ 2 + (2 * c + a) ^ 3 / (2 * a + c) ^ 3 ≥ 3 := by sorry
Source