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) :
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) :
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) :
@[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) :
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) :
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) :
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) :
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) :
@[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₂} :
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} :
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₂) :
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₂} :
@[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₂) :