lean_workbook_plus_75043

Proved

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

Find the minimum value of $f(x,y)=\frac{2020x}{y}+\frac{y}{2020x}$ if $x,y$ are positive real numbers such that $x+y=2020$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75043 (x y : ℝ) (h₁ : 0 < x ∧ 0 < y) (h₂ : x + y = 2020) : 2 ≤ 2020 * x / y + y / (2020 * x)   :=  by sorry

Source