Infinite sum or product in an order #
This file provides lemmas about the interaction of infinite sums and products and order operations.
abbrev
tsum_le_of_sum_range_le.match_1
{α : Type u_1}
[AddCommMonoid α]
[TopologicalSpace α]
{f : ℕ → α}
(motive : Summable f → Prop)
:
Equations
- ⋯ = ⋯
Instances For
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
tprod_le_of_prod_range_le
{α : Type u_3}
[Preorder α]
[CommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
[T2Space α]
{f : ℕ → α}
{c : α}
(hf : Multipliable f)
(h : ∀ (n : ℕ), (Finset.prod (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
hasProd_le
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
{a₁ : α}
{a₂ : α}
(h : ∀ (i : ι), f i ≤ g i)
(hf : HasProd f a₁)
(hg : HasProd 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
hasProd_mono
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
{a₁ : α}
{a₂ : α}
(hf : HasProd f a₁)
(hg : HasProd 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
hasProd_le_of_prod_le
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
{a₂ : α}
(hf : HasProd f a)
(h : ∀ (s : Finset ι), (Finset.prod 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
le_hasProd_of_le_prod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
{a₂ : α}
(hf : HasProd f a)
(h : ∀ (s : Finset ι), a₂ ≤ Finset.prod 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
hasProd_le_inj
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₁ : α}
{a₂ : α}
{g : κ → α}
(e : ι → κ)
(he : Function.Injective e)
(hs : ∀ c ∉ Set.range e, 1 ≤ g c)
(h : ∀ (i : ι), f i ≤ g (e i))
(hf : HasProd f a₁)
(hg : HasProd 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
tprod_le_tprod_of_inj
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : Function.Injective e)
(hs : ∀ c ∉ Set.range e, 1 ≤ g c)
(h : ∀ (i : ι), f i ≤ g (e i))
(hf : Multipliable f)
(hg : Multipliable 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
prod_le_hasProd
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(s : Finset ι)
(hs : ∀ i ∉ s, 1 ≤ f i)
(hf : HasProd f a)
:
(Finset.prod 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
isLUB_hasProd
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(h : ∀ (i : ι), 1 ≤ f i)
(hf : HasProd f a)
:
IsLUB (Set.range fun (s : Finset ι) => Finset.prod 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
le_hasProd
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasProd f a)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 1 ≤ 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
prod_le_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 1 ≤ f i)
(hf : Multipliable f)
:
(Finset.prod 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
le_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable f)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 1 ≤ 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
tprod_le_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
(h : ∀ (i : ι), f i ≤ g i)
(hf : Multipliable f)
(hg : Multipliable 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
tprod_mono
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
(hf : Multipliable f)
(hg : Multipliable 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
tprod_le_of_prod_le
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
(hf : Multipliable f)
(h : ∀ (s : Finset ι), (Finset.prod 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
tprod_le_of_prod_le'
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
(ha₂ : 1 ≤ a₂)
(h : ∀ (s : Finset ι), (Finset.prod 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
HasProd.one_le
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
(h : ∀ (i : ι), 1 ≤ g i)
(ha : HasProd g a)
:
1 ≤ 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
HasProd.le_one
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
(h : ∀ (i : ι), g i ≤ 1)
(ha : HasProd g a)
:
a ≤ 1
theorem
tsum_nonneg
{ι : Type u_1}
{α : Type u_3}
[OrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
(h : ∀ (i : ι), 0 ≤ g i)
:
0 ≤ ∑' (i : ι), g i
theorem
one_le_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
(h : ∀ (i : ι), 1 ≤ g i)
:
1 ≤ ∏' (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
tprod_le_one
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(h : ∀ (i : ι), f i ≤ 1)
:
∏' (i : ι), f i ≤ 1
theorem
hasSum_zero_iff_of_nonneg
{ι : Type u_1}
{α : Type u_3}
[OrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : ∀ (i : ι), 0 ≤ f i)
:
theorem
hasProd_one_iff_of_one_le
{ι : Type u_1}
{α : Type u_3}
[OrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : ∀ (i : ι), 1 ≤ 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
hasProd_lt
{ι : Type u_1}
{α : Type u_3}
[OrderedCommGroup α]
[TopologicalSpace α]
[TopologicalGroup α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
{a₁ : α}
{a₂ : α}
{i : ι}
(h : f ≤ g)
(hi : f i < g i)
(hf : HasProd f a₁)
(hg : HasProd 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
hasProd_strict_mono
{ι : Type u_1}
{α : Type u_3}
[OrderedCommGroup α]
[TopologicalSpace α]
[TopologicalGroup α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
{a₁ : α}
{a₂ : α}
(hf : HasProd f a₁)
(hg : HasProd 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
tprod_lt_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommGroup α]
[TopologicalSpace α]
[TopologicalGroup α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
{i : ι}
(h : f ≤ g)
(hi : f i < g i)
(hf : Multipliable f)
(hg : Multipliable 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
tprod_strict_mono
{ι : Type u_1}
{α : Type u_3}
[OrderedCommGroup α]
[TopologicalSpace α]
[TopologicalGroup α]
[OrderClosedTopology α]
{f : ι → α}
{g : ι → α}
(hf : Multipliable f)
(hg : Multipliable 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
one_lt_tprod
{ι : Type u_1}
{α : Type u_3}
[OrderedCommGroup α]
[TopologicalSpace α]
[TopologicalGroup α]
[OrderClosedTopology α]
{g : ι → α}
(hsum : Multipliable g)
(hg : ∀ (i : ι), 1 ≤ g i)
(i : ι)
(hi : 1 < g i)
:
1 < ∏' (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_hasProd'
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasProd 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
le_tprod'
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable f)
(i : ι)
:
f i ≤ ∏' (i : ι), f i
theorem
hasSum_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
:
theorem
hasProd_one_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
:
theorem
tsum_eq_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
theorem
tprod_eq_one_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable f)
:
theorem
tsum_ne_zero_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedAddCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
theorem
tprod_ne_one_iff
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable 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
theorem
isLUB_hasProd'
{ι : Type u_1}
{α : Type u_3}
[CanonicallyOrderedCommMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasProd f a)
:
IsLUB (Set.range fun (s : Finset ι) => Finset.prod 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
hasProd_of_isLUB_of_one_le
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedCommMonoid α]
[TopologicalSpace α]
[OrderTopology α]
{f : ι → α}
(i : α)
(h : ∀ (i : ι), 1 ≤ f i)
(hf : IsLUB (Set.range fun (s : Finset ι) => Finset.prod s fun (i : ι) => f i) i)
:
HasProd 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
hasProd_of_isLUB
{ι : Type u_1}
{α : Type u_3}
[CanonicallyLinearOrderedCommMonoid α]
[TopologicalSpace α]
[OrderTopology α]
{f : ι → α}
(b : α)
(hf : IsLUB (Set.range fun (s : Finset ι) => Finset.prod s fun (i : ι) => f i) b)
:
HasProd f b
theorem
summable_abs_iff
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommGroup α]
[UniformSpace α]
[UniformAddGroup α]
[CompleteSpace α]
{f : ι → α}
:
theorem
multipliable_mabs_iff
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedCommGroup α]
[UniformSpace α]
[UniformGroup α]
[CompleteSpace α]
{f : ι → α}
:
(Multipliable fun (x : ι) => mabs (f x)) ↔ Multipliable f
theorem
Summable.abs
{ι : Type u_1}
{α : Type u_3}
[LinearOrderedAddCommGroup α]
[UniformSpace α]
[UniformAddGroup α]
[CompleteSpace α]
{f : ι → α}
:
Alias of the reverse direction of summable_abs_iff.
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
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