Documentation

Mathlib.Topology.Algebra.InfiniteSum.Order

Infinite sum or product in an order #

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

abbrev tsum_le_of_sum_range_le.match_1 {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {f : α} (motive : Summable fProp) :
∀ (hf : Summable f), (∀ (_l : α) (hl : HasSum f _l), motive )motive hf
Equations
  • =
Instances For
    theorem tsum_le_of_sum_range_le {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α] {f : α} {c : α} (hf : Summable f) (h : ∀ (n : ), iFinset.range n, f i c) :
    ∑' (n : ), f n c
    theorem tprod_le_of_prod_range_le {α : Type u_3} [Preorder α] [CommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] [T2Space α] {f : α} {c : α} (hf : Multipliable f) (h : ∀ (n : ), iFinset.range n, f i c) :
    ∏' (n : ), f n c
    theorem hasSum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (h : ∀ (i : ι), f i g i) (hf : HasSum f a₁) (hg : HasSum g a₂) :
    a₁ a₂
    theorem hasProd_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (h : ∀ (i : ι), f i g i) (hf : HasProd f a₁) (hg : HasProd g a₂) :
    a₁ a₂
    theorem hasSum_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f g) :
    a₁ a₂
    theorem hasProd_mono {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f g) :
    a₁ a₂
    theorem hasSum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasSum f a) (h : ∀ (s : Finset ι), is, f i a₂) :
    a a₂
    theorem hasProd_le_of_prod_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasProd f a) (h : ∀ (s : Finset ι), is, f i a₂) :
    a a₂
    theorem le_hasSum_of_le_sum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasSum f a) (h : ∀ (s : Finset ι), a₂ is, f i) :
    a₂ a
    theorem le_hasProd_of_le_prod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} {a₂ : α} (hf : HasProd f a) (h : ∀ (s : Finset ι), a₂ is, f i) :
    a₂ a
    theorem hasSum_le_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₁ : α} {a₂ : α} {g : κα} (e : ικ) (he : Function.Injective e) (hs : cSet.range e, 0 g c) (h : ∀ (i : ι), f i g (e i)) (hf : HasSum f a₁) (hg : HasSum g a₂) :
    a₁ a₂
    theorem hasProd_le_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₁ : α} {a₂ : α} {g : κα} (e : ικ) (he : Function.Injective e) (hs : cSet.range e, 1 g c) (h : ∀ (i : ι), f i g (e i)) (hf : HasProd f a₁) (hg : HasProd g a₂) :
    a₁ a₂
    theorem tsum_le_tsum_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : κα} (e : ικ) (he : Function.Injective e) (hs : cSet.range e, 0 g c) (h : ∀ (i : ι), f i g (e i)) (hf : Summable f) (hg : Summable g) :
    theorem tprod_le_tprod_of_inj {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : κα} (e : ικ) (he : Function.Injective e) (hs : cSet.range e, 1 g c) (h : ∀ (i : ι), f i g (e i)) (hf : Multipliable f) (hg : Multipliable g) :
    theorem tsum_subtype_le {κ : Type u_4} {γ : Type u_5} [OrderedAddCommGroup γ] [UniformSpace γ] [UniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κγ) (β : Set κ) (h : ∀ (a : κ), 0 f a) (hf : Summable f) :
    ∑' (b : β), f b ∑' (a : κ), f a
    theorem tprod_subtype_le {κ : Type u_4} {γ : Type u_5} [OrderedCommGroup γ] [UniformSpace γ] [UniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κγ) (β : Set κ) (h : ∀ (a : κ), 1 f a) (hf : Multipliable f) :
    ∏' (b : β), f b ∏' (a : κ), f a
    theorem sum_le_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (s : Finset ι) (hs : is, 0 f i) (hf : HasSum f a) :
    is, f i a
    theorem prod_le_hasProd {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (s : Finset ι) (hs : is, 1 f i) (hf : HasProd f a) :
    is, f i a
    theorem isLUB_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (h : ∀ (i : ι), 0 f i) (hf : HasSum f a) :
    IsLUB (Set.range fun (s : Finset ι) => is, f i) a
    theorem isLUB_hasProd {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (h : ∀ (i : ι), 1 f i) (hf : HasProd f a) :
    IsLUB (Set.range fun (s : Finset ι) => is, f i) a
    theorem le_hasSum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) (i : ι) (hb : ∀ (j : ι), j i0 f j) :
    f i a
    theorem le_hasProd {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasProd f a) (i : ι) (hb : ∀ (j : ι), j i1 f j) :
    f i a
    theorem sum_le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (s : Finset ι) (hs : is, 0 f i) (hf : Summable f) :
    is, f i ∑' (i : ι), f i
    theorem prod_le_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (s : Finset ι) (hs : is, 1 f i) (hf : Multipliable f) :
    is, f i ∏' (i : ι), f i
    theorem le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) (i : ι) (hb : ∀ (j : ι), j i0 f j) :
    f i ∑' (i : ι), f i
    theorem le_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Multipliable f) (i : ι) (hb : ∀ (j : ι), j i1 f j) :
    f i ∏' (i : ι), f i
    theorem tsum_le_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) (hf : Summable f) (hg : Summable g) :
    ∑' (i : ι), f i ∑' (i : ι), g i
    theorem tprod_le_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) (hf : Multipliable f) (hg : Multipliable g) :
    ∏' (i : ι), f i ∏' (i : ι), g i
    theorem tsum_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Summable f) (hg : Summable g) (h : f g) :
    ∑' (n : ι), f n ∑' (n : ι), g n
    theorem tprod_mono {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Multipliable f) (hg : Multipliable g) (h : f g) :
    ∏' (n : ι), f n ∏' (n : ι), g n
    theorem tsum_le_of_sum_le {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (hf : Summable f) (h : ∀ (s : Finset ι), is, f i a₂) :
    ∑' (i : ι), f i a₂
    theorem tprod_le_of_prod_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (hf : Multipliable f) (h : ∀ (s : Finset ι), is, f i a₂) :
    ∏' (i : ι), f i a₂
    theorem tsum_le_of_sum_le' {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (ha₂ : 0 a₂) (h : ∀ (s : Finset ι), is, f i a₂) :
    ∑' (i : ι), f i a₂
    theorem tprod_le_of_prod_le' {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a₂ : α} (ha₂ : 1 a₂) (h : ∀ (s : Finset ι), is, f i a₂) :
    ∏' (i : ι), f i a₂
    theorem HasSum.nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), 0 g i) (ha : HasSum g a) :
    0 a
    theorem HasProd.one_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), 1 g i) (ha : HasProd g a) :
    1 a
    theorem HasSum.nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), g i 0) (ha : HasSum g a) :
    a 0
    theorem HasProd.le_one {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} {a : α} (h : ∀ (i : ι), g i 1) (ha : HasProd g a) :
    a 1
    theorem tsum_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} (h : ∀ (i : ι), 0 g i) :
    0 ∑' (i : ι), g i
    theorem one_le_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {g : ια} (h : ∀ (i : ι), 1 g i) :
    1 ∏' (i : ι), g i
    theorem tsum_nonpos {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (h : ∀ (i : ι), f i 0) :
    ∑' (i : ι), f i 0
    theorem tprod_le_one {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (h : ∀ (i : ι), f i 1) :
    ∏' (i : ι), f i 1
    theorem hasSum_zero_iff_of_nonneg {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : ∀ (i : ι), 0 f i) :
    HasSum f 0 f = 0
    theorem hasProd_one_iff_of_one_le {ι : Type u_1} {α : Type u_3} [OrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : ∀ (i : ι), 1 f i) :
    HasProd f 1 f = 1
    theorem hasSum_lt {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} {i : ι} (h : f g) (hi : f i < g i) (hf : HasSum f a₁) (hg : HasSum g a₂) :
    a₁ < a₂
    theorem hasProd_lt {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} {i : ι} (h : f g) (hi : f i < g i) (hf : HasProd f a₁) (hg : HasProd g a₂) :
    a₁ < a₂
    theorem hasSum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) (h : f < g) :
    a₁ < a₂
    abbrev hasSum_strict_mono.match_1 {ι : Type u_1} {α : Type u_2} [OrderedAddCommGroup α] {f : ια} {g : ια} (motive : (f g ∃ (i : ι), f i < g i)Prop) :
    ∀ (x : f g ∃ (i : ι), f i < g i), (∀ (hle : f g) (_i : ι) (hi : f _i < g _i), motive )motive x
    Equations
    • =
    Instances For
      theorem hasProd_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {a₁ : α} {a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) (h : f < g) :
      a₁ < a₂
      theorem tsum_lt_tsum {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {i : ι} (h : f g) (hi : f i < g i) (hf : Summable f) (hg : Summable g) :
      ∑' (n : ι), f n < ∑' (n : ι), g n
      theorem tprod_lt_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {f : ια} {g : ια} {i : ι} (h : f g) (hi : f i < g i) (hf : Multipliable f) (hg : Multipliable g) :
      ∏' (n : ι), f n < ∏' (n : ι), g n
      theorem tsum_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Summable f) (hg : Summable g) (h : f < g) :
      ∑' (n : ι), f n < ∑' (n : ι), g n
      theorem tprod_strict_mono {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {f : ια} {g : ια} (hf : Multipliable f) (hg : Multipliable g) (h : f < g) :
      ∏' (n : ι), f n < ∏' (n : ι), g n
      theorem tsum_pos {ι : Type u_1} {α : Type u_3} [OrderedAddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [OrderClosedTopology α] {g : ια} (hsum : Summable g) (hg : ∀ (i : ι), 0 g i) (i : ι) (hi : 0 < g i) :
      0 < ∑' (i : ι), g i
      theorem one_lt_tprod {ι : Type u_1} {α : Type u_3} [OrderedCommGroup α] [TopologicalSpace α] [TopologicalGroup α] [OrderClosedTopology α] {g : ια} (hsum : Multipliable g) (hg : ∀ (i : ι), 1 g i) (i : ι) (hi : 1 < g i) :
      1 < ∏' (i : ι), g i
      theorem le_hasSum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) (i : ι) :
      f i a
      theorem le_hasProd' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasProd f a) (i : ι) :
      f i a
      theorem le_tsum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) (i : ι) :
      f i ∑' (i : ι), f i
      theorem le_tprod' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Multipliable f) (i : ι) :
      f i ∏' (i : ι), f i
      theorem hasSum_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} :
      HasSum f 0 ∀ (x : ι), f x = 0
      theorem hasProd_one_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} :
      HasProd f 1 ∀ (x : ι), f x = 1
      theorem tsum_eq_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) :
      ∑' (i : ι), f i = 0 ∀ (x : ι), f x = 0
      theorem tprod_eq_one_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Multipliable f) :
      ∏' (i : ι), f i = 1 ∀ (x : ι), f x = 1
      theorem tsum_ne_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Summable f) :
      ∑' (i : ι), f i 0 ∃ (x : ι), f x 0
      theorem tprod_ne_one_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} (hf : Multipliable f) :
      ∏' (i : ι), f i 1 ∃ (x : ι), f x 1
      theorem isLUB_hasSum' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasSum f a) :
      IsLUB (Set.range fun (s : Finset ι) => is, f i) a
      theorem isLUB_hasProd' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedCommMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ια} {a : α} (hf : HasProd f a) :
      IsLUB (Set.range fun (s : Finset ι) => is, f i) a

      For infinite sums taking values in a linearly ordered monoid, the existence of a least upper bound for the finite sums is a criterion for summability.

      This criterion is useful when applied in a linearly ordered monoid which is also a complete or conditionally complete linear order, such as , ℝ≥0, ℝ≥0∞, because it is then easy to check the existence of a least upper bound.

      theorem hasSum_of_isLUB_of_nonneg {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (i : α) (h : ∀ (i : ι), 0 f i) (hf : IsLUB (Set.range fun (s : Finset ι) => is, f i) i) :
      HasSum f i
      theorem hasProd_of_isLUB_of_one_le {ι : Type u_1} {α : Type u_3} [LinearOrderedCommMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (i : α) (h : ∀ (i : ι), 1 f i) (hf : IsLUB (Set.range fun (s : Finset ι) => is, f i) i) :
      theorem hasSum_of_isLUB {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedAddCommMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => is, f i) b) :
      HasSum f b
      theorem hasProd_of_isLUB {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedCommMonoid α] [TopologicalSpace α] [OrderTopology α] {f : ια} (b : α) (hf : IsLUB (Set.range fun (s : Finset ι) => is, f i) b) :
      theorem summable_abs_iff {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
      (Summable fun (x : ι) => |f x|) Summable f
      theorem multipliable_mabs_iff {ι : Type u_1} {α : Type u_3} [LinearOrderedCommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] {f : ια} :
      (Multipliable fun (x : ι) => mabs (f x)) Multipliable f
      theorem Summable.of_abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
      (Summable fun (x : ι) => |f x|)Summable f

      Alias of the forward direction of summable_abs_iff.

      theorem Summable.abs {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ια} :
      Summable fSummable fun (x : ι) => |f x|

      Alias of the reverse direction of summable_abs_iff.

      theorem Finite.of_summable_const {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun (x : ι) => b) :
      theorem Set.Finite.of_summable_const {ι : Type u_1} {α : Type u_3} [LinearOrderedAddCommGroup α] [TopologicalSpace α] [Archimedean α] [OrderClosedTopology α] {b : α} (hb : 0 < b) (hf : Summable fun (x : ι) => b) :
      Set.univ.Finite
      theorem Summable.tendsto_atTop_of_pos {α : Type u_3} [LinearOrderedField α] [TopologicalSpace α] [OrderTopology α] {f : α} (hf : Summable f⁻¹) (hf' : ∀ (n : ), 0 < f n) :
      Filter.Tendsto f Filter.atTop Filter.atTop