# mathlib3documentation

topology.algebra.infinite_sum.module

# Infinite sums in topological vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem has_sum.smul_const {ι : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [ M] [ M] {f : ι R} {r : R} (hf : r) (a : M) :
has_sum (λ (z : ι), f z a) (r a)
theorem summable.smul_const {ι : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [ M] [ M] {f : ι R} (hf : summable f) (a : M) :
summable (λ (z : ι), f z a)
theorem tsum_smul_const {ι : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [ M] [ M] {f : ι R} [t2_space M] (hf : summable f) (a : M) :
∑' (z : ι), f z a = (∑' (z : ι), f z) a
@[protected]
theorem continuous_linear_map.has_sum {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) {x : M} (hf : x) :
has_sum (λ (b : ι), φ (f b)) (φ x)

Applying a continuous linear map commutes with taking an (infinite) sum.

theorem has_sum.mapL {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) {x : M} (hf : x) :
has_sum (λ (b : ι), φ (f b)) (φ x)

Alias of continuous_linear_map.has_sum.

@[protected]
theorem continuous_linear_map.summable {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) (hf : summable f) :
summable (λ (b : ι), φ (f b))
theorem summable.mapL {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) (hf : summable f) :
summable (λ (b : ι), φ (f b))

Alias of continuous_linear_map.summable.

@[protected]
theorem continuous_linear_map.map_tsum {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} [t2_space M₂] {f : ι M} (φ : M →SL[σ] M₂) (hf : summable f) :
φ (∑' (z : ι), f z) = ∑' (z : ι), φ (f z)
@[protected]
theorem continuous_linear_equiv.has_sum {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ σ'] [ σ] {f : ι M} (e : M ≃SL[σ] M₂) {y : M₂} :
has_sum (λ (b : ι), e (f b)) y ((e.symm) y)

Applying a continuous linear map commutes with taking an (infinite) sum.

@[protected]
theorem continuous_linear_equiv.has_sum' {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ σ'] [ σ] {f : ι M} (e : M ≃SL[σ] M₂) {x : M} :
has_sum (λ (b : ι), e (f b)) (e x) x

Applying a continuous linear map commutes with taking an (infinite) sum.

@[protected]
theorem continuous_linear_equiv.summable {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ σ'] [ σ] {f : ι M} (e : M ≃SL[σ] M₂) :
summable (λ (b : ι), e (f b))
theorem continuous_linear_equiv.tsum_eq_iff {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ σ'] [ σ] [t2_space M] [t2_space M₂] {f : ι M} (e : M ≃SL[σ] M₂) {y : M₂} :
∑' (z : ι), e (f z) = y ∑' (z : ι), f z = (e.symm) y
@[protected]
theorem continuous_linear_equiv.map_tsum {ι : Type u_1} {R : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [ M] [add_comm_monoid M₂] [module R₂ M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ σ'] [ σ] [t2_space M] [t2_space M₂] {f : ι M} (e : M ≃SL[σ] M₂) :
e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)