# Infinite sums in topological vector spaces #

theorem HasSum.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βα} {a : α} (b : γ) (hf : HasSum f a) :
HasSum (fun (i : β) => b f i) (b a)
theorem Summable.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βα} (b : γ) (hf : ) :
Summable fun (i : β) => b f i
theorem tsum_const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βα} [] (b : γ) (hf : ) :
∑' (i : β), b f i = b ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a Monoid, but requiring a summability hypothesis.

theorem tsum_const_smul' {α : Type u_1} {β : Type u_2} [] [] {f : βα} {γ : Type u_5} [] [] [] [] (g : γ) :
∑' (i : β), g f i = g ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a Group, but not requiring any summability hypothesis.

theorem tsum_const_smul'' {α : Type u_1} {β : Type u_2} [] [] {f : βα} {γ : Type u_5} [] [Module γ α] [] [] (g : γ) :
∑' (i : β), g f i = g ∑' (i : β), f i

Infinite sums commute with scalar multiplication. Version for scalars living in a DivisionRing; no summability hypothesis. This could be made to work for a [GroupWithZero γ] if there was such a thing as DistribMulActionWithZero.

theorem HasSum.smul_const {ι : Type u_5} {R : Type u_7} {M : Type u_9} [] [] [] [] [Module R M] [] {f : ιR} {r : R} (hf : HasSum f r) (a : M) :
HasSum (fun (z : ι) => f z a) (r a)
theorem Summable.smul_const {ι : Type u_5} {R : Type u_7} {M : Type u_9} [] [] [] [] [Module R M] [] {f : ιR} (hf : ) (a : M) :
Summable fun (z : ι) => f z a
theorem tsum_smul_const {ι : Type u_5} {R : Type u_7} {M : Type u_9} [] [] [] [] [Module R M] [] {f : ιR} [] (hf : ) (a : M) :
∑' (z : ι), f z a = (∑' (z : ι), f z) a

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_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [] [] [Module 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) :
s t = u
theorem HasSum.smul {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [] [] [Module 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) :
HasSum (fun (x : ι × κ) => f x.1 g x.2) (s t)
theorem tsum_smul_tsum {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [] [] [Module R M] [] [] [] [] [] {f : ιR} {g : κM} (hf : ) (hg : ) (hfg : Summable fun (x : ι × κ) => f x.1 g x.2) :
(∑' (x : ι), f x) ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 g z.2

Scalar product of two infinites sums indexed by arbitrary types.

theorem ContinuousLinearMap.hasSum {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ 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_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ 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_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {f : ιM} (φ : M →SL[σ] M₂) (hf : ) :
Summable fun (b : ι) => φ (f b)
theorem Summable.mapL {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {f : ιM} (φ : M →SL[σ] M₂) (hf : ) :
Summable fun (b : ι) => φ (f b)

Alias of ContinuousLinearMap.summable.

theorem ContinuousLinearMap.map_tsum {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} [T2Space M₂] {f : ιM} (φ : M →SL[σ] M₂) (hf : ) :
φ (∑' (z : ι), f z) = ∑' (z : ι), φ (f z)
theorem ContinuousLinearEquiv.hasSum {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {σ' : R₂ →+* R} [] [] {f : ιM} (e : M ≃SL[σ] M₂) {y : M₂} :
HasSum (fun (b : ι) => e (f b)) y HasSum f (e.symm y)

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

theorem ContinuousLinearEquiv.hasSum' {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {σ' : R₂ →+* R} [] [] {f : ιM} (e : M ≃SL[σ] M₂) {x : M} :
HasSum (fun (b : ι) => e (f b)) (e x) HasSum f x

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

theorem ContinuousLinearEquiv.summable {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {σ' : R₂ →+* R} [] [] {f : ιM} (e : M ≃SL[σ] M₂) :
(Summable fun (b : ι) => e (f b))
theorem ContinuousLinearEquiv.tsum_eq_iff {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {σ' : R₂ →+* R} [] [] [] [T2Space M₂] {f : ιM} (e : M ≃SL[σ] M₂) {y : M₂} :
∑' (z : ι), e (f z) = y ∑' (z : ι), f z = e.symm y
theorem ContinuousLinearEquiv.map_tsum {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [] [Semiring R₂] [] [Module R M] [] [Module R₂ M₂] [] [] {σ : R →+* R₂} {σ' : R₂ →+* R} [] [] [] [T2Space M₂] {f : ιM} (e : M ≃SL[σ] M₂) :
e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)
abbrev AddAction.automorphize.match_1 {α : Type u_2} {β : Type u_1} [] [] (b₁ : β) (b₂ : β) (motive : b₁ b₂Prop) :
∀ (h : b₁ b₂), (∀ (a : α) (ha : a +ᵥ b₂ = b₁), motive )motive h
Equations
• =
Instances For
noncomputable def AddAction.automorphize {α : Type u_1} {β : Type u_2} {M : Type u_11} [] [] [] [] (f : βM) :
M

Given an additive group α acting on a type β, and a function f : β → M, we automorphize f to a function β ⧸ α → M by summing over α orbits, b ↦ ∑' (a : α), f(a • b).

Equations
Instances For
theorem AddAction.automorphize.proof_1 {α : Type u_2} {β : Type u_1} {M : Type u_3} [] [] [] [] (f : βM) (b₁ : β) (b₂ : β) :
b₁ b₂(fun (b : β) => ∑' (a : α), f (a +ᵥ b)) b₁ = (fun (b : β) => ∑' (a : α), f (a +ᵥ b)) b₂
noncomputable def MulAction.automorphize {α : Type u_1} {β : Type u_2} {M : Type u_11} [] [] [] [] (f : βM) :
M

Given a group α acting on a type β, and a function f : β → M, we "automorphize" f to a function β ⧸ α → M by summing over α orbits, b ↦ ∑' (a : α), f(a • b).

Equations
Instances For
theorem MulAction.automorphize_smul_left {α : Type u_1} {β : Type u_2} {M : Type u_11} [] [] [] {R : Type u_12} [] [Module R M] [] [] [] (f : βM) (g : R) :
MulAction.automorphize (g Quotient.mk' f) =

Automorphization of a function into an R-Module distributes, that is, commutes with the R-scalar multiplication.

theorem AddAction.automorphize_smul_left {α : Type u_1} {β : Type u_2} {M : Type u_11} [] [] [] {R : Type u_12} [] [Module R M] [] [] [] (f : βM) (g : R) :
AddAction.automorphize (g Quotient.mk' f) =

Automorphization of a function into an R-Module distributes, that is, commutes with the R-scalar multiplication.

noncomputable def QuotientAddGroup.automorphize {M : Type u_11} [] [] {G : Type u_13} [] {Γ : } (f : GM) :
G ΓM

Given a subgroup Γ of an additive group G, and a function f : G → M, we automorphize f to a function G ⧸ Γ → M by summing over Γ orbits, g ↦ ∑' (γ : Γ), f(γ • g).

Equations
Instances For
noncomputable def QuotientGroup.automorphize {M : Type u_11} [] [] {G : Type u_13} [] {Γ : } (f : GM) :
G ΓM

Given a subgroup Γ of a group G, and a function f : G → M, we "automorphize" f to a function G ⧸ Γ → M by summing over Γ orbits, g ↦ ∑' (γ : Γ), f(γ • g).

Equations
Instances For
theorem QuotientGroup.automorphize_smul_left {M : Type u_11} [] [] [] {R : Type u_12} [] [Module R M] [] {G : Type u_13} [] {Γ : } (f : GM) (g : G ΓR) :
QuotientGroup.automorphize (g Quotient.mk' f) =

Automorphization of a function into an R-Module distributes, that is, commutes with the R-scalar multiplication.

theorem QuotientAddGroup.automorphize_smul_left {M : Type u_11} [] [] [] {R : Type u_12} [] [Module R M] [] {G : Type u_13} [] {Γ : } (f : GM) (g : G ΓR) :

Automorphization of a function into an R-Module distributes, that is, commutes with the R-scalar multiplication.