English
If n > 0 and s > 1, then term n s equals the specified decomposition.
Русский
Если n>0 и s>1, то term n s равно заданному разложению.
LaTeX
$$$$\\\\operatorname{term}(n,s) = \\frac{1}{s-1}\\left(\\frac{1}{n^{s-1}} - \\frac{1}{(n+1)^{s-1}}\\right) - \\frac{n}{s}\\left(\\frac{1}{n^{s}} - \\frac{1}{(n+1)^{s}}\\right)$$$$
Lean4
theorem term_of_lt {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : 1 < s) :
term n s = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1)) - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) :=
by
have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
intro x hx
rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
exact (Nat.cast_pos.mpr hn).trans_le hx.1
calc
term n s
_ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
_ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) :=
by
refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne', rpow_neg (hv x hx).le,
rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm, div_eq_mul_inv]
_ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;> [skip;
apply IntervalIntegrable.const_mul] <;>
· refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
· exact_mod_cast hn
· linarith
_ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1)) - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) :=
by
have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
congr 1
·
rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
·
rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div, mul_div_assoc,
rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
