English
For a field with a linear order and strict ordered ring structure, and natural numbers n ≤ m < j, the sum of 1/m! over m from n to j−1 is bounded by n.succ/(n! n).
Русский
Для поля с линейным порядком и структурой строгого упорядоченного кольца, при натуральных числах n ≤ m < j сумма 1/m! по m от n до j−1 не превышает n+1/(n! n).
LaTeX
$$$\displaystyle \sum_{m=n}^{j-1} \frac{1}{m!} \le \frac{n+1}{n!\, n}$$$
Lean4
theorem sum_div_factorial_le {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (n j : ℕ) (hn : 0 < n) :
(∑ m ∈ range j with n ≤ m, (1 / m.factorial : α)) ≤ n.succ / (n.factorial * n) :=
calc
(∑ m ∈ range j with n ≤ m, (1 / m.factorial : α)) = ∑ m ∈ range (j - n), (1 / ((m + n).factorial : α)) := by
refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_ <;> simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]
_ ≤ ∑ m ∈ range (j - n), ((n.factorial : α) * (n.succ : α) ^ m)⁻¹ :=
by
simp_rw [one_div]
gcongr
rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
exact Nat.factorial_mul_pow_le_factorial
_ = (n.factorial : α)⁻¹ * ∑ m ∈ range (j - n), (n.succ : α)⁻¹ ^ m := by simp [← mul_sum, mul_comm, inv_pow]
_ = ((n.succ : α) - n.succ * (n.succ : α)⁻¹ ^ (j - n)) / (n.factorial * n) :=
by
have h₁ : (n.succ : α) ≠ 1 := @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))
have h₂ : (n.succ : α) ≠ 0 := by positivity
have h₃ : (n.factorial * n : α) ≠ 0 := by positivity
have h₄ : (n.succ - 1 : α) = n := by simp
rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α), ← mul_assoc (n.factorial⁻¹ : α), ←
mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α), mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul,
mul_comm]
_ ≤ n.succ / (n.factorial * n : α) := by gcongr; apply sub_le_self; positivity
