-
Notifications
You must be signed in to change notification settings - Fork 297
/
exponential.lean
69 lines (62 loc) · 2.21 KB
/
exponential.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
/-
Copyright (c) 2021 Henry Swanson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henry Swanson, Patrick Massot
-/
import analysis.complex.basic
import data.complex.exponential
import data.equiv.derangements.finite
import topology.metric_space.cau_seq_filter
open filter
open finset
open_locale big_operators
open_locale topological_space
-- TODO move this out of "data" to somewhere else
-- TODO i suspect this already exists somewhere, or something similar
lemma complex.tendsto_iff_real (u : ℕ → ℝ) (x : ℝ) :
tendsto (λ n, u n) at_top (𝓝 x) ↔
tendsto (λ n, (u n : ℂ)) at_top (𝓝 (x : ℂ)) :=
begin
split,
{ exact λ h, (complex.continuous_of_real.tendsto x).comp h },
{ exact λ h, (complex.continuous_re.tendsto x).comp h },
end
-- TODO what's the appropriate place for these lemmas?
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
rw complex.tendsto_iff_real,
convert complex.tendsto_exp_series x; simp,
end
theorem num_derangements_tendsto_e :
tendsto (λ n, (num_derangements n : ℝ) / n.factorial) at_top
(𝓝 (real.exp (-1))) :=
begin
-- useful shorthand function
let s : ℕ → ℝ := λ n, ∑ k in finset.range n, (-1 : ℝ)^k / k.factorial,
-- this isn't entirely obvious, since we have to ensure that desc_fac and factorial interact in
-- the right way, e.g. that k stays less than n
have : ∀ n : ℕ, (num_derangements n : ℝ) / n.factorial = s(n+1),
{ 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,
-- now we shift the function by 1, and use the power series lemma
rw tendsto_add_at_top_iff_nat 1,
exact real.tendsto_exp_series (-1),
end