Infinite sum over a topological monoid
This sum is known as unconditionally convergent, as it sums to the same value under all possible permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.
Note: There are summable sequences which are not unconditionally convergent! The other way holds
generally, see has_sum.tendsto_sum_nat.
References
- Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
def
has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
(β → α) → α → Prop
Infinite sum on a topological monoid
The at_top filter on finset α is the limit of all finite sets towards the entire type. So we sum
up bigger and bigger sets. This sum operation is still invariant under reordering, and a absolute
sum operator.
This is based on Mario Carneiro's infinite sum in Metamath.
For the definition or many statements, α does not need to be a topological monoid. We only add this assumption later, for the lemmas where it is relevant.
Equations
- has_sum f a = filter.tendsto (λ (s : finset β), s.sum (λ (b : β), f b)) filter.at_top (nhds a)
def
summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
(β → α) → Prop
summable f means that f has some (infinite) sum. Use tsum to get the value.
∑' i, f i is the sum of f it exists, or 0 otherwise
theorem
summable.has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α} :
theorem
has_sum.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α} :
theorem
has_sum_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
has_sum (λ (b : β), 0) 0
Constant zero function has sum 0
theorem
summable_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α] :
summable (λ (b : β), 0)
theorem
tsum_eq_zero_of_not_summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α} :
theorem
has_sum.has_sum_of_sum_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α} :
theorem
has_sum_iff_has_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α} :
(∀ (u : finset γ), ∃ (v : finset β), ∀ (v' : finset β), v ⊆ v' → (∃ (u' : finset γ), u ⊆ u' ∧ u'.sum (λ (x : γ), g x) = v'.sum (λ (b : β), f b))) → (∀ (v : finset β), ∃ (u : finset γ), ∀ (u' : finset γ), u ⊆ u' → (∃ (v' : finset β), v ⊆ v' ∧ v'.sum (λ (b : β), f b) = u'.sum (λ (x : γ), g x))) → (has_sum f a ↔ has_sum g a)
theorem
function.injective.has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → β} :
theorem
function.injective.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{g : γ → β} :
theorem
has_sum_subtype_iff_of_support_subset
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{s : set β} :
theorem
has_sum_subtype_iff_indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{s : set β} :
@[simp]
theorem
has_sum_subtype_support
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α} :
theorem
has_sum_fintype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[fintype β]
(f : β → α) :
has_sum f (finset.univ.sum (λ (b : β), f b))
theorem
finset.has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(s : finset β)
(f : β → α) :
theorem
finset.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(s : finset β)
(f : β → α) :
theorem
set.finite.summable
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{s : set β}
(hs : s.finite)
(f : β → α) :
theorem
has_sum_sum_of_ne_finset_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{s : finset β} :
If a function f vanishes outside of a finite set s, then it has_sum ∑ b in s, f b.
theorem
summable_of_ne_finset_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{s : finset β} :
theorem
has_sum_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(b : β) :
theorem
has_sum_ite_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
(b : β)
(a : α) :
theorem
equiv.has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
(e : γ ≃ β) :
theorem
equiv.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
(e : γ ≃ β) :
theorem
summable.prod_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β × γ → α} :
theorem
equiv.has_sum_iff_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g)) :
theorem
has_sum_iff_has_sum_of_ne_zero_bij
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
{g : γ → α}
(i : ↥(function.support g) → β) :
theorem
equiv.summable_iff_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g)) :
theorem
has_sum.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a : α}
[add_comm_monoid γ]
[topological_space γ]
(hf : has_sum f a)
(g : α →+ γ) :
theorem
has_sum.tendsto_sum_nat
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
{a : α}
{f : ℕ → α} :
has_sum f a → filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds a)
If f : ℕ → α has sum a, then the partial sums ∑_{i=0}^{n-1} f i converge to a.
theorem
has_sum.unique
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a₁ a₂ : α}
[t2_space α] :
theorem
summable.has_sum_iff_tendsto_nat
{α : Type u_1}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : ℕ → α}
{a : α} :
summable f → (has_sum f a ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds a))
theorem
equiv.summable_iff_of_has_sum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
{α' : Type u_4}
[add_comm_monoid α']
[topological_space α']
(e : α' ≃ α)
{f : β → α}
{g : γ → α'} :
theorem
has_sum.add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
{a b : α}
[has_continuous_add α] :
theorem
summable.add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f g : β → α}
[has_continuous_add α] :
theorem
has_sum_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{f : γ → β → α}
{a : γ → α}
{s : finset γ} :
theorem
summable_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
{f : γ → β → α}
{s : finset γ} :
theorem
has_sum.add_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s : set β} :
theorem
summable.add_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[has_continuous_add α]
{s : set β} :
theorem
has_sum.compl_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
{a b : α}
[has_continuous_add α]
{s : set β} :
theorem
summable.compl_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
{f : β → α}
[has_continuous_add α]
{s : set β} :
theorem
has_sum.sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
{g : β → α}
{a : α} :
theorem
has_sum.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{f : β × γ → α}
{g : β → α}
{a : α} :
If a series f on β × γ has sum a and for each b the restriction of f to {b} × γ
has sum g b, then the series g has sum a.
theorem
summable.sigma'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α} :
theorem
has_sum.sigma_of_has_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
{g : β → α}
{a : α} :
theorem
has_sum.tsum_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{a : α} :
theorem
summable.has_sum_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{a : α} :
@[simp]
theorem
tsum_zero
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α] :
(∑' (b : β), 0) = 0
theorem
tsum_eq_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{s : finset β} :
theorem
tsum_fintype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[fintype β]
(f : β → α) :
(∑' (b : β), f b) = finset.univ.sum (λ (b : β), f b)
@[simp]
theorem
finset.tsum_subtype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(s : finset β)
(f : β → α) :
theorem
tsum_eq_single
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
(b : β) :
@[simp]
theorem
tsum_ite_eq
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(b : β)
(a : α) :
theorem
equiv.tsum_eq_tsum_of_has_sum_iff_has_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{α' : Type u_4}
[add_comm_monoid α']
[topological_space α']
(e : α' ≃ α)
(h0 : ⇑e 0 = 0)
{f : β → α}
{g : γ → α'} :
theorem
tsum_eq_tsum_of_has_sum_iff_has_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{g : γ → α} :
theorem
equiv.tsum_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(j : γ ≃ β)
(f : β → α) :
theorem
equiv.tsum_eq_tsum_of_support
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{g : γ → α}
(e : ↥(function.support f) ≃ ↥(function.support g)) :
theorem
tsum_eq_tsum_of_ne_zero_bij
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f : β → α}
{g : γ → α}
(i : ↥(function.support g) → β) :
(∀ ⦃x y : ↥(function.support g)⦄, i x = i y → ↑x = ↑y) → function.support f ⊆ set.range i → (∀ (x : ↥(function.support g)), f (i x) = g ↑x) → ((∑' (x : β), f x) = ∑' (y : γ), g y)
theorem
tsum_subtype
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
(s : set β)
(f : β → α) :
theorem
tsum_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
{f g : β → α}
[has_continuous_add α] :
theorem
tsum_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[has_continuous_add α]
{f : γ → β → α}
{s : finset γ} :
theorem
tsum_sigma'
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[has_continuous_add α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α} :
theorem
tsum_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[has_continuous_add α]
[regular_space α]
{f : β × γ → α} :
theorem
tsum_comm'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[has_continuous_add α]
[regular_space α]
{f : β → γ → α} :
summable (function.uncurry f) → (∀ (b : β), summable (f b)) → (∀ (c : γ), summable (λ (b : β), f b c)) → ((∑' (c : γ) (b : β), f b c) = ∑' (b : β) (c : γ), f b c)
theorem
tsum_supr_decode2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[encodable γ]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(s : γ → β) :
(∑' (i : ℕ), m (⨆ (b : γ) (H : b ∈ encodable.decode2 γ i), s b)) = ∑' (b : γ), m (s b)
You can compute a sum over an encodably type by summing over the natural numbers and taking a supremum. This is useful for outer measures.
theorem
tsum_Union_decode2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[encodable γ]
(m : set β → α)
(m0 : m ∅ = 0)
(s : γ → set β) :
(∑' (i : ℕ), m (⋃ (b : γ) (H : b ∈ encodable.decode2 γ i), s b)) = ∑' (b : γ), m (s b)
tsum_supr_decode2 specialized to the complete lattice of sets.
Some properties about measure-like functions.
These could also be functions defined on complete sublattices of sets, with the property
that they are countably sub-additive.
R will probably be instantiated with (≤) in all applications.
theorem
rel_supr_tsum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[encodable γ]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s : γ → β) :
R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))
If a function is countably sub-additive then it is sub-additive on encodable types
theorem
rel_supr_sum
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s : δ → β)
(t : finset δ) :
If a function is countably sub-additive then it is sub-additive on finite sets
theorem
rel_sup_add
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid α]
[topological_space α]
[t2_space α]
[complete_lattice β]
(m : β → α)
(m0 : m ⊥ = 0)
(R : α → α → Prop)
(m_supr : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i)))
(s₁ s₂ : β) :
If a function is countably sub-additive then it is binary sub-additive
theorem
has_sum.neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α} :
theorem
summable.neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α} :
theorem
has_sum.sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
{a₁ a₂ : α} :
theorem
summable.sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α} :
theorem
has_sum.has_sum_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a₁ a₂ : α}
{s : set β} :
theorem
has_sum.has_sum_iff_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a₁ a₂ : α}
{s : set β} :
theorem
summable.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{s : set β} :
theorem
finset.has_sum_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
(s : finset β) :
theorem
finset.has_sum_iff_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{a : α}
(s : finset β) :
theorem
finset.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
(s : finset β) :
theorem
set.finite.summable_compl_iff
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
{s : set β} :
theorem
tsum_neg
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
[t2_space α] :
theorem
tsum_sub
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f g : β → α}
[t2_space α] :
theorem
tsum_add_tsum_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
[t2_space α]
{s : set β} :
theorem
sum_add_tsum_compl
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : β → α}
[t2_space α]
{s : finset β} :
Sums on subtypes
If s is a finset of α, we show that the summability of f in the whole space and on the subtype
univ - s are equivalent, and relate their sums. For a function defined on ℕ, we deduce the
formula (∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f i), in sum_add_tsum_nat_add.
theorem
has_sum_nat_add_iff
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ)
{a : α} :
theorem
summable_nat_add_iff
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ) :
theorem
has_sum_nat_add_iff'
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
{f : ℕ → α}
(k : ℕ)
{a : α} :
theorem
sum_add_tsum_nat_add
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
[t2_space α]
{f : ℕ → α}
(k : ℕ) :
theorem
tsum_eq_zero_add
{α : Type u_1}
[add_comm_group α]
[topological_space α]
[topological_add_group α]
[t2_space α]
{f : ℕ → α} :
theorem
has_sum.mul_left
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a₁ : α}
(a₂ : α) :
theorem
has_sum.mul_right
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a₁ : α}
(a₂ : α) :
theorem
summable.mul_left
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
(a : α) :
theorem
summable.mul_right
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
(a : α) :
theorem
tsum_mul_left
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
[t2_space α]
(a : α) :
theorem
tsum_mul_right
{α : Type u_1}
{β : Type u_2}
[semiring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
[t2_space α]
(a : α) :
theorem
has_sum_mul_left_iff
{α : Type u_1}
{β : Type u_2}
[division_ring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a₁ a₂ : α} :
theorem
has_sum_mul_right_iff
{α : Type u_1}
{β : Type u_2}
[division_ring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a₁ a₂ : α} :
theorem
summable_mul_left_iff
{α : Type u_1}
{β : Type u_2}
[division_ring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a : α} :
theorem
summable_mul_right_iff
{α : Type u_1}
{β : Type u_2}
[division_ring α]
[topological_space α]
[topological_semiring α]
{f : β → α}
{a : α} :
theorem
has_sum_le
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f g : β → α}
{a₁ a₂ : α} :
theorem
has_sum_le_inj
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : β → α}
{a₁ a₂ : α}
{g : γ → α}
(i : β → γ) :
theorem
tsum_le_tsum_of_inj
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : β → α}
{g : γ → α}
(i : β → γ) :
theorem
sum_le_has_sum
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{a : α}
{f : β → α}
(s : finset β) :
theorem
sum_le_tsum
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : β → α}
(s : finset β) :
theorem
tsum_le_tsum
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f g : β → α} :
theorem
tsum_nonneg
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{g : β → α} :
theorem
tsum_nonpos
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[topological_space α]
[order_closed_topology α]
{f : β → α} :
theorem
summable_iff_cauchy_seq_finset
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[complete_space α] :
summable f ↔ cauchy_seq (λ (s : finset β), s.sum (λ (b : β), f b))
theorem
cauchy_seq_finset_iff_vanishing
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[uniform_add_group α] :
theorem
summable_iff_vanishing
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[uniform_add_group α]
[complete_space α] :
theorem
summable.summable_of_eq_zero_or_self
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f g : β → α}
[uniform_add_group α]
[complete_space α] :
theorem
summable.indicator
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[uniform_add_group α]
[complete_space α]
(hf : summable f)
(s : set β) :
theorem
summable.comp_injective
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[uniform_add_group α]
[complete_space α]
{i : γ → β} :
summable f → function.injective i → summable (f ∘ i)
theorem
summable.subtype
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
{f : β → α}
[uniform_add_group α]
[complete_space α]
(hf : summable f)
(s : set β) :
theorem
summable.sigma_factor
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α}
(ha : summable f)
(b : β) :
theorem
summable.sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α} :
theorem
summable.prod_factor
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
{f : β × γ → α}
(h : summable f)
(b : β) :
summable (λ (c : γ), f (b, c))
theorem
tsum_sigma
{α : Type u_1}
{β : Type u_2}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[regular_space α]
{γ : β → Type u_3}
{f : (Σ (b : β), γ b) → α} :
theorem
tsum_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[regular_space α]
{f : β × γ → α} :
theorem
tsum_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group α]
[uniform_space α]
[uniform_add_group α]
[complete_space α]
[regular_space α]
{f : β → γ → α} :
summable (function.uncurry f) → ((∑' (c : γ) (b : β), f b c) = ∑' (b : β) (c : γ), f b c)
theorem
cauchy_seq_of_edist_le_of_summable
{α : Type u_1}
[emetric_space α]
{f : ℕ → α}
(d : ℕ → nnreal) :
(∀ (n : ℕ), has_edist.edist (f n) (f n.succ) ≤ ↑(d n)) → summable d → cauchy_seq f
If the extended distance between consequent points of a sequence is estimated
by a summable series of nnreals, then the original sequence is a Cauchy sequence.
theorem
cauchy_seq_of_dist_le_of_summable
{α : Type u_1}
[metric_space α]
{f : ℕ → α}
(d : ℕ → ℝ) :
(∀ (n : ℕ), has_dist.dist (f n) (f n.succ) ≤ d n) → summable d → cauchy_seq f
If the distance between consequent points of a sequence is estimated by a summable series, then the original sequence is a Cauchy sequence.
theorem
cauchy_seq_of_summable_dist
{α : Type u_1}
[metric_space α]
{f : ℕ → α} :
summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ)) → cauchy_seq f
theorem
dist_le_tsum_of_dist_le_of_tendsto
{α : Type u_1}
[metric_space α]
{f : ℕ → α}
(d : ℕ → ℝ)
(hf : ∀ (n : ℕ), has_dist.dist (f n) (f n.succ) ≤ d n)
(hd : summable d)
{a : α}
(ha : filter.tendsto f filter.at_top (nhds a))
(n : ℕ) :
has_dist.dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
theorem
dist_le_tsum_of_dist_le_of_tendsto₀
{α : Type u_1}
[metric_space α]
{f : ℕ → α}
(d : ℕ → ℝ)
(hf : ∀ (n : ℕ), has_dist.dist (f n) (f n.succ) ≤ d n)
(hd : summable d)
{a : α} :
filter.tendsto f filter.at_top (nhds a) → has_dist.dist (f 0) a ≤ tsum d
theorem
dist_le_tsum_dist_of_tendsto
{α : Type u_1}
[metric_space α]
{f : ℕ → α}
(h : summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ)))
{a : α}
(ha : filter.tendsto f filter.at_top (nhds a))
(n : ℕ) :
has_dist.dist (f n) a ≤ ∑' (m : ℕ), has_dist.dist (f (n + m)) (f (n + m).succ)
theorem
dist_le_tsum_dist_of_tendsto₀
{α : Type u_1}
[metric_space α]
{f : ℕ → α}
(h : summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ)))
{a : α} :
filter.tendsto f filter.at_top (nhds a) → (has_dist.dist (f 0) a ≤ ∑' (n : ℕ), has_dist.dist (f n) (f n.succ))