A shifted-product bound on the unit circle

Proved

WorkbookSource.plus_30516

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

lean-workbooksource-checked

Let $a,b$ be reals such that $a^2+ b^ 2= 1.$ Prove that $(a+1)(a+2b + 1)\leq \frac{27}{5}$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_30516 (a b : ℝ) (h : a^2 + b^2 = 1) : (a + 1) * (a + 2 * b + 1) ≤ 27 / 5   :=  by sorry

Source