English
For every real x, the series ∑_{n=0}^{∞} x^n / n! converges (the exponential series). In particular, e^x is well-defined for all real x.
Русский
Для каждого действительного x ряд ∑_{n=0}^{∞} x^n / n! сходится (экспоненциальный ряд). В частности, e^x определим для всех x.
LaTeX
$$$\forall x \in \mathbb{R}, \; \sum_{n=0}^{\infty} \frac{x^n}{n!} < \infty$$$
Lean4
/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `expSeries_div_summable`
for a version that also works in `ℂ`, and `NormedSpace.expSeries_summable'` for a version
that works in any normed algebra over `ℝ` or `ℂ`. -/
theorem summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n / n ! : ℕ → ℝ) := by
-- We start with trivial estimates
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 :=
(div_lt_one A).2
(Nat.lt_floor_add_one _)
-- Then we apply the ratio test. The estimate works for `n ≥ ⌊‖x‖⌋₊`.
suffices ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (n + 1)!‖ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖ from
summable_of_ratio_norm_eventually_le B
(eventually_atTop.2 ⟨⌊‖x‖⌋₊, this⟩)
-- Finally, we prove the upper estimate
intro n hn
calc
‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul, norm_div,
Real.norm_natCast, Nat.cast_succ]
_ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr
