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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
@[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)
:
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)
:
Alias of Multipliable.tprod_le_of_prod_range_le.
theorem
hasProd_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[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]
:
theorem
hasSum_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[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]
:
theorem
hasProd_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
{a₁ a₂ : α}
(hf : HasProd f a₁ L)
(hg : HasProd g a₂ L)
(h : f ≤ g)
[L.NeBot]
:
theorem
hasSum_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
{a₁ a₂ : α}
(hf : HasSum f a₁ L)
(hg : HasSum g a₂ L)
(h : f ≤ g)
[L.NeBot]
:
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₂)
:
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₂)
:
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)
:
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)
:
@[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)
:
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)
:
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)
:
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)
:
@[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)
:
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)
:
Alias of Multipliable.tprod_subtype_le.
theorem
prod_le_hasProd
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
[L.NeBot]
[L.LeAtTop]
(s : Finset ι)
(hs : ∀ i ∉ s, 1 ≤ f i)
(hf : HasProd f a L)
:
theorem
sum_le_hasSum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
[L.NeBot]
[L.LeAtTop]
(s : Finset ι)
(hs : ∀ i ∉ s, 0 ≤ f i)
(hf : HasSum f a L)
:
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)
:
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)
:
theorem
le_hasProd
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
[L.NeBot]
[L.LeAtTop]
(hf : HasProd f a L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 1 ≤ f j)
:
theorem
le_hasSum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
[L.NeBot]
[L.LeAtTop]
(hf : HasSum f a L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 0 ≤ f j)
:
theorem
lt_hasProd
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[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)
:
theorem
lt_hasSum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[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)
:
theorem
Multipliable.prod_le_tprod
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
[L.NeBot]
[L.LeAtTop]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 1 ≤ f i)
(hf : Multipliable f L)
:
theorem
Summable.sum_le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
[L.NeBot]
[L.LeAtTop]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 0 ≤ f i)
(hf : Summable f L)
:
@[deprecated Summable.sum_le_tsum (since := "2025-04-12")]
theorem
sum_le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
[L.NeBot]
[L.LeAtTop]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 0 ≤ f i)
(hf : Summable f L)
:
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}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
[L.NeBot]
[L.LeAtTop]
{f : ι → α}
(s : Finset ι)
(hs : ∀ i ∉ s, 1 ≤ f i)
(hf : Multipliable f L)
:
Alias of Multipliable.prod_le_tprod.
theorem
Multipliable.le_tprod
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.NeBot]
[L.LeAtTop]
(hf : Multipliable f L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 1 ≤ f j)
:
theorem
Summable.le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.NeBot]
[L.LeAtTop]
(hf : Summable f L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 0 ≤ f j)
:
@[deprecated Summable.le_tsum (since := "2025-04-12")]
theorem
le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.NeBot]
[L.LeAtTop]
(hf : Summable f L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 0 ≤ f j)
:
Alias of Summable.le_tsum.
@[deprecated Multipliable.le_tprod (since := "2025-04-12")]
theorem
le_tprod
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.NeBot]
[L.LeAtTop]
(hf : Multipliable f L)
(i : ι)
(hb : ∀ (j : ι), j ≠ i → 1 ≤ f j)
:
Alias of Multipliable.le_tprod.
theorem
Multipliable.tprod_le_tprod
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(h : ∀ (i : ι), f i ≤ g i)
(hf : Multipliable f L)
(hg : Multipliable g L)
:
theorem
Summable.tsum_le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(h : ∀ (i : ι), f i ≤ g i)
(hf : Summable f L)
(hg : Summable g L)
:
@[deprecated Summable.tsum_le_tsum (since := "2025-04-12")]
theorem
tsum_le_tsum
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(h : ∀ (i : ι), f i ≤ g i)
(hf : Summable f L)
(hg : Summable g L)
:
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}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(h : ∀ (i : ι), f i ≤ g i)
(hf : Multipliable f L)
(hg : Multipliable g L)
:
Alias of Multipliable.tprod_le_tprod.
theorem
Multipliable.tprod_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(hf : Multipliable f L)
(hg : Multipliable g L)
(h : f ≤ g)
:
theorem
Summable.tsum_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(hf : Summable f L)
(hg : Summable g L)
(h : f ≤ g)
:
@[deprecated Summable.tsum_mono (since := "2025-04-12")]
theorem
tsum_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(hf : Summable f L)
(hg : Summable g L)
(h : f ≤ g)
:
Alias of Summable.tsum_mono.
@[deprecated Multipliable.tprod_mono (since := "2025-04-12")]
theorem
tprod_mono
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f g : ι → α}
[L.NeBot]
(hf : Multipliable f L)
(hg : Multipliable g L)
(h : f ≤ g)
:
Alias of Multipliable.tprod_mono.
theorem
Multipliable.tprod_le_of_prod_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
[L.NeBot]
(hf : Multipliable f L)
(h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂)
:
theorem
Summable.tsum_le_of_sum_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
[L.NeBot]
(hf : Summable f L)
(h : ∀ (s : Finset ι), ∑ i ∈ s, 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}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
[L.NeBot]
(hf : Summable f L)
(h : ∀ (s : Finset ι), ∑ i ∈ s, 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}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
[L.NeBot]
(hf : Multipliable f L)
(h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂)
:
Alias of Multipliable.tprod_le_of_prod_le.
theorem
tprod_le_of_prod_le'
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
(ha₂ : 1 ≤ a₂)
(h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂)
:
theorem
tsum_le_of_sum_le'
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a₂ : α}
(ha₂ : 0 ≤ a₂)
(h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ a₂)
:
theorem
HasProd.one_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
[L.NeBot]
(h : ∀ (i : ι), 1 ≤ g i)
(ha : HasProd g a L)
:
theorem
HasSum.nonneg
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
[L.NeBot]
(h : ∀ (i : ι), 0 ≤ g i)
(ha : HasSum g a L)
:
theorem
HasProd.le_one
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
[L.NeBot]
(h : ∀ (i : ι), g i ≤ 1)
(ha : HasProd g a L)
:
theorem
HasSum.nonpos
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
{a : α}
[L.NeBot]
(h : ∀ (i : ι), g i ≤ 0)
(ha : HasSum g a L)
:
theorem
one_le_tprod
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
(h : ∀ (i : ι), 1 ≤ g i)
:
theorem
tsum_nonneg
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{g : ι → α}
(h : ∀ (i : ι), 0 ≤ g i)
:
theorem
tprod_le_one
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(h : ∀ (i : ι), f i ≤ 1)
:
theorem
tsum_nonpos
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(h : ∀ (i : ι), f i ≤ 0)
:
theorem
hasProd_one_iff_of_one_le
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.LeAtTop]
[L.NeBot]
(hf : ∀ (i : ι), 1 ≤ f i)
:
theorem
hasSum_zero_iff_of_nonneg
{ι : Type u_1}
{α : Type u_3}
{L : SummationFilter ι}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
[L.LeAtTop]
[L.NeBot]
(hf : ∀ (i : ι), 0 ≤ f i)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
@[deprecated Summable.tsum_lt_tsum (since := "2025-04-12")]
theorem
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)
:
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}
{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)
:
Alias of Multipliable.tprod_lt_tprod.
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)
:
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)
:
@[deprecated Summable.tsum_strict_mono (since := "2025-04-12")]
theorem
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)
:
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}
{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)
:
Alias of Multipliable.tprod_strict_mono.
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)
:
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)
:
@[deprecated Summable.tsum_pos (since := "2025-04-12")]
theorem
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)
:
Alias of Summable.tsum_pos.
@[deprecated Multipliable.one_lt_tprod (since := "2025-04-12")]
theorem
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)
:
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 : ι)
:
theorem
le_hasSum'
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasSum f a)
(i : ι)
:
theorem
Multipliable.le_tprod'
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[CanonicallyOrderedMul α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable f)
(i : ι)
:
theorem
Summable.le_tsum'
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable 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 : ι)
:
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 : ι)
:
Alias of Multipliable.le_tprod'.
theorem
hasProd_one_iff
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[CanonicallyOrderedMul α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
:
theorem
hasSum_zero_iff
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
:
theorem
Multipliable.tprod_eq_one_iff
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[PartialOrder α]
[IsOrderedMonoid α]
[CanonicallyOrderedMul α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Multipliable f)
:
theorem
Summable.tsum_eq_zero_iff
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
@[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)
:
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)
:
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)
:
theorem
Summable.tsum_ne_zero_iff
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
(hf : Summable f)
:
@[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)
:
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)
:
Alias of Multipliable.tprod_ne_one_iff.
theorem
isLUB_hasProd'
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[PartialOrder α]
[CanonicallyOrderedMul α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasProd f a)
:
theorem
isLUB_hasSum'
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[CanonicallyOrderedAdd α]
[TopologicalSpace α]
[OrderClosedTopology α]
{f : ι → α}
{a : α}
(hf : HasSum f a)
:
For infinite sums taking values in a linearly ordered monoid, the existence of a least upper bound for the finite sums is a criterion for summability.
This criterion is useful when applied in a linearly ordered monoid which is also a complete or
conditionally complete linear order, such as ℝ, ℝ≥0, ℝ≥0∞, because it is then easy to check
the existence of a least upper bound.
theorem
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 α]
[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 : ι → α}
:
theorem
summable_abs_iff
{ι : Type u_1}
{α : Type u_3}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{f : ι → α}
:
theorem
Summable.of_abs
{ι : Type u_1}
{α : Type u_3}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{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 : ι → α}
:
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)
:
theorem
HasProd.abs
{ι : Type u_1}
{α : Type u_3}
[CommRing α]
[LinearOrder α]
[IsStrictOrderedRing α]
[TopologicalSpace α]
[OrderTopology α]
{f : ι → α}
{x : α}
(hfx : HasProd f 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)
:
@[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)
:
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)
:
Positivity extension for infinite sums.
This extension only proves non-negativity, strict positivity is more delicate for infinite sums and requires more assumptions.