1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143

import data.real.basic

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε

theorem converges_to_const (a : ℝ) : converges_to (λ x : ℕ, a) a :=
begin
  intros ε εpos,
  use 0,
  intros n nge, dsimp,
  rw [sub_self, abs_zero],
  apply εpos
end

theorem converges_to_add {s t : ℕ → ℝ} {a b : ℝ}
  (cs : converges_to s a) (ct : converges_to t b):
converges_to (λ n, s n + t n) (a + b) :=
begin
  intros ε εpos, dsimp,
  have ε2pos : 0 < ε / 2,
  { linarith },
  cases cs (ε / 2) ε2pos with Ns hs,
  cases ct (ε / 2) ε2pos with Nt ht,
  use max Ns Nt,
  intros n hn,
  have ngeNs : n ≥ Ns := le_of_max_le_left hn,
  have ngeNt : n ≥ Nt := le_of_max_le_right hn,
  calc
    |s n + t n - (a + b)| = | s n - a + (t n - b) | :
      by { congr, ring }
    ... ≤  | s n - a | + | (t n - b) | :
      abs_add _ _
    ... < ε / 2 + ε / 2 : add_lt_add (hs n ngeNs) (ht n ngeNt)
    ... = ε : by norm_num
end

theorem converges_to_mul_const {s : ℕ → ℝ} {a : ℝ}
    (c : ℝ) (cs : converges_to s a) :
  converges_to (λ n, c * s n) (c * a) :=
begin
  by_cases h : c = 0,
  { convert converges_to_const 0,
    { ext, rw [h, zero_mul] },
    rw [h, zero_mul] },
  have acpos : 0 < abs c,
    from abs_pos.mpr h,
  intros ε εpos, dsimp,
  have εcpos : 0 < ε / abs c,
  { apply div_pos εpos acpos },
  cases cs (ε / abs c) εcpos with Ns hs,
  use Ns,
  intros n ngt,
  calc
    |c * s n - c * a| = |c| * |s n - a| :
      by { rw [←abs_mul, mul_sub] }
    ... < |c| * (ε / |c|) :
      mul_lt_mul_of_pos_left (hs n ngt) acpos
    ... = ε : mul_div_cancel' _ (ne_of_lt acpos).symm
end

theorem exists_abs_le_of_converges_to {s : ℕ → ℝ} {a : ℝ}
    (cs : converges_to s a) :
  ∃ N b, ∀ n, N ≤ n → abs (s n) < b :=
begin
  cases cs 1 zero_lt_one with N h,
  use [N, abs a + 1],
  intros n ngt,
  calc
    |s n| = |s n - a + a| : by { congr, abel }
    ... ≤ |s n - a| + |a| : abs_add _ _
    ... < |a| + 1 : by linarith [h n ngt]
end

lemma aux {s t : ℕ → ℝ} {a : ℝ}
    (cs : converges_to s a) (ct : converges_to t 0) :
  converges_to (λ n, s n * t n) 0 :=
begin
  intros ε εpos, dsimp,
  rcases exists_abs_le_of_converges_to cs with ⟨N₀, B, h₀⟩,
  have Bpos : 0 < B,
    from lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _)),
  have pos₀ : ε / B > 0,
    from div_pos εpos Bpos,
  cases ct _ pos₀ with N₁ h₁,
  use max N₀ N₁,
  intros n ngt,
  have ngeN₀ : n ≥ N₀ := le_of_max_le_left ngt,
  have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt,
  calc
    |s n * t n - 0| = |s n| * |t n - 0| :
      by rw [sub_zero, abs_mul, sub_zero]
    ... < B * (ε / B) :
      mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _)
    ... = ε : mul_div_cancel' _ (ne_of_lt Bpos).symm
end

theorem converges_to_muL {s t : ℕ → ℝ} {a b : ℝ}
    (cs : converges_to s a) (ct : converges_to t b):
  converges_to (λ n, s n * t n) (a * b) :=
begin
  have h₁ : converges_to (λ n, s n * (t n - b)) 0,
  { apply aux cs,
    convert converges_to_add ct (converges_to_const (-b)),
    ring },
  convert (converges_to_add h₁ (converges_to_mul_const b cs)),
  { ext, ring },
  ring
end

theorem converges_to_unique {s : ℕ → ℝ} {a b : ℝ}
    (sa : converges_to s a) (sb : converges_to s b) :
  a = b :=
begin
  by_contradiction abne,
  have : abs (a - b) > 0,
  { apply lt_of_le_of_ne,
    { apply abs_nonneg },
      intro h'',
      apply abne,
      apply eq_of_abs_sub_eq_zero h''.symm, },
  let ε := abs (a - b) / 2,
  have εpos : ε > 0,
  { change abs (a - b) / 2 > 0, linarith },
  cases sa ε εpos with Na hNa,
  cases sb ε εpos with Nb hNb,
  let N := max Na Nb,
  have absa : abs (s N - a) < ε,
  { apply hNa, apply le_max_left },
  have absb : abs (s N - b) < ε,
  { apply hNb, apply le_max_right },
  have : abs (a - b) < abs (a - b),
    calc
      abs (a - b) = abs (- (s N - a) + (s N - b)) :
        by { congr, ring }
      ... ≤ abs (- (s N - a)) + abs (s N - b) :
        abs_add _ _
      ... = abs (s N - a) + abs (s N - b) :
        by rw [abs_neg]
      ... < ε + ε : add_lt_add absa absb
      ... = abs (a - b) : by norm_num,
  exact lt_irrefl _ this
end