English
A specialization of Cauchy–Schwarz: for a finite set s and positive weights g_i, (∑ f_i)^2 / ∑ g_i ≤ ∑ f_i^2 / g_i, provided g_i > 0.
Русский
Специализация неравенства Коши–Шварца: для конечного множества и положительных весов g_i выполняется (∑ f_i)^2 / ∑ g_i ≤ ∑ f_i^2 / g_i, при g_i > 0.
LaTeX
$$$\frac{\left(\sum_{i\in s} f(i)\right)^2}{\sum_{i\in s} g(i)} \le \sum_{i\in s} \frac{f(i)^2}{g(i)}$$$
Lean4
/-- **Sedrakyan's lemma**, aka **Titu's lemma** or **Engel's form**.
This is a specialization of the Cauchy-Schwarz inequality with the sequences `f n / √(g n)` and
`√(g n)`, though here it is proven without relying on square roots. -/
theorem sq_sum_div_le_sum_sq_div [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι)
(f : ι → R) {g : ι → R} (hg : ∀ i ∈ s, 0 < g i) : (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i :=
by
have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)
refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H) (sum_sq_le_sum_mul_sum_of_sq_eq_mul _ H hg' fun i hi ↦ ?_)
rw [div_mul_cancel₀]
exact (hg i hi).ne'
