cau_seq and tendsto

Stream: general

[Henry Swanson]

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?

link to the relevant code

[Heather Macbeth]

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]

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,
    rw [nat.desc_fac_eq_div, nat.add_sub_cancel' h_le],
    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 _,
  rw tendsto_add_at_top_iff_nat 1,
  apply real.tendsto_exp_series,

end

[Patrick Massot]

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

[Eric Rodriguez]

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]

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