mathlib3 documentation

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] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] {f : ι R} {r : R} (hf : has_sum f 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] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R 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] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) {x : M} (hf : has_sum f 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {f : ι M} (φ : M →SL[σ] M₂) {x : M} (hf : has_sum f 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {f : ι M} (e : M ≃SL[σ] M₂) {y : M₂} :
has_sum (λ (b : ι), e (f b)) y has_sum f ((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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {f : ι M} (e : M ≃SL[σ] M₂) {x : M} :
has_sum (λ (b : ι), e (f b)) (e x) has_sum f 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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {f : ι M} (e : M ≃SL[σ] M₂) :
summable (λ (b : ι), e (f b)) summable f
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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] [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₂] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [module R₂ M₂] [topological_space M] [topological_space M₂] {σ : R →+* R₂} {σ' : R₂ →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] [t2_space M] [t2_space M₂] {f : ι M} (e : M ≃SL[σ] M₂) :
e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)