lean_workbook_plus_28069

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find the minimum value of $f(r_1) = 8r_1 + 9 \cdot \frac{1 - r_1}{1 + r_1}$ and the corresponding value of $r_1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28069 (f : ℝ → ℝ) (r_1 : ℝ) (hf: f r_1 = 8 * r_1 + 9 * (1 - r_1) / (1 + r_1)) : ∃ r_1_min, f r_1_min ≤ f r_1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph