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} {L : SummationFilter ι} [Preorder α] [CommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot] (hf : HasProd f a L) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ c) : a ≤ c

theorem hasSum_le_of_sum_le {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot] (hf : HasSum f a L) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ c) : a ≤ c

theorem le_hasProd_of_le_prod {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [Preorder α] [CommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] [L.NeBot] (hf : HasProd f a L) (h : ∀ (s : Finset ι), c ≤ ∏ i ∈ s, f i) : c ≤ a

theorem le_hasSum_of_le_sum {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIciTopology α] [L.NeBot] (hf : HasSum f a L) (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

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

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

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

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

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

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

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

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

theorem isLUB_hasProd {ι : Type u_1} {α : Type u_3} [CommMonoid α] [Preorder α] [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 α] [Preorder α] [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} {L : SummationFilter ι} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop] (hf : HasProd f a L) (i : ι) (hb : ∀ (j : ι), j ≠ i → 1 ≤ f j) : f i ≤ a

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

theorem lt_hasProd {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop] [MulRightStrictMono α] (hf : HasProd f a L) (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} {L : SummationFilter ι} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop] [AddRightStrictMono α] (hf : HasSum f a L) (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} {L : SummationFilter ι} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [L.NeBot] [L.LeAtTop] {f : ι → α} (s : Finset ι) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : Multipliable f L) : ∏ i ∈ s, f i ≤ ∏'[L] (i : ι), f i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem hasProd_one_iff_of_one_le {ι : Type u_4} {α : Type u_5} {L : SummationFilter ι} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.LeAtTop] [L.NeBot] (hf : ∀ (i : ι), 1 ≤ f i) : HasProd f 1 L ↔ f = 1

theorem hasSum_zero_iff_of_nonneg {ι : Type u_4} {α : Type u_5} {L : SummationFilter ι} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.LeAtTop] [L.NeBot] (hf : ∀ (i : ι), 0 ≤ f i) : HasSum f 0 L ↔ f = 0

theorem hasProd_lt {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) : a₁ < a₂

theorem hasSum_lt {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι} [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : HasSum f a₁ L) (hg : HasSum g a₂ L) : 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} {L : SummationFilter ι} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {i : ι} [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : Multipliable f L) (hg : Multipliable g L) : ∏'[L] (n : ι), f n < ∏'[L] (n : ι), g n

theorem Summable.tsum_lt_tsum {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [IsTopologicalAddGroup α] [OrderClosedTopology α] {f g : ι → α} {i : ι} [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : Summable f L) (hg : Summable g L) : ∑'[L] (n : ι), f n < ∑'[L] (n : ι), g n

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

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

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

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

theorem HasProd.nonneg {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoidWithZero α] [TopologicalSpace α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] [L.NeBot] {f : ι → α} (hf : ∀ (i : ι), 0 ≤ f i) {a : α} (h : HasProd f a L) : 0 ≤ a

theorem tprod_nonneg {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoidWithZero α] [TopologicalSpace α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] {f : ι → α} (hf : ∀ (i : ι), 0 ≤ f i) : 0 ≤ ∏'[L] (x : ι), f x

theorem prod_le_hasProd_of_nonneg {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoidWithZero α] [TopologicalSpace α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] [L.NeBot] [L.LeAtTop] {f : ι → α} {a : α} {s : Finset ι} (hnonneg : ∀ i ∈ s, 0 ≤ f i) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : HasProd f a L) : ∏ i ∈ s, f i ≤ a

theorem Multipliable.prod_le_tprod_of_nonneg {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoidWithZero α] [TopologicalSpace α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] [ClosedIciTopology α] [L.NeBot] [L.LeAtTop] {f : ι → α} {s : Finset ι} (hnonneg : ∀ i ∈ s, 0 ≤ f i) (hs : ∀ i ∉ s, 1 ≤ f i) (hf : Multipliable f L) : ∏ i ∈ s, f i ≤ ∏'[L] (i : ι), f i

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

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

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

theorem isLUB_hasProd' {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [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 α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) : IsLUB (Set.range fun (s : Finset ι) => ∑ i ∈ s, f i) a

theorem CompleteLattice.hasSum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} : HasSum f (⨆ (s : Finset ι), ∑ a ∈ s, f a)

theorem CompleteLattice.summable {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} : Summable f

theorem tsum_eq_iSup_sum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} [T2Space α] : ∑' (x : ι), f x = ⨆ (s : Finset ι), ∑ a ∈ s, f a

theorem tsum_eq_iSup_sum' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} {f : ι → α} [T2Space α] (s : ι' → Finset ι) (hs : ∀ (t : Finset ι), ∃ (i : ι'), t ⊆ s i) : ∑' (a : ι), f a = ⨆ (i : ι'), ∑ a ∈ s i, f a

theorem tsum_add {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f g : ι → α} [T2Space α] [ContinuousAdd α] : ∑' (a : ι), (f a + g a) = ∑' (a : ι), f a + ∑' (a : ι), g a

See also Summable.tsum_add for more general result without CompleteLattice assumption.

theorem tsum_union_of_disjoint {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {s t : Set ι} [T2Space α] [ContinuousAdd α] (hd : Disjoint s t) : ∑' (x : ↑(s ∪ t)), f ↑x = ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

See also Summable.tsum_union_of_disjoint for more general result without CompleteLattice assumption.

theorem tsum_le_of_subset {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {s t : Set ι} [T2Space α] [ContinuousAdd α] (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

theorem tsum_union_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [T2Space α] [ContinuousAdd α] (f : ι → α) (s t : Set ι) : ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

theorem tsum_insert {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {s : Set ι} {i : ι} [T2Space α] [ContinuousAdd α] (h : i ∉ s) : ∑' (x : ↑(insert i s)), f ↑x = f i + ∑' (x : ↑s), f ↑x

theorem singleton_add_tsum_ne {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {i : ι} [T2Space α] [ContinuousAdd α] : f i + ∑' (x : { x : ι // x ≠ i }), f ↑x = ∑' (x : ι), f x

theorem tsum_eq_add_tsum_ite {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [T2Space α] [ContinuousAdd α] {f : ι' → α} (b : ι') : ∑' (x : ι'), f x = f b + ∑' (x : ι'), if x = b then 0 else f x

theorem tsum_fiberwise {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [ContinuousAdd α] [T3Space α] {ι'' : Type u_5} (f : ι' → α) (g : ι' → ι'') : ∑' (x : ι'') (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : ι'), f i

theorem tsum_comm {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [ContinuousAdd α] [T3Space α] {f : ι → ι' → α} : ∑' (a : ι) (b : ι'), f a b = ∑' (b : ι') (a : ι), f a b

See also Summable.tsum_comm' for more general result without CompleteLattice assumption.

theorem tsum_prod {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [ContinuousAdd α] [T3Space α] {f : ι → ι' → α} : ∑' (p : ι × ι'), f p.1 p.2 = ∑' (a : ι) (b : ι'), f a b

See also Summable.tsum_prod' for more general result without CompleteLattice assumption.

theorem tsum_prod' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [ContinuousAdd α] [T3Space α] {f : ι × ι' → α} : ∑' (p : ι × ι'), f p = ∑' (a : ι) (b : ι'), f (a, b)

See also Summable.tsum_prod' for more general result without CompleteLattice assumption.

theorem tsum_sigma {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [ContinuousAdd α] [T3Space α] {β : ι → Type u_5} (f : (a : ι) → β a → α) : ∑' (p : (i : ι) × β i), f p.fst p.snd = ∑' (i : ι) (j : β i), f i j

See also Summable.tsum_sigma' for more general result without CompleteLattice assumption.

theorem tsum_sigma' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [ContinuousAdd α] [T3Space α] {β : ι → Type u_5} (f : (i : ι) × β i → α) : ∑' (p : (i : ι) × β i), f p = ∑' (i : ι) (j : β i), f ⟨i, j⟩

See also Summable.tsum_sigma' for more general result without CompleteLattice assumption.

theorem tsum_biUnion {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} {f : ι → α} [ContinuousAdd α] [T3Space α] {S : Set ι'} {t : ι' → Set ι} (h : S.PairwiseDisjoint t) : ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x

theorem tsum_iUnion {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} {f : ι → α} [ContinuousAdd α] [T3Space α] {t : ι' → Set ι} (h : Set.univ.PairwiseDisjoint t) : ∑' (x : ↑(⋃ (i : ι'), t i)), f ↑x = ∑' (i : ι') (x : ↑(t i)), f ↑x

theorem tsum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f g : ι → α} [IsOrderedAddMonoid α] [OrderClosedTopology α] (h : f ≤ g) : ∑' (a : ι), f a ≤ ∑' (a : ι), g a

See also Summable.tsum_le_tsum for more general result without CompleteLattice assumption.

theorem sum_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} [IsOrderedAddMonoid α] [OrderClosedTopology α] (s : Finset ι) : ∑ x ∈ s, f x ≤ ∑' (x : ι), f x

See also Summable.sum_le_tsum for more general result without CompleteLattice assumption.

theorem le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [IsOrderedAddMonoid α] [OrderClosedTopology α] (f : ι → α) (a : ι) : f a ≤ ∑' (a : ι), f a

See also Summable.le_tsum' for more general result without CompleteLattice assumption.

theorem le_tsum_of_mem {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {s : Set ι} {i : ι} [IsOrderedAddMonoid α] [OrderClosedTopology α] (hi : i ∈ s) : f i ≤ ∑' (x : ↑s), f ↑x

@[simp]

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

See also Summable.tsum_eq_zero_iff for more general result without CompleteLattice assumption.

theorem tsum_eq_top_of_eq_top {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} [IsOrderedAddMonoid α] [OrderClosedTopology α] : (∃ (a : ι), f a = ⊤) → ∑' (a : ι), f a = ⊤

theorem tsum_subtype_eq_top_of_eq_top {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} {s : Set ι} [IsOrderedAddMonoid α] [OrderClosedTopology α] (h : ∃ a ∈ s, f a = ⊤) : ∑' (a : ↑s), f ↑a = ⊤

theorem tsum_comp_le_tsum_of_injective {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] {f : ι → ι'} (hf : Function.Injective f) (g : ι' → α) : ∑' (x : ι), g (f x) ≤ ∑' (y : ι'), g y

See also Summable.tsum_le_tsum_of_inj for more general result without CompleteLattice assumption.

theorem tsum_le_tsum_comp_of_surjective {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] {f : ι → ι'} (hf : Function.Surjective f) (g : ι' → α) : ∑' (y : ι'), g y ≤ ∑' (x : ι), g (f x)

theorem tsum_comp_eq_tsum_of_bijective {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] {f : ι → ι'} (hf : Function.Bijective f) (g : ι' → α) : ∑' (x : ι), g (f x) = ∑' (y : ι'), g y

theorem tsum_range_le_tsum_comp {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] (f : ι → α) (g : ι' → ι) : ∑' (x : ↑(Set.range g)), f ↑x ≤ ∑' (x : ι'), f (g x)

theorem tsum_comp_eq_tsum_of_equiv {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] (e : ι ≃ ι') (g : ι' → α) : ∑' (x : ι), g (e x) = ∑' (y : ι'), g y

theorem tsum_image_le_tsum_comp {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] (f : ι → α) (g : ι' → ι) (s : Set ι') : ∑' (x : ↑(g '' s)), f ↑x ≤ ∑' (x : ↑s), f (g ↑x)

theorem tsum_mono_subtype {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {s t : Set ι} [IsOrderedAddMonoid α] [OrderClosedTopology α] (f : ι → α) (h : s ⊆ t) : ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x

@[simp]

theorem tsum_top {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [IsOrderedAddMonoid α] [OrderClosedTopology α] [Nonempty α] : ∑' (x : α), ⊤ = ⊤

theorem ne_top_of_tsum_ne_top {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {f : ι → α} [IsOrderedAddMonoid α] [OrderClosedTopology α] (h : ∑' (a : ι), f a ≠ ⊤) (i : ι) : f i ≠ ⊤

theorem tsum_iUnion_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] (f : ι → α) (t : ι' → Set ι) : ∑' (x : ↑(⋃ (i : ι'), t i)), f ↑x ≤ ∑' (i : ι') (x : ↑(t i)), f ↑x

theorem tsum_biUnion_le_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] (f : ι → α) (s : Set ι') (t : ι' → Set ι) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑' (i : ↑s) (x : ↑(t ↑i)), f ↑x

theorem tsum_biUnion_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] (f : ι → α) (s : Finset ι') (t : ι' → Set ι) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x ≤ ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x

theorem tsum_iUnion_le {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] [Fintype ι'] (f : ι → α) (t : ι' → Set ι) : ∑' (x : ↑(⋃ (i : ι'), t i)), f ↑x ≤ ∑ i : ι', ∑' (x : ↑(t i)), f ↑x

theorem tsum_iUnion_eq_tsum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] (f : ι → α) (t : ι' → Set ι) (ht : Pairwise (Function.onFun Disjoint t)) : ∑' (x : ↑(⋃ (i : ι'), t i)), f ↑x = ∑' (i : ι') (x : ↑(t i)), f ↑x

theorem sum_add_tsum_compl {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [OrderClosedTopology α] [ContinuousAdd α] (s : Finset ι') (f : ι' → α) : ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι'), f i

theorem tsum_iUnion_le_sum {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] {ι' : Type u_4} [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] [Fintype ι'] (f : ι → α) (t : ι' → Set ι) : ∑' (x : ↑(⋃ (i : ι'), t i)), f ↑x ≤ ∑ i : ι', ∑' (x : ↑(t i)), f ↑x

theorem tsum_subtype_eq_tsum_support {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [CompleteLattice α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [SupConvergenceClass α] [IsOrderedAddMonoid α] [OrderClosedTopology α] [ContinuousAdd α] [T3Space α] (s : Set ι) (f : ι → α) : ∑' (x : ↑s), f ↑x = ∑' (x : ↑{x : ι | x ∈ s ∧ f x ≠ 0}), f ↑x

theorem mul_tsum {α : Type u_3} {R : Type u_4} [Semiring R] [CompleteLattice R] [IsQuantale R] [TopologicalSpace R] [CanonicallyOrderedAdd R] [SupConvergenceClass R] [T2Space R] (c : R) (f : α → R) : c * ∑' (a : α), f a = ∑' (a : α), c * f a

theorem tsum_mul {α : Type u_3} {R : Type u_4} [Semiring R] [CompleteLattice R] [IsQuantale R] [TopologicalSpace R] [CanonicallyOrderedAdd R] [SupConvergenceClass R] [T2Space R] (c : R) (f : α → R) : (∑' (a : α), f a) * c = ∑' (a : α), f a * c

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_isGLB_of_le_one {ι : Type u_1} {α : Type u_3} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α) (h₀ : ∀ (i : ι), f i ≤ 1) (hf : IsGLB (Set.range fun (s : Finset ι) => ∏ i ∈ s, f i) i) : HasProd f i

theorem hasSum_of_isGLB_of_nonpos {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α) (h₀ : ∀ (i : ι), f i ≤ 0) (hf : IsGLB (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 α] [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 α] [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 : ι) => |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.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 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 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|

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.