Documentation

Mathlib.Topology.Algebra.InfiniteSum.Order

Infinite sum in an order #

This file provides lemmas about the interaction of infinite sums and order operations.

theorem tsum_le_of_sum_range_le {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α] {f : α} {c : α} (hf : Summable f) (h : ∀ (n : ), (Finset.sum (Finset.range n) fun i => f i) c) :
∑' (n : ), f n c
theorem hasSum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (h : ∀ (i : ι), f i g i) (hf : HasSum f a₁) (hg : HasSum g a₂) :
a₁ a₂
theorem hasSum_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f g) :
a₁ a₂
theorem hasSum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasSum f a) (h : ∀ (s : Finset ι), (Finset.sum s fun i => f i) a₂) :
a a₂
theorem le_hasSum_of_le_sum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasSum f a) (h : ∀ (s : Finset ι), a₂ Finset.sum s fun i => f i) :
a₂ a
theorem hasSum_le_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₁ : α} {a₂ : α} {g : κα} (e : ικ) (he : Function.Injective e) (hs : ∀ (c : κ), ¬c Set.range e0 g c) (h : ∀ (i : ι), f i g (e i)) (hf : HasSum f a₁) (hg : HasSum g a₂) :
a₁ a₂
theorem tsum_le_tsum_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : κα} (e : ικ) (he : Function.Injective e) (hs : ∀ (c : κ), ¬c Set.range e0 g c) (h : ∀ (i : ι), f i g (e i)) (hf : Summable f) (hg : Summable g) :
theorem sum_le_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (s : Finset ι) (hs : ∀ (i : ι), ¬i s0 f i) (hf : HasSum f a) :
(Finset.sum s fun i => f i) a
theorem isLUB_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (h : ∀ (i : ι), 0 f i) (hf : HasSum f a) :
IsLUB (Set.range fun s => Finset.sum s fun i => f i) a
theorem le_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) (i : ι) (hb : ∀ (j : ι), j i0 f j) :
f i a
theorem sum_le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (s : Finset ι) (hs : ∀ (i : ι), ¬i s0 f i) (hf : Summable f) :
(Finset.sum s fun i => f i) ∑' (i : ι), f i
theorem le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) (i : ι) (hb : ∀ (j : ι), j i0 f j) :
f i ∑' (i : ι), f i
theorem tsum_le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) (hf : Summable f) (hg : Summable g) :
∑' (i : ι), f i ∑' (i : ι), g i
theorem tsum_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Summable f) (hg : Summable g) (h : f g) :
∑' (n : ι), f n ∑' (n : ι), g n
theorem tsum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (hf : Summable f) (h : ∀ (s : Finset ι), (Finset.sum s fun i => f i) a₂) :
∑' (i : ι), f i a₂
theorem tsum_le_of_sum_le' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (ha₂ : 0 a₂) (h : ∀ (s : Finset ι), (Finset.sum s fun i => f i) a₂) :
∑' (i : ι), f i a₂
theorem HasSum.nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), 0 g i) (ha : HasSum g a) :
0 a
theorem HasSum.nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), g i 0) (ha : HasSum g a) :
a 0
theorem tsum_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} (h : ∀ (i : ι), 0 g i) :
0 ∑' (i : ι), g i
theorem tsum_nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (h : ∀ (i : ι), f i 0) :
∑' (i : ι), f i 0
theorem hasSum_zero_iff_of_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : ∀ (i : ι), 0 f i) :
HasSum f 0 f = 0
theorem hasSum_lt {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} {i : ι} (h : f g) (hi : f i < g i) (hf : HasSum f a₁) (hg : HasSum g a₂) :
a₁ < a₂
theorem hasSum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) :
a₁ < a₂
theorem tsum_lt_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {i : ι} (h : f g) (hi : f i < g i) (hf : Summable f) (hg : Summable g) :
∑' (n : ι), f n < ∑' (n : ι), g n
theorem tsum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Summable f) (hg : Summable g) (h : f < g) :
∑' (n : ι), f n < ∑' (n : ι), g n
theorem tsum_pos {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {g : ια} (hsum : Summable g) (hg : ∀ (i : ι), 0 g i) (i : ι) (hi : 0 < g i) :
0 < ∑' (i : ι), g i
theorem le_hasSum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) (i : ι) :
f i a
theorem le_tsum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) (i : ι) :
f i ∑' (i : ι), f i
theorem hasSum_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} :
HasSum f 0 ∀ (x : ι), f x = 0
theorem tsum_eq_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) :
∑' (i : ι), f i = 0 ∀ (x : ι), f x = 0
theorem tsum_ne_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) :
∑' (i : ι), f i 0 x, f x 0
theorem isLUB_hasSum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) :
IsLUB (Set.range fun s => Finset.sum s fun i => f i) a

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 {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (i : α) (h : ∀ (i : ι), 0 f i) (hf : IsLUB (Set.range fun s => Finset.sum s fun i => f i) i) :
HasSum f i
theorem hasSum_of_isLUB {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedAddMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (b : α) (hf : IsLUB (Set.range fun s => Finset.sum s fun i => f i) b) :
HasSum f b
theorem summable_abs_iff {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
(Summable fun x => |f x|) Summable f
theorem Summable.of_abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
(Summable fun x => |f x|) → Summable f

Alias of the forward direction of summable_abs_iff.

theorem Summable.abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
Summable fSummable fun x => |f x|

Alias of the reverse direction of summable_abs_iff.

theorem Finite.of_summable_const {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun x => b) :
theorem Set.Finite.of_summable_const {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun x => b) :
Set.Finite Set.univ
theorem Summable.tendsto_atTop_of_pos {α : Type u_3} [LinearOrderedField α] [TopologicalSpace α] [OrderTopology α] {f : α} (hf : Summable f⁻¹) (hf' : ∀ (n : ), 0 < f n) :
Filter.Tendsto f Filter.atTop Filter.atTop