This repository has been archived by the owner on Oct 10, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 61
/
06_sub_sequences.lean
124 lines (95 loc) · 3.08 KB
/
06_sub_sequences.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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
import tuto_lib
/-
This file continues the elementary study of limits of sequences.
It can be skipped if the previous file was too easy, it won't introduce
any new tactic or trick.
Remember useful lemmas:
abs_le (x y : ℝ) : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y
abs_add (x y : ℝ) : |x + y| ≤ |x| + |y|
abs_sub (x y : ℝ) : |x - y| = |y - x|
ge_max_iff (p q r) : r ≥ max p q ↔ r ≥ p ∧ r ≥ q
le_max_left p q : p ≤ max p q
le_max_right p q : q ≤ max p q
and the definition:
def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
You can also use a property proved in the previous file:
unique_limit : seq_limit u l → seq_limit u l' → l = l'
def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m
-/
variable { φ : ℕ → ℕ}
/-
The next lemma is proved by an easy induction, but we haven't seen induction
in this tutorial. If you did the natural number game then you can delete
the proof below and try to reconstruct it.
-/
/-- An extraction is greater than id -/
lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n :=
begin
intros hyp n,
induction n with n hn,
{ exact nat.zero_le _ },
{ exact nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)]) },
end
/-- Extractions take arbitrarily large values for arbitrarily large
inputs. -/
-- 0039
lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
sorry
end
/-- A real number `a` is a cluster point of a sequence `u`
if `u` has a subsequence converging to `a`.
def cluster_point (u : ℕ → ℝ) (a : ℝ) :=
∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a
-/
variables {u : ℕ → ℝ} {a l : ℝ}
/-
In the exercise, we use `∃ n ≥ N, ...` which is the abreviation of
`∃ n, n ≥ N ∧ ...`.
Lean can read this abreviation, but displays as the confusing :
`∃ (n : ℕ) (H : n ≥ N)`
One gets used to it.
-/
/-- If `a` is a cluster point of `u` then there are values of
`u` arbitrarily close to `a` for arbitrarily large input. -/
-- 0040
lemma near_cluster :
cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
sorry
end
/-
The above exercice can be done in five lines.
Hint: you can use the anonymous constructor syntax when proving
existential statements.
-/
/-- If `u` tends to `l` then its subsequences tend to `l`. -/
-- 0041
lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) :
seq_limit (u ∘ φ) l :=
begin
sorry
end
/-- If `u` tends to `l` all its cluster points are equal to `l`. -/
-- 0042
lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l :=
begin
sorry
end
/-- cauchy_sequence sequence -/
def cauchy_sequence (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε
-- 0043
example : (∃ l, seq_limit u l) → cauchy_sequence u :=
begin
sorry
end
/-
In the next exercise, you can reuse
near_cluster : cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε
-/
-- 0044
example (hu : cauchy_sequence u) (hl : cluster_point u l) : seq_limit u l :=
begin
sorry
end