Documentation

Mathlib.Topology.Algebra.InfiniteSum.Order

Infinite sum or product in an order #

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

source
theorem hasProd_le_of_prod_le {ι : Type u_1} {α : Type u_3} [Preorder α] [CommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] (hf : HasProd f a) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ c) :
a ≤ c
source
theorem hasSum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] (hf : HasSum f a) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ c) :
a ≤ c
source
theorem le_hasProd_of_le_prod {ι : Type u_1} {α : Type u_3} [Preorder α] [CommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] (hf : HasProd f a) (h : ∀ (s : Finset ι), c ≤ ∏ i ∈ s, f i) :
c ≤ a
source
theorem le_hasSum_of_le_sum {ι : Type u_1} {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] (hf : HasSum f a) (h : ∀ (s : Finset ι), c ≤ ∑ i ∈ s, f i) :
c ≤ a
source
theorem tprod_le_of_prod_range_le {α : Type u_3} [Preorder α] [CommMonoid α] [TopologicalSpace α] {c : α} [ClosedIicTopology α] {f : ℕ → α} (hf : Multipliable f) (h : ∀ (n : ℕ), ∏ i ∈ Finset.range n, f i ≤ c) :
∏' (n : ℕ), f n ≤ c
source
theorem tsum_le_of_sum_range_le {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {c : α} [ClosedIicTopology α] {f : ℕ → α} (hf : Summable f) (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) :
∑' (n : ℕ), f n ≤ c
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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₂
source
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) :
tprod f ≤ tprod g
source
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) :
tsum f ≤ tsum g
source
theorem tprod_subtype_le {κ : Type u_4} {γ : Type u_5} [OrderedCommGroup γ] [UniformSpace γ] [UniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 1 ≤ f a) (hf : Multipliable f) :
∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a
source
theorem tsum_subtype_le {κ : Type u_4} {γ : Type u_5} [OrderedAddCommGroup γ] [UniformSpace γ] [UniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 0 ≤ f a) (hf : Summable f) :
∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a
source
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) :
∏ i ∈ s, f i ≤ a
source
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) :
∑ i ∈ s, f i ≤ a
source
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 ι) => ∏ i ∈ s, f i) a
source
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 ι) => ∑ i ∈ s, f i) a
source
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
source
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
source
theorem lt_hasProd {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [MulRightStrictMono α] (hf : HasProd f a) (i : ι) (hi : ∀ (j : ι), j ≠ i → 1 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 1 < f j) :
f i < a
source
theorem lt_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [AddRightStrictMono α] (hf : HasSum f a) (i : ι) (hi : ∀ (j : ι), j ≠ i → 0 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 0 < f j) :
f i < a
source
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) :
∏ i ∈ s, f i ≤ ∏' (i : ι), f i
source
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) :
∑ i ∈ s, f i ≤ ∑' (i : ι), f i
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem tprod_le_of_prod_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Multipliable f) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) :
∏' (i : ι), f i ≤ a₂
source
theorem tsum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Summable f) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) :
∑' (i : ι), f i ≤ a₂
source
theorem tprod_le_of_prod_le' {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (ha₂ : 1 ≤ a₂) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) :
∏' (i : ι), f i ≤ a₂
source
theorem tsum_le_of_sum_le' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (ha₂ : 0 ≤ a₂) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) :
∑' (i : ι), f i ≤ a₂
source
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
source
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
source
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
source
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
source
theorem one_le_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} (h : ∀ (i : ι), 1 ≤ g i) :
1 ≤ ∏' (i : ι), g i
source
theorem tsum_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} (h : ∀ (i : ι), 0 ≤ g i) :
0 ≤ ∑' (i : ι), g i
source
theorem tprod_le_one {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (h : ∀ (i : ι), f i ≤ 1) :
∏' (i : ι), f i ≤ 1
source
theorem tsum_nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (h : ∀ (i : ι), f i ≤ 0) :
∑' (i : ι), f i ≤ 0
source
theorem hasProd_one_iff_of_one_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : ∀ (i : ι), 1 ≤ f i) :
HasProd f 1 ↔ f = 1
source
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
source
theorem hasProd_lt {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) :
a₁ < a₂
source
theorem hasSum_lt {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} (h : f ≤ g) (hi : f i < g i) (hf : HasSum f a₁) (hg : HasSum g a₂) :
a₁ < a₂
source
theorem hasProd_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) :
a₁ < a₂
source
theorem hasSum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) :
a₁ < a₂
source
theorem tprod_lt_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {i : ι} (h : f ≤ g) (hi : f i < g i) (hf : Multipliable f) (hg : Multipliable g) :
∏' (n : ι), f n < ∏' (n : ι), g n
source
theorem tsum_lt_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {i : ι} (h : f ≤ g) (hi : f i < g i) (hf : Summable f) (hg : Summable g) :
∑' (n : ι), f n < ∑' (n : ι), g n
source
theorem tprod_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Multipliable f) (hg : Multipliable g) (h : f < g) :
∏' (n : ι), f n < ∏' (n : ι), g n
source
theorem tsum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Summable f) (hg : Summable g) (h : f < g) :
∑' (n : ι), f n < ∑' (n : ι), g n
source
theorem one_lt_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Multipliable g) (hg : ∀ (i : ι), 1 ≤ g i) (i : ι) (hi : 1 < g i) :
1 < ∏' (i : ι), g i
source
theorem tsum_pos {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Summable g) (hg : ∀ (i : ι), 0 ≤ g i) (i : ι) (hi : 0 < g i) :
0 < ∑' (i : ι), g i
source
theorem le_hasProd' {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) (i : ι) :
f i ≤ a
source
theorem le_hasSum' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) (i : ι) :
f i ≤ a
source
theorem le_tprod' {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) (i : ι) :
f i ≤ ∏' (i : ι), f i
source
theorem le_tsum' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) (i : ι) :
f i ≤ ∑' (i : ι), f i
source
theorem hasProd_one_iff {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} :
HasProd f 1 ↔ ∀ (x : ι), f x = 1
source
theorem hasSum_zero_iff {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} :
HasSum f 0 ↔ ∀ (x : ι), f x = 0
source
theorem tprod_eq_one_iff {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) :
∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1
source
theorem tsum_eq_zero_iff {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) :
∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0
source
theorem tprod_ne_one_iff {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) :
∏' (i : ι), f i ≠ 1 ↔ ∃ (x : ι), f x ≠ 1
source
theorem tsum_ne_zero_iff {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) :
∑' (i : ι), f i ≠ 0 ↔ ∃ (x : ι), f x ≠ 0
source
theorem isLUB_hasProd' {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) :
IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) a
source
theorem isLUB_hasSum' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) :
IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, 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.

source
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 ι) => ∏ i ∈ s, f i) i) :
HasProd f i
source
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 ι) => ∑ i ∈ s, f i) i) :
HasSum f i
source
theorem hasProd_of_isLUB {ι : Type u_1} {α : Type u_3} [LinearOrderedCommMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) b) :
HasProd f b
source
theorem hasSum_of_isLUB {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, f i) b) :
HasSum f b
source
theorem multipliable_mabs_iff {ι : Type u_1} {α : Type u_3} [LinearOrderedCommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] {f : ι → α} :
(Multipliable fun (x : ι) => mabs (f x)) ↔ Multipliable f
source
theorem summable_abs_iff {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ι → α} :
(Summable fun (x : ι) => |f x|) ↔ Summable f
source
theorem Summable.abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ι → α} :
Summable f → Summable fun (x : ι) => |f x|

Alias of the reverse direction of summable_abs_iff.

source
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.

source
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 ι
source
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) :
univ.Finite
source
theorem HasProd.abs {ι : Type u_1} {α : Type u_3} [LinearOrderedCommRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} {x : α} (hfx : HasProd f x) :
HasProd (fun (x : ι) => |f x|) |x|
source
theorem Multipliable.abs {ι : Type u_1} {α : Type u_3} [LinearOrderedCommRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (hf : Multipliable f) :
Multipliable fun (x : ι) => |f x|
source
theorem abs_tprod {ι : Type u_1} {α : Type u_3} [LinearOrderedCommRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (hf : Multipliable f) :
|∏' (i : ι), f i| = ∏' (i : ι), |f i|
source
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