Documentation

Mathlib.Topology.Algebra.InfiniteSum.Module

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) :
HasSum (fun (i : β) => b f i) (b a)
theorem Summable.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid γ] [TopologicalSpace α] [AddCommMonoid α] [DistribMulAction γ α] [ContinuousConstSMul γ α] {f : βα} (b : γ) (hf : Summable f) :
Summable fun (i : β) => b f i
theorem tsum_const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid γ] [TopologicalSpace α] [AddCommMonoid α] [DistribMulAction γ α] [ContinuousConstSMul γ α] {f : βα} [T2Space α] (b : γ) (hf : Summable f) :
∑' (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} [TopologicalSpace α] [AddCommMonoid α] {f : βα} {γ : Type u_5} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α] [T2Space α] (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} [TopologicalSpace α] [AddCommMonoid α] {f : βα} {γ : Type u_5} [DivisionRing γ] [Module γ α] [ContinuousConstSMul γ α] [T2Space α] (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} [Semiring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul 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} [Semiring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] {f : ιR} (hf : Summable f) (a : M) :
Summable fun (z : ι) => f z a
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) :
∑' (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} [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) :
s t = 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) :
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} [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) :
(∑' (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] [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} :
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] [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₂) :
(Summable fun (b : ι) => e (f b)) Summable f
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)
abbrev AddAction.automorphize.match_1 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (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} [TopologicalSpace M] [AddCommMonoid M] [AddGroup α] [AddAction α β] (f : β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} [TopologicalSpace M] [AddCommMonoid M] [AddGroup α] [AddAction α β] (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} [TopologicalSpace M] [AddCommMonoid M] [Group α] [MulAction α β] (f : β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} [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) :

        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) :

        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 : 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} [TopologicalSpace M] [AddCommMonoid M] {G : Type u_13} [Group G] {Γ : Subgroup G} (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} [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 : GM) (g : G ΓR) :

            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 : GM) (g : G ΓR) :

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