lean_workbook_plus_10623
Provedbasically we want x>point of equality, since after the point of equality, the difference between 2x and sqrtx grow exponentially (2x is always bigger after point of equality). the 2 points of equality of are and 0. so we take x>the larger of the 2, or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10623 : ∀ x > 1/4, Real.sqrt x < 2 * x := by sorry
Source