English
For k ≤ n in N, the sum over i in Ioc(k,n) of 1/i^2 is bounded above by 1/k − 1/n; more precisely the partial sums satisfy an inequality of this form in any ordered field.
Русский
Для натуральных k ≤ n сумма по i из Ioc(k,n) единиц в квадрате обратно пропорциональна i^2 ограничена сверху выражением 1/k − 1/n; т. е. неравенство справедливо в любой упорядоченной полевой структуре.
LaTeX
$$$$\displaystyle \sum_{i=k}^{n-1} \frac{1}{i^{2}} \le \frac{1}{k} - \frac{1}{n}.$$$$
Lean4
theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) :
(∑ i ∈ Ioc k n, ((i : α) ^ 2)⁻¹) ≤ (k : α)⁻¹ - (n : α)⁻¹ :=
by
refine Nat.le_induction ?_ ?_ n h
· simp only [Ioc_self, sum_empty, sub_self, le_refl]
intro n hn IH
rw [sum_Ioc_succ_top hn]
grw [IH]
push_cast
have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
field_simp
linarith
