Infinite sums in topological vector spaces #
theorem
HasSum.smul_const
{ι : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
[ContinuousSMul R M]
{f : ι → R}
{r : R}
(hf : HasSum f r)
(a : M)
:
theorem
Summable.smul_const
{ι : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
[ContinuousSMul 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]
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
[ContinuousSMul R M]
{f : ι → R}
[T2Space M]
(hf : Summable f)
(a : M)
:
theorem
ContinuousLinearMap.hasSum
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
{x : M}
(hf : HasSum f x)
:
HasSum (fun b => ↑φ (f b)) (↑φ x)
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
HasSum.mapL
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
{x : M}
(hf : HasSum f x)
:
HasSum (fun b => ↑φ (f b)) (↑φ x)
Alias of ContinuousLinearMap.hasSum.
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
ContinuousLinearMap.summable
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : Summable f)
:
Summable fun 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₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : Summable f)
:
Summable fun b => ↑φ (f b)
Alias of ContinuousLinearMap.summable.
theorem
ContinuousLinearMap.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₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
[T2Space M₂]
{f : ι → M}
(φ : M →SL[σ] M₂)
(hf : Summable f)
:
↑φ (∑' (z : ι), f z) = ∑' (z : ι), ↑φ (f z)
theorem
ContinuousLinearEquiv.hasSum
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
{f : ι → M}
(e : M ≃SL[σ] M₂)
{y : M₂}
:
HasSum (fun b => ↑e (f b)) y ↔ HasSum f (↑(ContinuousLinearEquiv.symm e) y)
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
ContinuousLinearEquiv.hasSum'
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
{f : ι → M}
(e : M ≃SL[σ] M₂)
{x : M}
:
Applying a continuous linear map commutes with taking an (infinite) sum.
theorem
ContinuousLinearEquiv.summable
{ι : Type u_1}
{R : Type u_2}
{R₂ : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
{f : ι → M}
(e : M ≃SL[σ] M₂)
:
theorem
ContinuousLinearEquiv.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₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
[T2Space M]
[T2Space M₂]
{f : ι → M}
(e : M ≃SL[σ] M₂)
{y : M₂}
:
∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
theorem
ContinuousLinearEquiv.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₂]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R₂ M₂]
[TopologicalSpace M]
[TopologicalSpace M₂]
{σ : R →+* R₂}
{σ' : R₂ →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
[T2Space M]
[T2Space M₂]
{f : ι → M}
(e : M ≃SL[σ] M₂)
:
↑e (∑' (z : ι), f z) = ∑' (z : ι), ↑e (f z)