@@ -5,13 +5,71 @@ Authors: Johannes Hölzl
55
66A collection of limit properties.
77-/
8- import algebra.big_operators algebra.group_power topology.real topology.of_nat topology.infinite_sum
8+ import algebra.big_operators algebra.group_power
9+ analysis.metric_space analysis.of_nat analysis.topology.infinite_sum
910noncomputable theory
1011open classical set finset function filter
1112local attribute [instance] decidable_inhabited prop_decidable
1213
1314infix ` ^ ` := pow_nat
1415
16+ section real
17+
18+ lemma has_sum_of_absolute_convergence {f : ℕ → ℝ}
19+ (hf : ∃r, tendsto (λn, (upto n).sum (λi, abs (f i))) at_top (nhds r)) : has_sum f :=
20+ let f' := λs:finset ℕ, s.sum (λi, abs (f i)) in
21+ suffices cauchy (map (λs:finset ℕ, s.sum f) at_top),
22+ from complete_space.complete this ,
23+ cauchy_iff.mpr $ and.intro (map_ne_bot at_top_ne_bot) $
24+ assume s hs,
25+ let ⟨ε, hε, hsε⟩ := mem_uniformity_dist.mp hs, ⟨r, hr⟩ := hf in
26+ have hε' : {p : ℝ × ℝ | dist p.1 p.2 < ε / 2 } ∈ (@uniformity ℝ _).sets,
27+ from mem_uniformity_dist.mpr ⟨ε / 2 , div_pos_of_pos_of_pos hε two_pos, assume a b h, h⟩,
28+ have cauchy (at_top.map $ λn, f' (upto n)),
29+ from cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hr,
30+ have ∃n, ∀{n'}, n ≤ n' → dist (f' (upto n)) (f' (upto n')) < ε / 2 ,
31+ by simp [cauchy_iff, mem_at_top_iff] at this ;
32+ from let ⟨t, ht, u, hu⟩ := this _ hε' in
33+ ⟨u, assume n' hn, ht $ prod_mk_mem_set_prod_eq.mpr ⟨hu _ (le_refl _), hu _ hn⟩⟩,
34+ let ⟨n, hn⟩ := this in
35+ have ∀{s}, upto n ⊆ s → abs ((s \ upto n).sum f) < ε / 2 ,
36+ from assume s hs,
37+ let ⟨n', hn'⟩ := @exists_nat_subset_upto s in
38+ have upto n ⊆ upto n', from subset.trans hs hn',
39+ have f'_nn : 0 ≤ f' (upto n' \ upto n), from zero_le_sum $ assume _ _, abs_nonneg _,
40+ calc abs ((s \ upto n).sum f) ≤ f' (s \ upto n) : abs_sum_le_sum_abs
41+ ... ≤ f' (upto n' \ upto n) : sum_le_sum_of_subset_of_nonneg
42+ (finset.sdiff_subset_sdiff hn' (finset.subset.refl _))
43+ (assume _ _ _, abs_nonneg _)
44+ ... = abs (f' (upto n' \ upto n)) : (abs_of_nonneg f'_nn).symm
45+ ... = abs (f' (upto n') - f' (upto n)) :
46+ by simp [f', (sum_sdiff ‹upto n ⊆ upto n'›).symm]
47+ ... = abs (f' (upto n) - f' (upto n')) : abs_sub _ _
48+ ... < ε / 2 : hn $ upto_subset_upto_iff.mp this ,
49+ have ∀{s t}, upto n ⊆ s → upto n ⊆ t → dist (s.sum f) (t.sum f) < ε,
50+ from assume s t hs ht,
51+ calc abs (s.sum f - t.sum f) = abs ((s \ upto n).sum f + - (t \ upto n).sum f) :
52+ by rw [←sum_sdiff hs, ←sum_sdiff ht]; simp
53+ ... ≤ abs ((s \ upto n).sum f) + abs ((t \ upto n).sum f) :
54+ le_trans (abs_add_le_abs_add_abs _ _) $ by rw [abs_neg]; exact le_refl _
55+ ... < ε / 2 + ε / 2 : add_lt_add (this hs) (this ht)
56+ ... = ε : by rw [←add_div, add_self_div_two],
57+ ⟨(λs:finset ℕ, s.sum f) '' {s | upto n ⊆ s}, image_mem_map $ mem_at_top (upto n),
58+ assume ⟨a, b⟩ ⟨⟨t, ht, ha⟩, ⟨s, hs, hb⟩⟩, by simp at ha hb; exact ha ▸ hb ▸ hsε _ _ (this ht hs)⟩
59+
60+ lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} {r : ℝ} (hf : ∀n, 0 ≤ f n) :
61+ is_sum f r ↔ tendsto (λn, (upto n).sum f) at_top (nhds r) :=
62+ ⟨tendsto_sum_nat_of_is_sum,
63+ assume hr,
64+ have tendsto (λn, (upto n).sum (λn, abs (f n))) at_top (nhds r),
65+ by simp [(λi, abs_of_nonneg (hf i)), hr],
66+ let ⟨p, h⟩ := has_sum_of_absolute_convergence ⟨r, this ⟩ in
67+ have hp : tendsto (λn, (upto n).sum f) at_top (nhds p), from tendsto_sum_nat_of_is_sum h,
68+ have p = r, from tendsto_nhds_unique at_top_ne_bot hp hr,
69+ this ▸ h⟩
70+
71+ end real
72+
1573lemma mul_add_one_le_pow {r : ℝ} (hr : 0 ≤ r) : ∀{n}, (of_nat n) * r + 1 ≤ (r + 1 ) ^ n
1674| 0 := by simp; exact le_refl 1
1775| (n + 1 ) :=
0 commit comments