Infinite sums in topological vector spaces #
theorem
HasSum.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Monoid γ]
[TopologicalSpace α]
[AddCommMonoid α]
[DistribMulAction γ α]
[ContinuousConstSMul γ α]
{f : β → α}
{a : α}
(b : γ)
(hf : HasSum f a)
:
theorem
Summable.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Monoid γ]
[TopologicalSpace α]
[AddCommMonoid α]
[DistribMulAction γ α]
[ContinuousConstSMul γ α]
{f : β → α}
(b : γ)
(hf : Summable f)
:
theorem
tsum_const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Monoid γ]
[TopologicalSpace α]
[AddCommMonoid α]
[DistribMulAction γ α]
[ContinuousConstSMul γ α]
{f : β → α}
[T2Space α]
(b : γ)
(hf : Summable f)
:
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}
[TopologicalSpace α]
[AddCommMonoid α]
{f : β → α}
{γ : Type u_5}
[Group γ]
[DistribMulAction γ α]
[ContinuousConstSMul γ α]
[T2Space α]
(g : γ)
:
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}
[TopologicalSpace α]
[AddCommMonoid α]
{f : β → α}
{γ : Type u_5}
[DivisionRing γ]
[Module γ α]
[ContinuousConstSMul γ α]
[T2Space α]
(g : γ)
:
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}
[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_5}
{R : Type u_7}
{M : Type u_9}
[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_5}
{R : Type u_7}
{M : Type u_9}
[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_5}
{κ : Type u_6}
{R : Type u_7}
{M : Type u_9}
[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_5}
{κ : Type u_6}
{R : Type u_7}
{M : Type u_9}
[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_5}
{κ : Type u_6}
{R : Type u_7}
{M : Type u_9}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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_5}
{R : Type u_7}
{R₂ : Type u_8}
{M : Type u_9}
{M₂ : Type u_10}
[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)
noncomputable def
AddAction.automorphize
{α : Type u_1}
{β : Type u_2}
{M : Type u_11}
[TopologicalSpace M]
[AddCommMonoid M]
[AddGroup α]
[AddAction α β]
(f : β → M)
:
Quotient (AddAction.orbitRel α β) → 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
- AddAction.automorphize f = Quotient.lift (fun (b : β) => ∑' (a : α), f (a +ᵥ b)) ⋯
Instances For
theorem
AddAction.automorphize.proof_1
{α : Type u_2}
{β : Type u_1}
{M : Type u_3}
[TopologicalSpace M]
[AddCommMonoid M]
[AddGroup α]
[AddAction α β]
(f : β → M)
(b₁ : β)
(b₂ : β)
:
noncomputable def
MulAction.automorphize
{α : Type u_1}
{β : Type u_2}
{M : Type u_11}
[TopologicalSpace M]
[AddCommMonoid M]
[Group α]
[MulAction α β]
(f : β → M)
:
Quotient (MulAction.orbitRel α β) → 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
- MulAction.automorphize f = Quotient.lift (fun (b : β) => ∑' (a : α), f (a • b)) ⋯
Instances For
theorem
MulAction.automorphize_smul_left
{α : Type u_1}
{β : Type u_2}
{M : Type u_11}
[TopologicalSpace M]
[AddCommMonoid M]
[T2Space M]
{R : Type u_12}
[DivisionRing R]
[Module R M]
[ContinuousConstSMul R M]
[Group α]
[MulAction α β]
(f : β → M)
(g : Quotient (MulAction.orbitRel α β) → R)
:
MulAction.automorphize (g ∘ Quotient.mk' • f) = g • MulAction.automorphize 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}
[TopologicalSpace M]
[AddCommMonoid M]
[T2Space M]
{R : Type u_12}
[DivisionRing R]
[Module R M]
[ContinuousConstSMul R M]
[AddGroup α]
[AddAction α β]
(f : β → M)
(g : Quotient (AddAction.orbitRel α β) → R)
:
AddAction.automorphize (g ∘ Quotient.mk' • f) = g • AddAction.automorphize 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}
[TopologicalSpace M]
[AddCommMonoid M]
{G : Type u_13}
[AddGroup G]
{Γ : AddSubgroup G}
(f : G → M)
:
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}
[TopologicalSpace M]
[AddCommMonoid M]
{G : Type u_13}
[Group G]
{Γ : Subgroup G}
(f : G → M)
:
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}
[TopologicalSpace M]
[AddCommMonoid M]
[T2Space M]
{R : Type u_12}
[DivisionRing R]
[Module R M]
[ContinuousConstSMul R M]
{G : Type u_13}
[Group G]
{Γ : Subgroup G}
(f : G → M)
(g : G ⧸ Γ → R)
:
QuotientGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientGroup.automorphize 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}
[TopologicalSpace M]
[AddCommMonoid M]
[T2Space M]
{R : Type u_12}
[DivisionRing R]
[Module R M]
[ContinuousConstSMul R M]
{G : Type u_13}
[AddGroup G]
{Γ : AddSubgroup G}
(f : G → M)
(g : G ⧸ Γ → R)
:
QuotientAddGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientAddGroup.automorphize f
Automorphization of a function into an R-module distributes, that is, commutes with the
R-scalar multiplication.