Infinite sums in topological vector spaces #
theorem
HasSum.smul_const
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[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_3}
{M : Type u_5}
[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_3}
{M : Type u_5}
[Semiring R]
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
[ContinuousSMul R M]
{f : ι → R}
[T2Space M]
(hf : Summable f)
(a : M)
:
Note we cannot derive the mul lemmas from these smul lemmas, as the mul versions do not
require associativity, but Module does.
theorem
HasSum.smul_eq
{ι : Type u_1}
{κ : Type u_2}
{R : Type u_3}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace R]
[TopologicalSpace M]
[T3Space M]
[ContinuousAdd M]
[ContinuousSMul R M]
{f : ι → R}
{g : κ → M}
{s : R}
{t : M}
{u : M}
(hf : HasSum f s)
(hg : HasSum g t)
(hfg : HasSum (fun (x : ι × κ) => f x.1 • g x.2) u)
:
theorem
HasSum.smul
{ι : Type u_1}
{κ : Type u_2}
{R : Type u_3}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace R]
[TopologicalSpace M]
[T3Space M]
[ContinuousAdd M]
[ContinuousSMul R M]
{f : ι → R}
{g : κ → M}
{s : R}
{t : M}
(hf : HasSum f s)
(hg : HasSum g t)
(hfg : Summable fun (x : ι × κ) => f x.1 • g x.2)
:
theorem
tsum_smul_tsum
{ι : Type u_1}
{κ : Type u_2}
{R : Type u_3}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace R]
[TopologicalSpace M]
[T3Space M]
[ContinuousAdd M]
[ContinuousSMul R M]
{f : ι → R}
{g : κ → M}
(hf : Summable f)
(hg : Summable g)
(hfg : Summable fun (x : ι × κ) => f x.1 • g x.2)
:
Scalar product of two infinites sums indexed by arbitrary types.
theorem
ContinuousLinearMap.hasSum
{ι : Type u_1}
{R : Type u_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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_3}
{R₂ : Type u_4}
{M : Type u_5}
{M₂ : Type u_6}
[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)