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)
:
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 ∉ Set.range e, 0 ≤ 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 ∉ Set.range e, 0 ≤ 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 ∉ s, 0 ≤ 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 ι) => 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 ≠ i → 0 ≤ f j)
:
f i ≤ a
theorem
sum_le_tsum
{ι : Type u_1}
{α : Type u_3}
[OrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 0 ≤ 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 ≠ i → 0 ≤ 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)
:
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}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasSum f a)
(i : ι)
:
f i ≤ a
theorem
le_tsum'
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
(i : ι)
:
f i ≤ ∑' (i : ι), f i
theorem
hasSum_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
:
theorem
tsum_eq_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
theorem
tsum_ne_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
theorem
isLUB_hasSum'
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasSum f a)
:
IsLUB (Set.range fun (s : Finset ι) => 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 ι) => Finset.sum s fun (i : ι) => f i) i)
:
HasSum f i
theorem
hasSum_of_isLUB
{ι : Type u_1}
{α : Type u_3}
[CanonicallyLinearOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderTopology α]
{f : ι → α}
(b : α)
(hf : IsLUB (Set.range fun (s : Finset ι) => 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 : ι → α}
:
theorem
Summable.of_abs
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommGroup α]
[UniformSpace α]
[UniformAddGroup α]
[CompleteSpace α]
{f : ι → α}
:
Alias of the forward direction of summable_abs_iff.
theorem
Summable.abs
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommGroup α]
[UniformSpace α]
[UniformAddGroup α]
[CompleteSpace α]
{f : ι → α}
:
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)
:
Finite ι
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