English
For suitable k ≤ n, the sum over i in Ioo(k,n) of 1/i^2 is bounded by 2/(k+1).
Русский
Для подходящих k ≤ n сумма по i из Ioo(k,n) 1/i^2 ограничена сверху 2/(k+1).
LaTeX
$$$$\displaystyle \sum_{i \in Ioo(k,n)} \frac{1}{i^{2}} \le \frac{2}{k+1}.$$$$
Lean4
theorem sum_Ioo_inv_sq_le (k n : ℕ) : (∑ i ∈ Ioo k n, (i ^ 2 : α)⁻¹) ≤ 2 / (k + 1) :=
calc
(∑ i ∈ Ioo k n, ((i : α) ^ 2)⁻¹) ≤ ∑ i ∈ Ioc k (max (k + 1) n), ((i : α) ^ 2)⁻¹ :=
by
apply sum_le_sum_of_subset_of_nonneg
· intro x hx
simp only [mem_Ioo] at hx
simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true, and_self_iff]
· intro i _hi _hident
positivity
_ ≤ ((k + 1 : α) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), ((i : α) ^ 2)⁻¹ :=
by
rw [← Icc_add_one_left_eq_Ioc, ← Ico_add_one_right_eq_Icc, sum_eq_sum_Ico_succ_bot]
swap; · exact Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))
rw [Ico_add_one_right_eq_Icc, Icc_add_one_left_eq_Ioc]
norm_cast
_ ≤ ((k + 1 : α) ^ 2)⁻¹ + (k + 1 : α)⁻¹ :=
by
refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)
· simp only [Ne, Nat.succ_ne_zero, not_false_iff]
· simp only [Nat.cast_succ, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]
_ ≤ 1 / (k + 1) + 1 / (k + 1) :=
by
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
simp_rw [← one_div]
gcongr
simpa using pow_right_mono₀ A one_le_two
_ = 2 / (k + 1) := by ring
