Infinite sum in an order #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides lemmas about the interaction of infinite sums and order operations.
theorem
tsum_le_of_sum_range_le
{α : Type u_3}
[preorder α]
[add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
[t2_space α]
{f : ℕ → α}
{c : α}
(hf : summable f)
(h : ∀ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i) ≤ c) :
theorem
has_sum_le
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f g : ι → α}
{a₁ a₂ : α}
(h : ∀ (i : ι), f i ≤ g i)
(hf : has_sum f a₁)
(hg : has_sum g a₂) :
a₁ ≤ a₂
theorem
has_sum_mono
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f g : ι → α}
{a₁ a₂ : α}
(hf : has_sum f a₁)
(hg : has_sum g a₂)
(h : f ≤ g) :
a₁ ≤ a₂
theorem
has_sum_le_of_sum_le
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a a₂ : α}
(hf : has_sum f a)
(h : ∀ (s : finset ι), s.sum (λ (i : ι), f i) ≤ a₂) :
a ≤ a₂
theorem
le_has_sum_of_le_sum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a a₂ : α}
(hf : has_sum f a)
(h : ∀ (s : finset ι), a₂ ≤ s.sum (λ (i : ι), f i)) :
a₂ ≤ a
theorem
has_sum_le_inj
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a₁ a₂ : α}
{g : κ → α}
(e : ι → κ)
(he : function.injective e)
(hs : ∀ (c : κ), c ∉ set.range e → 0 ≤ g c)
(h : ∀ (i : ι), f i ≤ g (e i))
(hf : has_sum f a₁)
(hg : has_sum g a₂) :
a₁ ≤ a₂
theorem
tsum_le_tsum_of_inj
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : function.injective e)
(hs : ∀ (c : κ), c ∉ set.range e → 0 ≤ g c)
(h : ∀ (i : ι), f i ≤ g (e i))
(hf : summable f)
(hg : summable g) :
theorem
sum_le_has_sum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a : α}
(s : finset ι)
(hs : ∀ (i : ι), i ∉ s → 0 ≤ f i)
(hf : has_sum f a) :
theorem
is_lub_has_sum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a : α}
(h : ∀ (i : ι), 0 ≤ f i)
(hf : has_sum f a) :
theorem
le_has_sum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a : α}
(hf : has_sum f a)
(i : ι)
(hb : ∀ (b' : ι), b' ≠ i → 0 ≤ f b') :
f i ≤ a
theorem
sum_le_tsum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
(s : finset ι)
(hs : ∀ (i : ι), i ∉ s → 0 ≤ f i)
(hf : summable f) :
theorem
tsum_le_tsum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f g : ι → α}
(h : ∀ (i : ι), f i ≤ g i)
(hf : summable f)
(hg : summable g) :
theorem
tsum_le_of_sum_le
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a₂ : α}
(hf : summable f)
(h : ∀ (s : finset ι), s.sum (λ (i : ι), f i) ≤ a₂) :
theorem
tsum_le_of_sum_le'
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a₂ : α}
(ha₂ : 0 ≤ a₂)
(h : ∀ (s : finset ι), s.sum (λ (i : ι), f i) ≤ a₂) :
theorem
has_sum.nonneg
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{g : ι → α}
{a : α}
(h : ∀ (i : ι), 0 ≤ g i)
(ha : has_sum g a) :
0 ≤ a
theorem
has_sum.nonpos
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{g : ι → α}
{a : α}
(h : ∀ (i : ι), g i ≤ 0)
(ha : has_sum g a) :
a ≤ 0
theorem
tsum_nonneg
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{g : ι → α}
(h : ∀ (i : ι), 0 ≤ g i) :
theorem
tsum_nonpos
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
(h : ∀ (i : ι), f i ≤ 0) :
theorem
has_sum_lt
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{f g : ι → α}
{a₁ a₂ : α}
{i : ι}
(h : f ≤ g)
(hi : f i < g i)
(hf : has_sum f a₁)
(hg : has_sum g a₂) :
a₁ < a₂
theorem
has_sum_strict_mono
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{f g : ι → α}
{a₁ a₂ : α}
(hf : has_sum f a₁)
(hg : has_sum g a₂)
(h : f < g) :
a₁ < a₂
theorem
tsum_lt_tsum
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{f g : ι → α}
{i : ι}
(h : f ≤ g)
(hi : f i < g i)
(hf : summable f)
(hg : summable g) :
theorem
tsum_strict_mono
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{f g : ι → α}
(hf : summable f)
(hg : summable g)
(h : f < g) :
theorem
tsum_pos
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{g : ι → α}
(hsum : summable g)
(hg : ∀ (i : ι), 0 ≤ g i)
(i : ι)
(hi : 0 < g i) :
theorem
has_sum_zero_iff_of_nonneg
{ι : Type u_1}
{α : Type u_3}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
[order_closed_topology α]
{f : ι → α}
(hf : ∀ (i : ι), 0 ≤ f i) :
theorem
le_has_sum'
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a : α}
(hf : has_sum f a)
(i : ι) :
f i ≤ a
theorem
le_tsum'
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
(hf : summable f)
(i : ι) :
theorem
has_sum_zero_iff
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α} :
theorem
tsum_eq_zero_iff
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
(hf : summable f) :
theorem
tsum_ne_zero_iff
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
(hf : summable f) :
theorem
is_lub_has_sum'
{ι : Type u_1}
{α : Type u_3}
[canonically_ordered_add_monoid α]
[topological_space α]
[order_closed_topology α]
{f : ι → α}
{a : α}
(hf : has_sum f 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
has_sum_of_is_lub_of_nonneg
{ι : Type u_1}
{α : Type u_3}
[linear_ordered_add_comm_monoid α]
[topological_space α]
[order_topology α]
{f : ι → α}
(i : α)
(h : ∀ (i : ι), 0 ≤ f i)
(hf : is_lub (set.range (λ (s : finset ι), s.sum (λ (i : ι), f i))) i) :
has_sum f i
theorem
has_sum_of_is_lub
{ι : Type u_1}
{α : Type u_3}
[canonically_linear_ordered_add_monoid α]
[topological_space α]
[order_topology α]
{f : ι → α}
(b : α)
(hf : is_lub (set.range (λ (s : finset ι), s.sum (λ (i : ι), f i))) b) :
has_sum f b
theorem
summable_abs_iff
{ι : Type u_1}
{α : Type u_3}
[linear_ordered_add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{f : ι → α} :
theorem
summable.abs
{ι : Type u_1}
{α : Type u_3}
[linear_ordered_add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{f : ι → α} :
Alias of the reverse direction of summable_abs_iff.
theorem
summable.of_abs
{ι : Type u_1}
{α : Type u_3}
[linear_ordered_add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{f : ι → α} :
Alias of the forward direction of summable_abs_iff.
theorem
finite_of_summable_const
{ι : Type u_1}
{α : Type u_3}
[linear_ordered_add_comm_group α]
[topological_space α]
[archimedean α]
[order_closed_topology α]
{b : α}
(hb : 0 < b)
(hf : summable (λ (i : ι), b)) :
theorem
summable.tendsto_top_of_pos
{α : Type u_3}
[linear_ordered_field α]
[topological_space α]
[order_topology α]
{f : ℕ → α}
(hf : summable f⁻¹)
(hf' : ∀ (n : ℕ), 0 < f n) :