Infinite sum or product in an order

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

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

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

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

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

theorem Multipliable.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

theorem Summable.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

@[deprecated Summable.tsum_le_of_sum_range_le (since := "2025-04-12")]

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

Alias of Summable.tsum_le_of_sum_range_le.

@[deprecated Multipliable.tprod_le_of_prod_range_le (since := "2025-04-12")]

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

Alias of Multipliable.tprod_le_of_prod_range_le.

theorem hasProd_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (h : ∀ (i : ι), f i ≤ g i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂

theorem hasSum_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (h : ∀ (i : ι), f i ≤ g i) (hf : HasSum f a₁) (hg : HasSum g a₂) : a₁ ≤ a₂

theorem hasProd_mono {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f ≤ g) : a₁ ≤ a₂

theorem hasSum_mono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f ≤ g) : a₁ ≤ a₂

theorem hasProd_le_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [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 hasSum_le_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [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 Multipliable.tprod_le_tprod_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [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

theorem Summable.tsum_le_tsum_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [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

@[deprecated Summable.tsum_le_tsum_of_inj (since := "2025-04-12")]

theorem tsum_le_tsum_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [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

Alias of Summable.tsum_le_tsum_of_inj.

@[deprecated Multipliable.tprod_le_tprod_of_inj (since := "2025-04-12")]

theorem tprod_le_tprod_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [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

Alias of Multipliable.tprod_le_tprod_of_inj.

theorem Multipliable.tprod_subtype_le {κ : Type u_4} {γ : Type u_5} [CommGroup γ] [PartialOrder γ] [IsOrderedMonoid γ] [UniformSpace γ] [IsUniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 1 ≤ f a) (hf : Multipliable f) : ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

theorem Summable.tsum_subtype_le {κ : Type u_4} {γ : Type u_5} [AddCommGroup γ] [PartialOrder γ] [IsOrderedAddMonoid γ] [UniformSpace γ] [IsUniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 0 ≤ f a) (hf : Summable f) : ∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a

@[deprecated Summable.tsum_subtype_le (since := "2025-04-12")]

theorem tsum_subtype_le {κ : Type u_4} {γ : Type u_5} [AddCommGroup γ] [PartialOrder γ] [IsOrderedAddMonoid γ] [UniformSpace γ] [IsUniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 0 ≤ f a) (hf : Summable f) : ∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a

Alias of Summable.tsum_subtype_le.

@[deprecated Multipliable.tprod_subtype_le (since := "2025-04-12")]

theorem tprod_subtype_le {κ : Type u_4} {γ : Type u_5} [CommGroup γ] [PartialOrder γ] [IsOrderedMonoid γ] [UniformSpace γ] [IsUniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ (a : κ), 1 ≤ f a) (hf : Multipliable f) : ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

Alias of Multipliable.tprod_subtype_le.

theorem prod_le_hasProd {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (s : Finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : HasProd f a) : ∏ i ∈ s, f i ≤ a

theorem sum_le_hasSum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (s : Finset ι) (hs : ∀ i ∉ s, 0 ≤ f i) (hf : HasSum f a) : ∑ i ∈ s, f i ≤ a

theorem isLUB_hasProd {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (h : ∀ (i : ι), 1 ≤ f i) (hf : HasProd f a) : IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) a

theorem isLUB_hasSum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (h : ∀ (i : ι), 0 ≤ f i) (hf : HasSum f a) : IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, f i) a

theorem le_hasProd {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) (i : ι) (hb : ∀ (j : ι), j ≠ i → 1 ≤ f j) : f i ≤ a

theorem le_hasSum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) (i : ι) (hb : ∀ (j : ι), j ≠ i → 0 ≤ f j) : f i ≤ a

theorem lt_hasProd {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [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

theorem lt_hasSum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [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

theorem Multipliable.prod_le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (s : Finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : Multipliable f) : ∏ i ∈ s, f i ≤ ∏' (i : ι), f i

theorem Summable.sum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (s : Finset ι) (hs : ∀ i ∉ s, 0 ≤ f i) (hf : Summable f) : ∑ i ∈ s, f i ≤ ∑' (i : ι), f i

@[deprecated Summable.sum_le_tsum (since := "2025-04-12")]

theorem sum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (s : Finset ι) (hs : ∀ i ∉ s, 0 ≤ f i) (hf : Summable f) : ∑ i ∈ s, f i ≤ ∑' (i : ι), f i

Alias of Summable.sum_le_tsum.

@[deprecated Multipliable.prod_le_tprod (since := "2025-04-12")]

theorem prod_le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (s : Finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : Multipliable f) : ∏ i ∈ s, f i ≤ ∏' (i : ι), f i

Alias of Multipliable.prod_le_tprod.

theorem Multipliable.le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) (i : ι) (hb : ∀ (j : ι), j ≠ i → 1 ≤ f j) : f i ≤ ∏' (i : ι), f i

theorem Summable.le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) (i : ι) (hb : ∀ (j : ι), j ≠ i → 0 ≤ f j) : f i ≤ ∑' (i : ι), f i

@[deprecated Summable.le_tsum (since := "2025-04-12")]

theorem le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) (i : ι) (hb : ∀ (j : ι), j ≠ i → 0 ≤ f j) : f i ≤ ∑' (i : ι), f i

Alias of Summable.le_tsum.

@[deprecated Multipliable.le_tprod (since := "2025-04-12")]

theorem le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) (i : ι) (hb : ∀ (j : ι), j ≠ i → 1 ≤ f j) : f i ≤ ∏' (i : ι), f i

Alias of Multipliable.le_tprod.

theorem Multipliable.tprod_le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) (hf : Multipliable f) (hg : Multipliable g) : ∏' (i : ι), f i ≤ ∏' (i : ι), g i

theorem Summable.tsum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) (hf : Summable f) (hg : Summable g) : ∑' (i : ι), f i ≤ ∑' (i : ι), g i

@[deprecated Summable.tsum_le_tsum (since := "2025-04-12")]

theorem tsum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) (hf : Summable f) (hg : Summable g) : ∑' (i : ι), f i ≤ ∑' (i : ι), g i

Alias of Summable.tsum_le_tsum.

@[deprecated Multipliable.tprod_le_tprod (since := "2025-04-12")]

theorem tprod_le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (h : ∀ (i : ι), f i ≤ g i) (hf : Multipliable f) (hg : Multipliable g) : ∏' (i : ι), f i ≤ ∏' (i : ι), g i

Alias of Multipliable.tprod_le_tprod.

theorem Multipliable.tprod_mono {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (hf : Multipliable f) (hg : Multipliable g) (h : f ≤ g) : ∏' (n : ι), f n ≤ ∏' (n : ι), g n

theorem Summable.tsum_mono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (hf : Summable f) (hg : Summable g) (h : f ≤ g) : ∑' (n : ι), f n ≤ ∑' (n : ι), g n

@[deprecated Summable.tsum_mono (since := "2025-04-12")]

theorem tsum_mono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (hf : Summable f) (hg : Summable g) (h : f ≤ g) : ∑' (n : ι), f n ≤ ∑' (n : ι), g n

Alias of Summable.tsum_mono.

@[deprecated Multipliable.tprod_mono (since := "2025-04-12")]

theorem tprod_mono {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} (hf : Multipliable f) (hg : Multipliable g) (h : f ≤ g) : ∏' (n : ι), f n ≤ ∏' (n : ι), g n

Alias of Multipliable.tprod_mono.

theorem Multipliable.tprod_le_of_prod_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Multipliable f) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) : ∏' (i : ι), f i ≤ a₂

theorem Summable.tsum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Summable f) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) : ∑' (i : ι), f i ≤ a₂

@[deprecated Summable.tsum_le_of_sum_le (since := "2025-04-12")]

theorem tsum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Summable f) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) : ∑' (i : ι), f i ≤ a₂

Alias of Summable.tsum_le_of_sum_le.

@[deprecated Multipliable.tprod_le_of_prod_le (since := "2025-04-12")]

theorem tprod_le_of_prod_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (hf : Multipliable f) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) : ∏' (i : ι), f i ≤ a₂

Alias of Multipliable.tprod_le_of_prod_le.

theorem tprod_le_of_prod_le' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (ha₂ : 1 ≤ a₂) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) : ∏' (i : ι), f i ≤ a₂

theorem tsum_le_of_sum_le' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} (ha₂ : 0 ≤ a₂) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂) : ∑' (i : ι), f i ≤ a₂

theorem HasProd.one_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} (h : ∀ (i : ι), 1 ≤ g i) (ha : HasProd g a) : 1 ≤ a

theorem HasSum.nonneg {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} (h : ∀ (i : ι), 0 ≤ g i) (ha : HasSum g a) : 0 ≤ a

theorem HasProd.le_one {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} (h : ∀ (i : ι), g i ≤ 1) (ha : HasProd g a) : a ≤ 1

theorem HasSum.nonpos {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} (h : ∀ (i : ι), g i ≤ 0) (ha : HasSum g a) : a ≤ 0

theorem one_le_tprod {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} (h : ∀ (i : ι), 1 ≤ g i) : 1 ≤ ∏' (i : ι), g i

theorem tsum_nonneg {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} (h : ∀ (i : ι), 0 ≤ g i) : 0 ≤ ∑' (i : ι), g i

theorem tprod_le_one {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (h : ∀ (i : ι), f i ≤ 1) : ∏' (i : ι), f i ≤ 1

theorem tsum_nonpos {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (h : ∀ (i : ι), f i ≤ 0) : ∑' (i : ι), f i ≤ 0

theorem hasProd_one_iff_of_one_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : ∀ (i : ι), 1 ≤ f i) : HasProd f 1 ↔ f = 1

theorem hasSum_zero_iff_of_nonneg {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : ∀ (i : ι), 0 ≤ f i) : HasSum f 0 ↔ f = 0

theorem hasProd_lt {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [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₂

theorem hasSum_lt {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [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₂

theorem hasProd_strict_mono {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) : a₁ < a₂

theorem hasSum_strict_mono {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) : a₁ < a₂

theorem Multipliable.tprod_lt_tprod {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [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

theorem Summable.tsum_lt_tsum {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [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

@[deprecated Summable.tsum_lt_tsum (since := "2025-04-12")]

theorem tsum_lt_tsum {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [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

Alias of Summable.tsum_lt_tsum.

@[deprecated Multipliable.tprod_lt_tprod (since := "2025-04-12")]

theorem tprod_lt_tprod {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [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

Alias of Multipliable.tprod_lt_tprod.

theorem Multipliable.tprod_strict_mono {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Multipliable f) (hg : Multipliable g) (h : f < g) : ∏' (n : ι), f n < ∏' (n : ι), g n

theorem Summable.tsum_strict_mono {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Summable f) (hg : Summable g) (h : f < g) : ∑' (n : ι), f n < ∑' (n : ι), g n

@[deprecated Summable.tsum_strict_mono (since := "2025-04-12")]

theorem tsum_strict_mono {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Summable f) (hg : Summable g) (h : f < g) : ∑' (n : ι), f n < ∑' (n : ι), g n

Alias of Summable.tsum_strict_mono.

@[deprecated Multipliable.tprod_strict_mono (since := "2025-04-12")]

theorem tprod_strict_mono {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} (hf : Multipliable f) (hg : Multipliable g) (h : f < g) : ∏' (n : ι), f n < ∏' (n : ι), g n

Alias of Multipliable.tprod_strict_mono.

theorem Multipliable.one_lt_tprod {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Multipliable g) (hg : ∀ (i : ι), 1 ≤ g i) (i : ι) (hi : 1 < g i) : 1 < ∏' (i : ι), g i

theorem Summable.tsum_pos {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Summable g) (hg : ∀ (i : ι), 0 ≤ g i) (i : ι) (hi : 0 < g i) : 0 < ∑' (i : ι), g i

@[deprecated Summable.tsum_pos (since := "2025-04-12")]

theorem tsum_pos {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Summable g) (hg : ∀ (i : ι), 0 ≤ g i) (i : ι) (hi : 0 < g i) : 0 < ∑' (i : ι), g i

Alias of Summable.tsum_pos.

@[deprecated Multipliable.one_lt_tprod (since := "2025-04-12")]

theorem one_lt_tprod {ι : Type u_1} {α : Type u_3} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {g : ι → α} (hsum : Multipliable g) (hg : ∀ (i : ι), 1 ≤ g i) (i : ι) (hi : 1 < g i) : 1 < ∏' (i : ι), g i

Alias of Multipliable.one_lt_tprod.

theorem le_hasProd' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) (i : ι) : f i ≤ a

theorem le_hasSum' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) (i : ι) : f i ≤ a

theorem Multipliable.le_tprod' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) (i : ι) : f i ≤ ∏' (i : ι), f i

theorem Summable.le_tsum' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) (i : ι) : f i ≤ ∑' (i : ι), f i

@[deprecated Summable.le_tsum' (since := "2025-04-12")]

theorem le_tsum' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) (i : ι) : f i ≤ ∑' (i : ι), f i

Alias of Summable.le_tsum'.

@[deprecated Multipliable.le_tprod' (since := "2025-04-12")]

theorem le_tprod' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) (i : ι) : f i ≤ ∏' (i : ι), f i

Alias of Multipliable.le_tprod'.

theorem hasProd_one_iff {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} : HasProd f 1 ↔ ∀ (x : ι), f x = 1

theorem hasSum_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} : HasSum f 0 ↔ ∀ (x : ι), f x = 0

theorem Multipliable.tprod_eq_one_iff {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) : ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

theorem Summable.tsum_eq_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) : ∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0

@[deprecated Summable.tsum_eq_zero_iff (since := "2025-04-12")]

theorem tsum_eq_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) : ∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0

Alias of Summable.tsum_eq_zero_iff.

@[deprecated Multipliable.tprod_eq_one_iff (since := "2025-04-12")]

theorem tprod_eq_one_iff {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) : ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

Alias of Multipliable.tprod_eq_one_iff.

theorem Multipliable.tprod_ne_one_iff {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) : ∏' (i : ι), f i ≠ 1 ↔ ∃ (x : ι), f x ≠ 1

theorem Summable.tsum_ne_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) : ∑' (i : ι), f i ≠ 0 ↔ ∃ (x : ι), f x ≠ 0

@[deprecated Summable.tsum_ne_zero_iff (since := "2025-04-12")]

theorem tsum_ne_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Summable f) : ∑' (i : ι), f i ≠ 0 ↔ ∃ (x : ι), f x ≠ 0

Alias of Summable.tsum_ne_zero_iff.

@[deprecated Multipliable.tprod_ne_one_iff (since := "2025-04-12")]

theorem tprod_ne_one_iff {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} (hf : Multipliable f) : ∏' (i : ι), f i ≠ 1 ↔ ∃ (x : ι), f x ≠ 1

Alias of Multipliable.tprod_ne_one_iff.

theorem isLUB_hasProd' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) : IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) a

theorem isLUB_hasSum' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [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.

theorem hasProd_of_isLUB_of_one_le {ι : Type u_1} {α : Type u_3} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α) (h : ∀ (i : ι), 1 ≤ f i) (hf : IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) i) : HasProd f i

theorem hasSum_of_isLUB_of_nonneg {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α) (h : ∀ (i : ι), 0 ≤ f i) (hf : IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, f i) i) : HasSum f i

theorem hasProd_of_isLUB {ι : Type u_1} {α : Type u_3} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) b) : HasProd f b

theorem hasSum_of_isLUB {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, f i) b) : HasSum f b

theorem multipliable_mabs_iff {ι : Type u_1} {α : Type u_3} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {f : ι → α} : (Multipliable fun (x : ι) => mabs (f x)) ↔ Multipliable f

theorem summable_abs_iff {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ι → α} : (Summable fun (x : ι) => |f x|) ↔ Summable f

theorem Summable.of_abs {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [UniformSpace α] [IsUniformAddGroup α] [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} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ι → α} : Summable f → Summable fun (x : ι) => |f x|

Alias of the reverse direction of summable_abs_iff.

theorem Finite.of_summable_const {ι : Type u_1} {α : Type u_3} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [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} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun (x : ι) => b) : univ.Finite

theorem HasProd.abs {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} {x : α} (hfx : HasProd f x) : HasProd (fun (x : ι) => |f x|) |x|

theorem Multipliable.abs {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (hf : Multipliable f) : Multipliable fun (x : ι) => |f x|

theorem Multipliable.abs_tprod {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (hf : Multipliable f) : |∏' (i : ι), f i| = ∏' (i : ι), |f i|

@[deprecated Multipliable.abs_tprod (since := "2025-04-12")]

theorem abs_tprod {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (hf : Multipliable f) : |∏' (i : ι), f i| = ∏' (i : ι), |f i|

Alias of Multipliable.abs_tprod.

theorem Summable.tendsto_atTop_of_pos {α : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α] {f : ℕ → α} (hf : Summable f⁻¹) (hf' : ∀ (n : ℕ), 0 < f n) : Filter.Tendsto f Filter.atTop Filter.atTop

def Mathlib.Meta.Positivity.evalTsum : PositivityExt

Positivity extension for infinite sums.

This extension only proves non-negativity, strict positivity is more delicate for infinite sums and requires more assumptions.