## Stream: general

### Topic: cau_seq and tendsto

#### Henry Swanson (Jun 12 2021 at 02:36):

I've got a function from N -> R, which is defined as f(N) = \sum_{k = 0}^N (-1)^k / k!, and I want to show that f(N) -> exp(-1) as N \to \infty.

It seems like this should be straightforward, but I'm having significant trouble with it. Specifically, the limit is defined as a tendsto/filter kind of thing, but the exponential is defined as a Cauchy sequence. I tried to find a lemma that says "the tendsto-limit of a cau_seq is just cau_seq.lim", but I can't seem to find it.

Is there something I've overlooked here?

#### Heather Macbeth (Jun 12 2021 at 02:46):

You almost always want to avoid working with cau_seq; there should be some API for the exponential function that lets you avoid it. What's the goal state before you start unfolding?

#### Patrick Massot (Jun 12 2021 at 10:01):

Henry Swanson said:

I tried to find a lemma that says "the tendsto-limit of a cau_seq is just cau_seq.lim", but I can't seem to find it.

This lemma is docs#cau_seq.tendsto_limit. This whole cau_seq shouldn't exist at all. It's a historical accident, we're sorry about that. After escaping cau_seq hell you'll run into coercion hell. You can do something like:

open finset

lemma complex.re_sum (u : ℕ → ℂ) (n : ℕ) : (∑ k in range n, u k).re = ∑ k in range n, (u k).re :=
complex.re_lm.map_sum

open_locale topological_space

lemma complex.tendsto_exp_series (z : ℂ) : tendsto (λ n, ∑ k in range n, z ^ k / k.factorial) at_top (𝓝 $z.exp) := begin convert z.exp'.tendsto_limit, unfold complex.exp end lemma real.tendsto_exp_series (x : ℝ) : tendsto (λ n, ∑ k in range n, x ^ k / k.factorial) at_top (𝓝$ x.exp) :=
begin
have : (λ (n : ℕ), ∑ (k : ℕ) in range n, x ^ k / k.factorial) =
(λ (n : ℕ), (∑ (k : ℕ) in range n, (x ^ k : ℂ) / k.factorial).re),
{ ext n,
rw complex.re_sum,
congr' 1,
ext k,
rw [show (x : ℂ) ^ k / (k.factorial : ℂ) = ((x ^ k / k.factorial : ℝ) : ℂ), by simp,
complex.of_real_re] },
rw this,
exact (complex.continuous_re.tendsto _).comp (complex.tendsto_exp_series x)
end

theorem num_derangements_tendsto_e :
tendsto (λ n, (num_derangements n : ℝ) / n.factorial) at_top
(𝓝 (real.exp (-1))) :=
begin
have : ∀ n : ℕ, (num_derangements n : ℝ) / n.factorial =
∑ k in finset.range (n + 1), (-1 : ℝ)^k / k.factorial,
{ intro n,
rw num_derangements_sum,
push_cast,
rw finset.sum_div,
refine finset.sum_congr (refl _) _,
intros k hk,
have h_le : k ≤ n := finset.mem_range_succ_iff.mp hk,
push_cast [nat.factorial_dvd_factorial h_le],
field_simp [nat.factorial_ne_zero],
ring,
},
simp_rw this,
set s : ℕ → ℝ := λ (n : ℕ), ∑ (k : ℕ) in range n, (-1) ^ k / k.factorial,
change tendsto (λ n, s (n+1)) at_top _,
apply real.tendsto_exp_series,

end


#### Patrick Massot (Jun 12 2021 at 10:01):

Clearly this shouldn't be in the data folder since it contains actual math.

#### Eric Rodriguez (Jun 12 2021 at 10:38):

Yeah, I'd move it to a separate file as well Henry, as it's quite heavy with the extra imports:

import topology.metric_space.cau_seq_filter
import data.complex.module
import analysis.complex.basic


#### Anatole Dedecker (Jun 12 2021 at 19:26):

I had a plan to redefine exp in a more general setting this summer, I'll get back to it hopefully.

Last updated: Aug 03 2023 at 10:10 UTC