Mathlib.Topology.Algebra.InfiniteSum.Module

HasSum.const_smul theorem

{a : α} (b : γ) (hf : HasSum f a) : HasSum (fun i ↦ b • f i) (b • a)

Full source

theorem HasSum.const_smul {a : α} (b : γ) (hf : HasSum f a) : HasSum (fun i ↦ b • f i) (b • a) :=
  hf.map (DistribMulAction.toAddMonoidHom α _) <| continuous_const_smul _

Scalar Multiplication Preserves Sum Convergence

Informal description

Let $f$ be a function such that the sum of $f(i)$ over all $i$ converges to $a$. Then for any scalar $b$, the sum of $b \cdot f(i)$ over all $i$ converges to $b \cdot a$.

Summable.const_smul theorem

(b : γ) (hf : Summable f) : Summable fun i ↦ b • f i

Full source

theorem Summable.const_smul (b : γ) (hf : Summable f) : Summable fun i ↦ b • f i :=
  (hf.hasSum.const_smul _).summable

Summability under Scalar Multiplication

Informal description

Let $f$ be a summable function. Then for any scalar $b$, the function $i \mapsto b \cdot f(i)$ is also summable.

Summable.tsum_const_smul theorem

[T2Space α] (b : γ) (hf : Summable f) : ∑' i, b • f i = b • ∑' i, f i

Full source

/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Monoid`, but
  requiring a summability hypothesis. -/
protected theorem Summable.tsum_const_smul [T2Space α] (b : γ) (hf : Summable f) :
    ∑' i, b • f i = b • ∑' i, f i :=
  (hf.hasSum.const_smul _).tsum_eq

Scalar Multiplication Commutes with Infinite Sum in Hausdorff Spaces

Informal description

Let $\alpha$ be a Hausdorff topological space and $\gamma$ a type with a scalar multiplication action on $\alpha$. If $f$ is a summable function with values in $\alpha$, then for any scalar $b \in \gamma$, the sum $\sum_{i} b \cdot f(i)$ equals $b$ multiplied by the sum $\sum_{i} f(i)$, i.e., \[ \sum_{i} b \cdot f(i) = b \cdot \sum_{i} f(i). \]

tsum_const_smul' theorem

 {γ : Type*} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) :
  ∑' (i : β), g • f i = g • ∑' (i : β), f i

Full source

/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Group`, but
  not requiring any summability hypothesis. -/
lemma tsum_const_smul' {γ : Type*} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α]
    [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i := by
  by_cases hf : Summable f
  · exact hf.tsum_const_smul g
  rw [tsum_eq_zero_of_not_summable hf]
  simp only [smul_zero]
  let mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
  apply tsum_eq_zero_of_not_summable
  change ¬ Summable (mul_g ∘ f)
  rwa [Summable.map_iff_of_equiv mul_g]
  · apply continuous_const_smul
  · apply continuous_const_smul

Scalar Multiplication Commutes with Infinite Sum in Hausdorff Spaces for Group Actions

Informal description

Let $\alpha$ be a Hausdorff topological space with a continuous scalar multiplication action by a group $\gamma$, and let $f : \beta \to \alpha$ be a function. Then for any $g \in \gamma$, the infinite sum $\sum_{i \in \beta} g \cdot f(i)$ is equal to $g$ multiplied by the infinite sum $\sum_{i \in \beta} f(i)$, i.e., \[ \sum_{i \in \beta} g \cdot f(i) = g \cdot \sum_{i \in \beta} f(i). \]

tsum_const_smul'' theorem

 {γ : Type*} [DivisionSemiring γ] [Module γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) :
  ∑' (i : β), g • f i = g • ∑' (i : β), f i

Full source

/-- 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`. -/
lemma tsum_const_smul'' {γ : Type*} [DivisionSemiring γ] [Module γ α] [ContinuousConstSMul γ α]
    [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i := by
  rcases eq_or_ne g 0 with rfl | hg
  · simp
  · exact tsum_const_smul' (Units.mk0 g hg)

Scalar Multiplication Commutes with Infinite Sum in Hausdorff Spaces for Division Semiring Actions

Informal description

Let $\alpha$ be a Hausdorff topological space equipped with a continuous scalar multiplication action by a division semiring $\gamma$, and let $f : \beta \to \alpha$ be a function. Then for any scalar $g \in \gamma$, the infinite sum $\sum_{i \in \beta} g \cdot f(i)$ is equal to $g$ multiplied by the infinite sum $\sum_{i \in \beta} f(i)$, i.e., \[ \sum_{i \in \beta} g \cdot f(i) = g \cdot \sum_{i \in \beta} f(i). \]

HasSum.smul_const theorem

{r : R} (hf : HasSum f r) (a : M) : HasSum (fun z ↦ f z • a) (r • a)

Full source

theorem HasSum.smul_const {r : R} (hf : HasSum f r) (a : M) : HasSum (fun z ↦ f z • a) (r • a) :=
  hf.map ((smulAddHom R M).flip a) (continuous_id.smul continuous_const)

Scalar Multiplication Preserves Summability: $\sum_z f(z) \cdot a = (\sum_z f(z)) \cdot a$

Informal description

Let $f$ be a function such that the sum of $f$ over its domain converges to $r \in R$. Then for any element $a \in M$, the sum of the function $z \mapsto f(z) \cdot a$ converges to $r \cdot a$, where $\cdot$ denotes the scalar multiplication operation.

Summable.smul_const theorem

(hf : Summable f) (a : M) : Summable fun z ↦ f z • a

Full source

theorem Summable.smul_const (hf : Summable f) (a : M) : Summable fun z ↦ f z • a :=
  (hf.hasSum.smul_const _).summable

Summability under Scalar Multiplication by a Constant

Informal description

If a function $f$ is summable, then for any element $a$ in a topological vector space $M$, the function $z \mapsto f(z) \cdot a$ is also summable.

Summable.tsum_smul_const theorem

[T2Space M] (hf : Summable f) (a : M) : ∑' z, f z • a = (∑' z, f z) • a

Full source

protected theorem Summable.tsum_smul_const [T2Space M] (hf : Summable f) (a : M) :
    ∑' z, f z • a = (∑' z, f z) • a :=
  (hf.hasSum.smul_const _).tsum_eq

Sum of Scalar Multiples Equals Scalar Multiple of Sum in Hausdorff Spaces

Informal description

Let $M$ be a Hausdorff topological space and $f$ be a summable function. Then for any element $a \in M$, the sum $\sum_{z} f(z) \cdot a$ is equal to $(\sum_{z} f(z)) \cdot a$, where $\cdot$ denotes the scalar multiplication operation.

HasSum.smul_eq theorem

(hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun x : ι × κ ↦ f x.1 • g x.2) u) : s • t = u

Full source

theorem HasSum.smul_eq (hf : HasSum f s) (hg : HasSum g t)
    (hfg : HasSum (fun x : ι × κ ↦ f x.1 • g x.2) u) : s • t = u :=
  have key₁ : HasSum (fun i ↦ f i • t) (s • t) := hf.smul_const t
  have this : ∀ i : ι, HasSum (fun c : κ ↦ f i • g c) (f i • t) := fun i ↦ hg.const_smul (f i)
  have key₂ : HasSum (fun i ↦ f i • t) u := HasSum.prod_fiberwise hfg this
  key₁.unique key₂

Scalar Product of Sums Equals Double Sum: $s \cdot t = \sum_{i,j} f(i) \cdot g(j)$

Informal description

Let $f$ and $g$ be functions such that $\sum f(i) = s$ and $\sum g(j) = t$, and suppose the double sum $\sum_{i,j} f(i) \cdot g(j)$ converges to $u$. Then the scalar product $s \cdot t$ equals $u$.

HasSum.smul theorem

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

Full source

theorem HasSum.smul (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) :=
  let ⟨_u, hu⟩ := hfg
  (hf.smul_eq hg hu).symm ▸ hu

Double Sum of Scalar Products Equals Product of Sums: $\sum_{i,j} f(i) \cdot g(j) = (\sum_i f(i)) \cdot (\sum_j g(j))$

Informal description

Let $f : \iota \to M$ and $g : \kappa \to M$ be functions such that $\sum_{i \in \iota} f(i) = s$ and $\sum_{j \in \kappa} g(j) = t$. If the double sum $\sum_{(i,j) \in \iota \times \kappa} f(i) \cdot g(j)$ is summable, then it converges to $s \cdot t$.

tsum_smul_tsum theorem

 (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

Full source

/-- Scalar product of two infinites sums indexed by arbitrary types. -/
theorem tsum_smul_tsum (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 :=
  hf.hasSum.smul_eq hg.hasSum hfg.hasSum

Scalar Product of Sums Equals Double Sum: $(\sum f) \cdot (\sum g) = \sum_{i,j} f(i) \cdot g(j)$

Informal description

Let $f : \iota \to M$ and $g : \kappa \to M$ be summable functions, and suppose the double sum $\sum_{(i,j) \in \iota \times \kappa} f(i) \cdot g(j)$ is also summable. Then the scalar product of the sums equals the double sum, i.e., \[ \left(\sum_{i \in \iota} f(i)\right) \cdot \left(\sum_{j \in \kappa} g(j)\right) = \sum_{(i,j) \in \iota \times \kappa} f(i) \cdot g(j). \]

ContinuousLinearMap.hasSum theorem

{f : ι → M} (φ : M →SL[σ] M₂) {x : M} (hf : HasSum f x) : HasSum (fun b : ι ↦ φ (f b)) (φ x)

Full source

/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem ContinuousLinearMap.hasSum {f : ι → M} (φ : M →SL[σ] M₂) {x : M}
    (hf : HasSum f x) : HasSum (fun b : ι ↦ φ (f b)) (φ x) := by
  simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous

Continuous linear maps commute with infinite sums

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field with a continuous linear map $\phi: M \to M₂$. Given a function $f: \iota \to M$ and an element $x \in M$ such that $f$ has sum $x$ (i.e., $\sum_{i \in \iota} f(i) = x$), then the function $\phi \circ f: \iota \to M₂$ has sum $\phi(x)$ (i.e., $\sum_{i \in \iota} \phi(f(i)) = \phi(x)$).

ContinuousLinearMap.summable theorem

{f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f) : Summable fun b : ι ↦ φ (f b)

Full source

protected theorem ContinuousLinearMap.summable {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f) :
    Summable fun b : ι ↦ φ (f b) :=
  (hf.hasSum.mapL φ).summable

Summability under Continuous Linear Maps

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field, and let $\phi: M \to M₂$ be a continuous linear map. If a function $f: \iota \to M$ is summable, then the function $\phi \circ f: \iota \to M₂$ is also summable.

ContinuousLinearMap.map_tsum theorem

[T2Space M₂] {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f) : φ (∑' z, f z) = ∑' z, φ (f z)

Full source

protected theorem ContinuousLinearMap.map_tsum [T2Space M₂] {f : ι → M} (φ : M →SL[σ] M₂)
    (hf : Summable f) : φ (∑' z, f z) = ∑' z, φ (f z) :=
  (hf.hasSum.mapL φ).tsum_eq.symm

Continuous Linear Maps Commute with Infinite Sums in Hausdorff Spaces

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field, with $M₂$ being Hausdorff. Given a continuous linear map $\phi: M \to M₂$ and a summable function $f: \iota \to M$, the image of the sum of $f$ under $\phi$ equals the sum of the images, i.e., $\phi\left(\sum_{z \in \iota} f(z)\right) = \sum_{z \in \iota} \phi(f(z))$.

ContinuousLinearEquiv.hasSum theorem

{f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} : HasSum (fun b : ι ↦ e (f b)) y ↔ HasSum f (e.symm y)

Full source

/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem ContinuousLinearEquiv.hasSum {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} :
    HasSumHasSum (fun b : ι ↦ e (f b)) y ↔ HasSum f (e.symm y) :=
  ⟨fun h ↦ by simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M),
    fun h ↦ by simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h⟩

Continuous Linear Equivalence Preserves Summability: $e(\sum f) = y \leftrightarrow \sum f = e^{-1}(y)$

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field, and let $e: M \simeq M₂$ be a continuous linear equivalence. Given a function $f: \iota \to M$ and an element $y \in M₂$, the function $e \circ f: \iota \to M₂$ has sum $y$ if and only if $f$ has sum $e^{-1}(y)$.

ContinuousLinearEquiv.hasSum' theorem

{f : ι → M} (e : M ≃SL[σ] M₂) {x : M} : HasSum (fun b : ι ↦ e (f b)) (e x) ↔ HasSum f x

Full source

/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem ContinuousLinearEquiv.hasSum' {f : ι → M} (e : M ≃SL[σ] M₂) {x : M} :
    HasSumHasSum (fun b : ι ↦ e (f b)) (e x) ↔ HasSum f x := by
  rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]

Continuous Linear Equivalence Preserves Summability at Image Point: $e(\sum f) = e(x) \leftrightarrow \sum f = x$

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field, and let $e: M \simeq M₂$ be a continuous linear equivalence. Given a function $f: \iota \to M$ and an element $x \in M$, the function $e \circ f: \iota \to M₂$ has sum $e(x)$ if and only if $f$ has sum $x$.

ContinuousLinearEquiv.summable theorem

{f : ι → M} (e : M ≃SL[σ] M₂) : (Summable fun b : ι ↦ e (f b)) ↔ Summable f

Full source

protected theorem ContinuousLinearEquiv.summable {f : ι → M} (e : M ≃SL[σ] M₂) :
    (Summable fun b : ι ↦ e (f b)) ↔ Summable f :=
  ⟨fun hf ↦ (e.hasSum.1 hf.hasSum).summable, (e : M →SL[σ] M₂).summable⟩

Continuous Linear Equivalence Preserves Summability: $\sum e \circ f$ converges iff $\sum f$ converges

Informal description

Let $M$ and $M₂$ be topological vector spaces over a field, and let $e: M \simeq M₂$ be a continuous linear equivalence. Given a function $f: \iota \to M$, the function $e \circ f: \iota \to M₂$ is summable if and only if $f$ is summable.

ContinuousLinearEquiv.tsum_eq_iff theorem

 [T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} : (∑' z, e (f z)) = y ↔ ∑' z, f z = e.symm y

Full source

theorem ContinuousLinearEquiv.tsum_eq_iff [T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂)
    {y : M₂} : (∑' z, e (f z)) = y ↔ ∑' z, f z = e.symm y := by
  by_cases hf : Summable f
  · exact
      ⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
        (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
  · have hf' : ¬Summable fun z ↦ e (f z) := fun h ↦ hf (e.summable.mp h)
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
    refine ⟨?_, fun H ↦ ?_⟩
    · rintro rfl
      simp
    · simpa using congr_arg (fun z ↦ e z) H

Sum Equivalence under Continuous Linear Isomorphism: $\sum e(f) = y \leftrightarrow \sum f = e^{-1}(y)$

Informal description

Let $M$ and $M₂$ be Hausdorff topological vector spaces, and let $e: M \simeq M₂$ be a continuous linear equivalence. For a function $f: \iota \to M$ and an element $y \in M₂$, the sum $\sum_{z} e(f(z))$ equals $y$ if and only if the sum $\sum_{z} f(z)$ equals $e^{-1}(y)$.

ContinuousLinearEquiv.map_tsum theorem

[T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂) : e (∑' z, f z) = ∑' z, e (f z)

Full source

protected theorem ContinuousLinearEquiv.map_tsum [T2Space M] [T2Space M₂] {f : ι → M}
    (e : M ≃SL[σ] M₂) : e (∑' z, f z) = ∑' z, e (f z) := by
  refine symm (e.tsum_eq_iff.mpr ?_)
  rw [e.symm_apply_apply _]

Continuous Linear Equivalence Commutes with Infinite Sums: $e(\sum f) = \sum e \circ f$

Informal description

Let $M$ and $M₂$ be Hausdorff topological vector spaces, and let $e: M \simeq M₂$ be a continuous linear equivalence. For any summable function $f: \iota \to M$, the image of the sum $\sum_{z} f(z)$ under $e$ equals the sum $\sum_{z} e(f(z))$, i.e., $$ e\left(\sum_{z} f(z)\right) = \sum_{z} e(f(z)). $$

MulAction.automorphize definition

[Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M

Full source

/-- 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)`. -/
@[to_additive "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)`."]
noncomputable def MulAction.automorphize [Group α] [MulAction α β] (f : β → M) :
    Quotient (MulAction.orbitRel α β) → M := by
  refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_
  intro b₁ b₂ ⟨a, (ha : a • b₂ = b₁)⟩
  simp only
  rw [← ha]
  convert (Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂)) using 1
  simp only [Equiv.coe_mulRight]
  congr
  ext
  congr 1
  simp only [mul_smul]

Automorphization of a function under a group action

Informal description

Given a group $\alpha$ acting on a type $\beta$ and a function $f : \beta \to M$, the automorphization of $f$ is a function $\beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha \to M$ defined on the quotient space of $\beta$ by the orbit relation of $\alpha$, where for each equivalence class $[b]$, the value is given by the sum $\sum'_{a \in \alpha} f(a \cdot b)$. Here, $\beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha$ denotes the quotient of $\beta$ by the equivalence relation induced by the group action, and $\sum'$ denotes the sum over the group elements (which may be an infinite sum if $\alpha$ is infinite).

MulAction.automorphize_smul_left theorem

 [Group α] [MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R) :
  MulAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) =
    g • (MulAction.automorphize f : Quotient (MulAction.orbitRel α β) → M)

Full source

/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
lemma MulAction.automorphize_smul_left [Group α] [MulAction α β] (f : β → M)
    (g : Quotient (MulAction.orbitRel α β) → R) :
    MulAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f)
      = g • (MulAction.automorphize f : Quotient (MulAction.orbitRel α β) → M) := by
  ext x
  apply @Quotient.inductionOn' β (MulAction.orbitRel α β) _ x _
  intro b
  simp only [automorphize, Pi.smul_apply', comp_apply]
  set π : β → Quotient (MulAction.orbitRel α β) := Quotient.mk (MulAction.orbitRel α β)
  have H₁ : ∀ a : α, π (a • b) = π b := by
    intro a
    apply (@Quotient.eq _ (MulAction.orbitRel α β) (a • b) b).mpr
    use a
  change ∑' a : α, g (π (a • b)) • f (a • b) = g (π b) • ∑' a : α, f (a • b)
  simp_rw [H₁]
  exact tsum_const_smul'' _

Automorphization Commutes with Scalar Multiplication: $\text{automorphize}((g \circ \pi) \cdot f) = g \cdot \text{automorphize}(f)$

Informal description

Let $\alpha$ be a group acting on a type $\beta$, and let $f : \beta \to M$ be a function. For any function $g : \beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha \to R$ (where $\beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha$ denotes the quotient of $\beta$ by the orbit relation of $\alpha$), the automorphization of the scalar multiple $(g \circ \pi) \cdot f$ (with $\pi : \beta \to \beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha$ the projection) equals the scalar multiple $g \cdot \text{automorphize}(f)$. In other words: \[ \text{automorphize}\big((g \circ \pi) \cdot f\big) = g \cdot \text{automorphize}(f). \]

AddAction.automorphize_smul_left theorem

 [AddGroup α] [AddAction α β] (f : β → M) (g : Quotient (AddAction.orbitRel α β) → R) :
  AddAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) =
    g • (AddAction.automorphize f : Quotient (AddAction.orbitRel α β) → M)

Full source

/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
lemma AddAction.automorphize_smul_left [AddGroup α] [AddAction α β]  (f : β → M)
    (g : Quotient (AddAction.orbitRel α β) → R) :
    AddAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f)
      = g • (AddAction.automorphize f : Quotient (AddAction.orbitRel α β) → M) := by
  ext x
  apply @Quotient.inductionOn' β (AddAction.orbitRel α β) _ x _
  intro b
  simp only [automorphize, Pi.smul_apply', comp_apply]
  set π : β → Quotient (AddAction.orbitRel α β) := Quotient.mk (AddAction.orbitRel α β)
  have H₁ : ∀ a : α, π (a +ᵥ b) = π b := by
    intro a
    apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr
    use a
  change ∑' a : α, g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' a : α, f (a +ᵥ b)
  simp_rw [H₁]
  exact tsum_const_smul'' _

Automorphization Commutes with Scalar Multiplication for Additive Group Actions

Informal description

Let $\alpha$ be an additive group acting on a type $\beta$, and let $f : \beta \to M$ be a function. For any function $g : \beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha \to R$, the automorphization of the pointwise scalar multiplication $(g \circ \pi) \cdot f$ (where $\pi : \beta \to \beta \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \alpha$ is the quotient map) equals the scalar multiplication of $g$ with the automorphization of $f$, i.e., \[ \text{automorphize}\big((g \circ \pi) \cdot f\big) = g \cdot \text{automorphize}(f). \]

QuotientGroup.automorphize definition

(f : G → M) : G ⧸ Γ → M

Full source

/-- 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)`. -/
@[to_additive "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)`."]
noncomputable def QuotientGroup.automorphize (f : G → M) : G ⧸ Γ → M := MulAction.automorphize f

Automorphization of a function over a quotient group

Informal description

Given a subgroup $\Gamma$ of a group $G$ and a function $f : G \to M$, the automorphization of $f$ is a function $G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma \to M$ defined on the quotient space $G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma$ by summing over $\Gamma$-orbits: for each coset $g\Gamma$, the value is given by $\sum'_{\gamma \in \Gamma} f(\gamma \cdot g)$, where $\sum'$ denotes the sum over the subgroup elements (which may be an infinite sum if $\Gamma$ is infinite).

QuotientGroup.automorphize_smul_left theorem

 (f : G → M) (g : G ⧸ Γ → R) :
  (QuotientGroup.automorphize ((g ∘ (@Quotient.mk' _ (_)) : G → R) • f) : G ⧸ Γ → M) =
    g • (QuotientGroup.automorphize f : G ⧸ Γ → M)

Full source

/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
lemma QuotientGroup.automorphize_smul_left (f : G → M) (g : G ⧸ Γ → R) :
    (QuotientGroup.automorphize ((g ∘ (@Quotient.mk' _ (_)) : G → R) • f) : G ⧸ Γ → M)
      = g • (QuotientGroup.automorphize f : G ⧸ Γ → M) :=
  MulAction.automorphize_smul_left f g

Automorphization Commutes with Scalar Multiplication: $\text{automorphize}((g \circ \pi) \cdot f) = g \cdot \text{automorphize}(f)$

Informal description

Let $G$ be a group with a subgroup $\Gamma$, and let $f : G \to M$ be a function. For any function $g : G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma \to R$, the automorphization of the scalar multiple $(g \circ \pi) \cdot f$ (where $\pi : G \to G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma$ is the quotient map) equals the scalar multiple $g \cdot \text{automorphize}(f)$. In other words: \[ \text{automorphize}\big((g \circ \pi) \cdot f\big) = g \cdot \text{automorphize}(f). \]

QuotientAddGroup.automorphize_smul_left theorem

 (f : G → M) (g : G ⧸ Γ → R) :
  QuotientAddGroup.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) = g • (QuotientAddGroup.automorphize f : G ⧸ Γ → M)

Full source

/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
lemma QuotientAddGroup.automorphize_smul_left (f : G → M) (g : G ⧸ Γ → R) :
    QuotientAddGroup.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f)
      = g • (QuotientAddGroup.automorphize f : G ⧸ Γ → M) :=
  AddAction.automorphize_smul_left f g

Automorphization Commutes with Scalar Multiplication for Quotient Additive Groups

Informal description

Let $G$ be an additive group with a subgroup $\Gamma$ acting on $G$, and let $f : G \to M$ be a function. For any function $g : G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma \to R$, the automorphization of the pointwise scalar multiplication $(g \circ \pi) \cdot f$ (where $\pi : G \to G \mkern-2mu\mathbin{/\mkern-6mu/}\mkern-2mu \Gamma$ is the quotient map) equals the scalar multiplication of $g$ with the automorphization of $f$, i.e., \[ \text{automorphize}\big((g \circ \pi) \cdot f\big) = g \cdot \text{automorphize}(f). \]