-
Notifications
You must be signed in to change notification settings - Fork 257
/
Order.lean
287 lines (226 loc) · 11.5 KB
/
Order.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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Algebra.Order.Archimedean
import Mathlib.Topology.Algebra.InfiniteSum.NatInt
import Mathlib.Topology.Algebra.Order.Field
import Mathlib.Topology.Order.MonotoneConvergence
#align_import topology.algebra.infinite_sum.order from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514"
/-!
# Infinite sum in an order
This file provides lemmas about the interaction of infinite sums and order operations.
-/
open Finset Filter Function BigOperators
open scoped Classical
variable {ι κ α : Type*}
section Preorder
variable [Preorder α] [AddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α]
{f : ℕ → α} {c : α}
theorem tsum_le_of_sum_range_le (hf : Summable f) (h : ∀ n, ∑ i in range n, f i ≤ c) :
∑' n, f n ≤ c :=
let ⟨_l, hl⟩ := hf
hl.tsum_eq.symm ▸ le_of_tendsto' hl.tendsto_sum_nat h
#align tsum_le_of_sum_range_le tsum_le_of_sum_range_le
end Preorder
section OrderedAddCommMonoid
variable [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α}
{a a₁ a₂ : α}
theorem hasSum_le (h : ∀ i, f i ≤ g i) (hf : HasSum f a₁) (hg : HasSum g a₂) : a₁ ≤ a₂ :=
le_of_tendsto_of_tendsto' hf hg fun _ ↦ sum_le_sum fun i _ ↦ h i
#align has_sum_le hasSum_le
@[mono]
theorem hasSum_mono (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f ≤ g) : a₁ ≤ a₂ :=
hasSum_le h hf hg
#align has_sum_mono hasSum_mono
theorem hasSum_le_of_sum_le (hf : HasSum f a) (h : ∀ s, ∑ i in s, f i ≤ a₂) : a ≤ a₂ :=
le_of_tendsto' hf h
#align has_sum_le_of_sum_le hasSum_le_of_sum_le
theorem le_hasSum_of_le_sum (hf : HasSum f a) (h : ∀ s, a₂ ≤ ∑ i in s, f i) : a₂ ≤ a :=
ge_of_tendsto' hf h
#align le_has_sum_of_le_sum le_hasSum_of_le_sum
theorem hasSum_le_inj {g : κ → α} (e : ι → κ) (he : Injective e)
(hs : ∀ c, c ∉ Set.range e → 0 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : HasSum f a₁)
(hg : HasSum g a₂) : a₁ ≤ a₂ := by
rw [← hasSum_extend_zero he] at hf
refine hasSum_le (fun c ↦ ?_) hf hg
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
· rw [he.extend_apply]
exact h _
· rw [extend_apply' _ _ _ h]
exact hs _ h
#align has_sum_le_inj hasSum_le_inj
theorem tsum_le_tsum_of_inj {g : κ → α} (e : ι → κ) (he : Injective e)
(hs : ∀ c, c ∉ Set.range e → 0 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : Summable f)
(hg : Summable g) : tsum f ≤ tsum g :=
hasSum_le_inj _ he hs h hf.hasSum hg.hasSum
#align tsum_le_tsum_of_inj tsum_le_tsum_of_inj
theorem sum_le_hasSum (s : Finset ι) (hs : ∀ i, i ∉ s → 0 ≤ f i) (hf : HasSum f a) :
∑ i in s, f i ≤ a :=
ge_of_tendsto hf (eventually_atTop.2
⟨s, fun _t hst ↦ sum_le_sum_of_subset_of_nonneg hst fun i _ hbs ↦ hs i hbs⟩)
#align sum_le_has_sum sum_le_hasSum
theorem isLUB_hasSum (h : ∀ i, 0 ≤ f i) (hf : HasSum f a) :
IsLUB (Set.range fun s ↦ ∑ i in s, f i) a :=
isLUB_of_tendsto_atTop (Finset.sum_mono_set_of_nonneg h) hf
#align is_lub_has_sum isLUB_hasSum
theorem le_hasSum (hf : HasSum f a) (i : ι) (hb : ∀ j, j ≠ i → 0 ≤ f j) : f i ≤ a :=
calc
f i = ∑ i in {i}, f i := by rw [sum_singleton]
_ ≤ a := sum_le_hasSum _ (by simpa) hf
#align le_has_sum le_hasSum
theorem sum_le_tsum {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 0 ≤ f i) (hf : Summable f) :
∑ i in s, f i ≤ ∑' i, f i :=
sum_le_hasSum s hs hf.hasSum
#align sum_le_tsum sum_le_tsum
theorem le_tsum (hf : Summable f) (i : ι) (hb : ∀ j, j ≠ i → 0 ≤ f j) : f i ≤ ∑' i, f i :=
le_hasSum hf.hasSum i hb
#align le_tsum le_tsum
theorem tsum_le_tsum (h : ∀ i, f i ≤ g i) (hf : Summable f) (hg : Summable g) :
∑' i, f i ≤ ∑' i, g i :=
hasSum_le h hf.hasSum hg.hasSum
#align tsum_le_tsum tsum_le_tsum
@[mono]
theorem tsum_mono (hf : Summable f) (hg : Summable g) (h : f ≤ g) : ∑' n, f n ≤ ∑' n, g n :=
tsum_le_tsum h hf hg
#align tsum_mono tsum_mono
theorem tsum_le_of_sum_le (hf : Summable f) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ :=
hasSum_le_of_sum_le hf.hasSum h
#align tsum_le_of_sum_le tsum_le_of_sum_le
theorem tsum_le_of_sum_le' (ha₂ : 0 ≤ a₂) (h : ∀ s, ∑ i in s, f i ≤ a₂) : ∑' i, f i ≤ a₂ := by
by_cases hf : Summable f
· exact tsum_le_of_sum_le hf h
· rw [tsum_eq_zero_of_not_summable hf]
exact ha₂
#align tsum_le_of_sum_le' tsum_le_of_sum_le'
theorem HasSum.nonneg (h : ∀ i, 0 ≤ g i) (ha : HasSum g a) : 0 ≤ a :=
hasSum_le h hasSum_zero ha
#align has_sum.nonneg HasSum.nonneg
theorem HasSum.nonpos (h : ∀ i, g i ≤ 0) (ha : HasSum g a) : a ≤ 0 :=
hasSum_le h ha hasSum_zero
#align has_sum.nonpos HasSum.nonpos
theorem tsum_nonneg (h : ∀ i, 0 ≤ g i) : 0 ≤ ∑' i, g i := by
by_cases hg : Summable g
· exact hg.hasSum.nonneg h
· rw [tsum_eq_zero_of_not_summable hg]
#align tsum_nonneg tsum_nonneg
theorem tsum_nonpos (h : ∀ i, f i ≤ 0) : ∑' i, f i ≤ 0 := by
by_cases hf : Summable f
· exact hf.hasSum.nonpos h
· rw [tsum_eq_zero_of_not_summable hf]
#align tsum_nonpos tsum_nonpos
-- Porting note: generalized from `OrderedAddCommGroup` to `OrderedAddCommMonoid`
theorem hasSum_zero_iff_of_nonneg (hf : ∀ i, 0 ≤ f i) : HasSum f 0 ↔ f = 0 := by
refine' ⟨fun hf' ↦ _, _⟩
· ext i
exact (hf i).antisymm' (le_hasSum hf' _ fun j _ ↦ hf j)
· rintro rfl
exact hasSum_zero
#align has_sum_zero_iff_of_nonneg hasSum_zero_iff_of_nonneg
end OrderedAddCommMonoid
section OrderedAddCommGroup
variable [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α]
[OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι}
theorem hasSum_lt (h : f ≤ g) (hi : f i < g i) (hf : HasSum f a₁) (hg : HasSum g a₂) : a₁ < a₂ := by
have : update f i 0 ≤ update g i 0 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
have : 0 - f i + a₁ ≤ 0 - g i + a₂ := hasSum_le this (hf.update i 0) (hg.update i 0)
simpa only [zero_sub, add_neg_cancel_left] using add_lt_add_of_lt_of_le hi this
#align has_sum_lt hasSum_lt
@[mono]
theorem hasSum_strict_mono (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) : a₁ < a₂ :=
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
hasSum_lt hle hi hf hg
#align has_sum_strict_mono hasSum_strict_mono
theorem tsum_lt_tsum (h : f ≤ g) (hi : f i < g i) (hf : Summable f) (hg : Summable g) :
∑' n, f n < ∑' n, g n :=
hasSum_lt h hi hf.hasSum hg.hasSum
#align tsum_lt_tsum tsum_lt_tsum
@[mono]
theorem tsum_strict_mono (hf : Summable f) (hg : Summable g) (h : f < g) :
∑' n, f n < ∑' n, g n :=
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
tsum_lt_tsum hle hi hf hg
#align tsum_strict_mono tsum_strict_mono
theorem tsum_pos (hsum : Summable g) (hg : ∀ i, 0 ≤ g i) (i : ι) (hi : 0 < g i) :
0 < ∑' i, g i := by
rw [← tsum_zero]
exact tsum_lt_tsum hg hi summable_zero hsum
#align tsum_pos tsum_pos
end OrderedAddCommGroup
section CanonicallyOrderedAddCommMonoid
variable [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α]
{f : ι → α} {a : α}
theorem le_hasSum' (hf : HasSum f a) (i : ι) : f i ≤ a :=
le_hasSum hf i fun _ _ ↦ zero_le _
#align le_has_sum' le_hasSum'
theorem le_tsum' (hf : Summable f) (i : ι) : f i ≤ ∑' i, f i :=
le_tsum hf i fun _ _ ↦ zero_le _
#align le_tsum' le_tsum'
theorem hasSum_zero_iff : HasSum f 0 ↔ ∀ x, f x = 0 :=
(hasSum_zero_iff_of_nonneg fun _ ↦ zero_le _).trans funext_iff
#align has_sum_zero_iff hasSum_zero_iff
theorem tsum_eq_zero_iff (hf : Summable f) : ∑' i, f i = 0 ↔ ∀ x, f x = 0 := by
rw [← hasSum_zero_iff, hf.hasSum_iff]
#align tsum_eq_zero_iff tsum_eq_zero_iff
theorem tsum_ne_zero_iff (hf : Summable f) : ∑' i, f i ≠ 0 ↔ ∃ x, f x ≠ 0 := by
rw [Ne.def, tsum_eq_zero_iff hf, not_forall]
#align tsum_ne_zero_iff tsum_ne_zero_iff
theorem isLUB_hasSum' (hf : HasSum f a) : IsLUB (Set.range fun s ↦ ∑ i in s, f i) a :=
isLUB_of_tendsto_atTop (Finset.sum_mono_set f) hf
#align is_lub_has_sum' isLUB_hasSum'
end CanonicallyOrderedAddCommMonoid
section LinearOrder
/-!
For infinite sums taking values in a linearly ordered monoid, the existence of a least upper
bound for the finite sums is a criterion for summability.
This criterion is useful when applied in a linearly ordered monoid which is also a complete or
conditionally complete linear order, such as `ℝ`, `ℝ≥0`, `ℝ≥0∞`, because it is then easy to check
the existence of a least upper bound.
-/
theorem hasSum_of_isLUB_of_nonneg [LinearOrderedAddCommMonoid α] [TopologicalSpace α]
[OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 0 ≤ f i)
(hf : IsLUB (Set.range fun s ↦ ∑ i in s, f i) i) : HasSum f i :=
tendsto_atTop_isLUB (Finset.sum_mono_set_of_nonneg h) hf
#align has_sum_of_is_lub_of_nonneg hasSum_of_isLUB_of_nonneg
theorem hasSum_of_isLUB [CanonicallyLinearOrderedAddCommMonoid α] [TopologicalSpace α]
[OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∑ i in s, f i) b) :
HasSum f b :=
tendsto_atTop_isLUB (Finset.sum_mono_set f) hf
#align has_sum_of_is_lub hasSum_of_isLUB
theorem summable_abs_iff [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α]
[CompleteSpace α] {f : ι → α} : (Summable fun x ↦ |f x|) ↔ Summable f :=
let s := { x | 0 ≤ f x }
have h1 : ∀ x : s, |f x| = f x := fun x ↦ abs_of_nonneg x.2
have h2 : ∀ x : ↑sᶜ, |f x| = -f x := fun x ↦ abs_of_neg (not_le.1 x.2)
calc (Summable fun x ↦ |f x|) ↔
(Summable fun x : s ↦ |f x|) ∧ Summable fun x : ↑sᶜ ↦ |f x| :=
summable_subtype_and_compl.symm
_ ↔ (Summable fun x : s ↦ f x) ∧ Summable fun x : ↑sᶜ ↦ -f x := by simp only [h1, h2]
_ ↔ Summable f := by simp only [summable_neg_iff, summable_subtype_and_compl]
#align summable_abs_iff summable_abs_iff
alias ⟨Summable.of_abs, Summable.abs⟩ := summable_abs_iff
#align summable.of_abs Summable.of_abs
#align summable.abs Summable.abs
theorem Finite.of_summable_const [LinearOrderedAddCommGroup α] [TopologicalSpace α] [Archimedean α]
[OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) :
Finite ι := by
have H : ∀ s : Finset ι, s.card • b ≤ ∑' _ : ι, b := fun s ↦ by
simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
have : ∀ s : Finset ι, s.card ≤ n := fun s ↦ by
simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn
have : Fintype ι := fintypeOfFinsetCardLe n this
infer_instance
theorem Set.Finite.of_summable_const [LinearOrderedAddCommGroup α] [TopologicalSpace α]
[Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun _ : ι ↦ b) :
(Set.univ : Set ι).Finite :=
finite_univ_iff.2 <| .of_summable_const hb hf
#align finite_of_summable_const Set.Finite.of_summable_const
end LinearOrder
theorem Summable.tendsto_atTop_of_pos [LinearOrderedField α] [TopologicalSpace α] [OrderTopology α]
{f : ℕ → α} (hf : Summable f⁻¹) (hf' : ∀ n, 0 < f n) : Tendsto f atTop atTop :=
inv_inv f ▸ Filter.Tendsto.inv_tendsto_zero <|
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf.tendsto_atTop_zero <|
eventually_of_forall fun _ ↦ inv_pos.2 (hf' _)
#align summable.tendsto_top_of_pos Summable.tendsto_atTop_of_pos