tsum_const_smul'
theorem tsum_const_smul' :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] {f : β → α} {γ : Type u_5}
[inst_2 : Group γ] [inst_3 : DistribMulAction γ α] [inst_4 : ContinuousConstSMul γ α] [inst_5 : T2Space α]
(g : γ), ∑' (i : β), g • f i = g • ∑' (i : β), f i
This theorem states that infinite sums commute with scalar multiplication. In other words, for any group of scalars (`γ`) and any function (`f`) mapping from an arbitrary type (`β`) to a topological space (`α`), the infinite sum of the scalar multiplied by the function value at each point (`∑' (i : β), g • f i`) is equal to the scalar multiplied by the infinite sum of the function values at each point (`g • ∑' (i : β), f i`). This holds true even without any assumptions about the summability of the series.
More concisely: For any group of scalars `γ` and any function `f` from type `β` to topological space `α`, the infinite sum `∑' (i : β), g • f i` equals `g • ∑' (i : β), f i`, without any assumptions on summability.
|
HasSum.const_smul
theorem HasSum.const_smul :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Monoid γ] [inst_1 : TopologicalSpace α]
[inst_2 : AddCommMonoid α] [inst_3 : DistribMulAction γ α] [inst_4 : ContinuousConstSMul γ α] {f : β → α} {a : α}
(b : γ), HasSum f a → HasSum (fun i => b • f i) (b • a)
This theorem, `HasSum.const_smul`, states that for any types `α`, `β`, and `γ` where `α` is a topological space and an additive commutative monoid, `γ` is a monoid, and there exists a distributive multiplication action of `γ` on `α` that is continuous, if the function `f` mapping from `β` to `α` has a sum `a`, then the function where each term `f i` is scaled by a constant `b` from `γ` also has a sum, specifically `b • a`. In other words, scaling all terms in a summable sequence by a constant factor scales the sum by that same factor.
More concisely: If `f` is a summable function from a monoid `β` to a topological space and additive commutative monoid `α` with a continuous, distributive multiplication action of a monoid `γ`, then scaling each term of the sum `f` by a constant `b` from `γ` results in a sum equal to `b * (sum of f)`.
|
tsum_const_smul''
theorem tsum_const_smul'' :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] {f : β → α} {γ : Type u_5}
[inst_2 : DivisionRing γ] [inst_3 : Module γ α] [inst_4 : ContinuousConstSMul γ α] [inst_5 : T2Space α] (g : γ),
∑' (i : β), g • f i = g • ∑' (i : β), f i
This theorem states that infinite sums can be commuted with scalar multiplication for scalars residing in a `DivisionRing`. There is no requirement for the sums to be summable. The theorem could potentially be generalized to work for a `GroupWithZero γ` if a structure like `DistribMulActionWithZero` existed. Specifically, given a function `f` from `β` to `α`, and a scalar `g` from a division ring `γ`, the sum of the scalar-multiplied function values over all `i` in `β` is equal to the scalar multiplied by the sum of the function values over all `i` in `β`. This is expressed mathematically as ∑' (i : β), g • f i = g • ∑' (i : β), f i.
More concisely: For any function `f` from a set `β` to a module `α` over a division ring `γ`, and for any scalar `g` in `γ`, the infinite sum of scalar-multiplied function values equals the scalar multiplication of the infinite sum of function values: g • ∑' (i : β), f i = ∑' (i : β), g • f i.
|
MulAction.automorphize_smul_left
theorem MulAction.automorphize_smul_left :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
[inst_2 : T2Space M] {R : Type u_12} [inst_3 : DivisionRing R] [inst_4 : Module R M]
[inst_5 : ContinuousConstSMul R M] [inst_6 : Group α] [inst_7 : MulAction α β] (f : β → M)
(g : Quotient (MulAction.orbitRel α β) → R),
MulAction.automorphize (g ∘ Quotient.mk' • f) = g • MulAction.automorphize f
The theorem `MulAction.automorphize_smul_left` states that for a given function `f` from a type `β` into a `R`-`Module` `M`, and a function `g` from the quotient of type `β` under a `MulAction` to a `DivisionRing` `R`, the "automorphization" of the function `f` (which is a process that sums over the `α` orbits, transforming `f` into a function from `β ⧸ α` to `M`), distributes over the `R`-scalar multiplication. In other words, the automorphization of the scalar multiplication of `g` and the function `f` is equal to the scalar multiplication of `g` and the automorphization of `f`. This means that automorphization commutes with the `R`-scalar multiplication. The types involved must satisfy conditions like being a `TopologicalSpace`, a `AddCommMonoid`, a `T2Space`, a `DivisionRing`, a `Module`, and having a `MulAction`, amongst others.
More concisely: The automorphization of an `R`-linear map `f` from a `β`-quotiented `T2Space` into an `R`-module, with respect to a `MulAction` and a homomorphism `g` from the `β`-quotient to a division ring `R`, commutes with `R`-scalar multiplication.
|
QuotientGroup.automorphize_smul_left
theorem QuotientGroup.automorphize_smul_left :
∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [inst_2 : T2Space M] {R : Type u_12}
[inst_3 : DivisionRing R] [inst_4 : Module R M] [inst_5 : ContinuousConstSMul R M] {G : Type u_13}
[inst_6 : Group G] {Γ : Subgroup G} (f : G → M) (g : G ⧸ Γ → R),
QuotientGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientGroup.automorphize f
This theorem states that the process of automorphization of a function into an `R`-Module is distributive, meaning it commutes with the scalar multiplication of `R`. Specifically, for any topological space `M` that is also an `R`-Module, a group `G`, a subgroup `Γ` of `G`, and functions `f : G → M` and `g : G ⧸ Γ → R`, the result of first applying the scalar multiplication `g ∘ Quotient.mk'` to `f` and then performing the automorphization is the same as first performing the automorphization of `f` and then applying the scalar multiplication by `g`. This theorem is significant in the study of group theory and Module theory, as it relates the algebraic operations of scalar multiplication and automorphization.
More concisely: For any topological space M that is an R-Module, group G, subgroup Γ of G, functions f : G → M, and g : G ⧸ Γ → R, the automorphization of f and application of g via scalar multiplication commute: g ∘ Quotient.mk ' ∘ f = (g ∘ Quotient.mk ') ∘ Aut f.
|
ContinuousLinearMap.hasSum
theorem ContinuousLinearMap.hasSum :
∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
[inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {f : ι → M}
(φ : M →SL[σ] M₂) {x : M}, HasSum f x → HasSum (fun b => φ (f b)) (φ x)
This theorem states that for any semirings `R` and `R₂`, additively commutative monoids `M` and `M₂`, any `R`-module `M` and `R₂`-module `M₂`, where `M` and `M₂` are also topological spaces, a ring homomorphism `σ` from `R` to `R₂`, and a continuous linear map `φ` from `M` to `M₂`, if a sequence `f` (from an index set `ι` to `M`) sums to a value `x` in `M`, then the sequence obtained by applying the map `φ` to each term of `f` sums to `φ(x)` in `M₂`. In other words, applying a continuous linear map commutes with taking an infinite sum.
More concisely: Given ring homomorphisms `σ: R → R₂`, continuous linear maps `φ: M → M₂` between additively commutative monoids `M` and `M₂`, topological spaces `M` and `M₂`, and `R`-module/`R₂`-module structures on `M` and `M₂`, if a sequence `(x_i : M)` from an index set `ι` sums to `x` in `M`, then `(φ(x_i): M₂)` sums to `φ(x)` in `M₂`.
|
HasSum.smul_const
theorem HasSum.smul_const :
∀ {ι : Type u_5} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : TopologicalSpace R]
[inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : ContinuousSMul R M]
{f : ι → R} {r : R}, HasSum f r → ∀ (a : M), HasSum (fun z => f z • a) (r • a)
This theorem states that, for all types `ι`, `R`, and `M`, with `R` being a semiring and also topological space, `M` being a topological space, an additive commutative monoid, and a module over `R`, and the multiplication between `R` and `M` being continuous, if a function `f` from `ι` to `R` has a sum `r`, then for any element `a` of `M`, the function defined as the product of `f(z)` and `a` also has a sum, specifically `r • a`. This theorem relates the concept of sum in the case of functions with scalar multiplication.
More concisely: For any semiring `R` that is a topological space, any topological space and additive commutative monoid `M` that is an `R`-module with continuous scalar multiplication, and any function `f` from a type `ι` to `R` with sum `r`, the function `x => r * a * f x` has sum `r * a`, where `a` is any element of `M`.
|
QuotientAddGroup.automorphize_smul_left
theorem QuotientAddGroup.automorphize_smul_left :
∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [inst_2 : T2Space M] {R : Type u_12}
[inst_3 : DivisionRing R] [inst_4 : Module R M] [inst_5 : ContinuousConstSMul R M] {G : Type u_13}
[inst_6 : AddGroup G] {Γ : AddSubgroup G} (f : G → M) (g : G ⧸ Γ → R),
QuotientAddGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientAddGroup.automorphize f
This theorem states that the automorphization of a function into an `R`-`Module` commutes with the `R`-scalar multiplication. In more detail, for any topological space `M` with an additive commutative monoid structure and a `T2` space structure, any division ring `R` acting on `M` as a module, any additive group `G`, and any subgroup `Γ` of `G`, if we have a function `f` from `G` to `M` and a function `g` from the quotient group `G ⧸ Γ` to `R`, then the automorphization of the function obtained by composing `g` with the quotient map and multiplying by `f` is equal to the function obtained by multiplying `g` with the automorphization of `f`. In mathematical notation, this can be written as: if `f : G → M` and `g : G ⧸ Γ → R`, then `(g ∘ Quotient.mk') • f = g • automorphize f`.
More concisely: For any function `f : G -> M` from a group `G` to an `R`-module `M`, and any function `g : G / Γ -> R` from the quotient group of `G` by a subgroup `Γ` to `R`, the automorphization of the function `g ∘ Quotient.mk' ∘ f` is equal to the function `g ∘ automorphize f`, where `Quotient.mk'` is the quotient map.
|
Summable.mapL
theorem Summable.mapL :
∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
[inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {f : ι → M}
(φ : M →SL[σ] M₂), Summable f → Summable fun b => φ (f b)
The theorem `Summable.mapL` states that for any types `ι`, `R`, `R₂`, `M`, and `M₂`, given a semiring structure on `R` and `R₂`, an addition-commutative monoid structure on `M` and `M₂`, a module structure over `R` on `M` and over `R₂` on `M₂`, a topological space structure on `M` and `M₂`, a ring homomorphism `σ` from `R` to `R₂`, a function `f` from `ι` to `M`, and a continuous linear map `φ` from `M` to `M₂`, if the function `f` is summable then the function obtained by applying `φ` to each value of `f` is also summable. In other words, the summability property is preserved under continuous linear transformations.
More concisely: If `f` is a summable function from a type `ι` to a topological additive monoid `M` with module and topological structures over commutative semirings `R` and `R₂`, and `φ` is a continuous linear map from `M` to another topological additive monoid `M₂`, then the composition `φ ∘ f` is also a summable function.
|
HasSum.mapL
theorem HasSum.mapL :
∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
[inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {f : ι → M}
(φ : M →SL[σ] M₂) {x : M}, HasSum f x → HasSum (fun b => φ (f b)) (φ x)
This theorem, named `HasSum.mapL`, states that if you have a continuous linear map `φ` from one module `M` over a semiring `R` to another module `M₂` over a semiring `R₂`, and if a function `f` from an arbitrary type `ι` to `M` has an infinite sum `x`, then the infinite sum of the function obtained by applying `φ` to `f` is equal to the result of applying `φ` to `x`. In other words, applying a continuous linear map commutes with the operation of taking an infinite sum.
More concisely: If `φ: M →ₗ[R] M₂` is a continuous linear map between modules over semirings and `f: ι → M` has an infinite sum `x`, then `∑i φ(f i) = φ(∑i f i)`.
|
tsum_smul_tsum
theorem tsum_smul_tsum :
∀ {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M] [inst_5 : T3Space M]
[inst_6 : ContinuousAdd M] [inst_7 : ContinuousSMul R M] {f : ι → R} {g : κ → M},
Summable f →
Summable g →
(Summable fun x => f x.1 • g x.2) → (∑' (x : ι), f x) • ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 • g z.2
This theorem states that given two index types `ι` and `κ`, a semiring `R`, a type `M` that's a module over `R` with a topological structure and satisfying certain additional properties (like being a T3 space, having continuous addition, continuous scalar multiplication), and two functions `f : ι → R` and `g : κ → M`, if `f` and `g` are summable and the function `(x, y) ↦ f(x) • g(y)` is also summable (where `•` denotes scalar multiplication), then the scalar product of the (infinite) sums of `f` and `g` is equal to the (infinite) sum of the scalar products `f(z.1) • g(z.2)` over the product of the index sets `ι × κ`. In mathematical notation, if ∑`f(x)` and ∑`g(y)` exist, and ∑`f(x) • g(y)` also exists, then `(∑ f(x)) • (∑ g(y)) = ∑ (f(x) • g(y))` (sums over all `x` in `ι` and `y` in `κ`).
More concisely: Given two summable functions `f : ι → R` and `g : κ → M` from index types `ι` and `κ` into a commutative semiring `R` and an `R`-module `M` with a topological structure satisfying certain conditions, if the scalar products `f(x) • g(y)` are summable over all `x ∈ ι` and `y ∈ κ`, then `(∑ₙ f(x)) • (∑ₕ g(y)) = ∑ₙₕ (f(x) • g(y))`.
|
tsum_const_smul
theorem tsum_const_smul :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Monoid γ] [inst_1 : TopologicalSpace α]
[inst_2 : AddCommMonoid α] [inst_3 : DistribMulAction γ α] [inst_4 : ContinuousConstSMul γ α] {f : β → α}
[inst_5 : T2Space α] (b : γ), Summable f → ∑' (i : β), b • f i = b • ∑' (i : β), f i
This theorem, named `tsum_const_smul`, states that infinite sums commute with scalar multiplication. This is a version for scalars living in a monoid, but it requires a summability hypothesis. Specifically, given a type `α` with a topological space structure and an addition-commutative monoid structure, a type `β`, and a type `γ` with a monoid structure, along with a continuous scalar multiplication of `γ` and `α`, a function `f` from `β` to `α`, and a scalar `b` of type `γ`, if `f` is summable, then the infinite sum of the scalar multiplication of `b` and `f(i)` over all `i` of type `β` equals the scalar multiplication of `b` and the infinite sum of `f(i)` over all `i` of type `β`. In mathematical notation, this is saying that if ∑ f(i) exists, then ∑ (b * f(i)) = b * ∑ f(i).
More concisely: If `f : β -> α`, `b : γ`, and `∑ f i` exists in a topological monoid `(α, +)` with continuous scalar multiplication by `γ`, then `∑ (b * f i) = b * ∑ f i`.
|
ContinuousLinearMap.map_tsum
theorem ContinuousLinearMap.map_tsum :
∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
[inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
[inst_8 : T2Space M₂] {f : ι → M} (φ : M →SL[σ] M₂), Summable f → φ (∑' (z : ι), f z) = ∑' (z : ι), φ (f z)
This theorem states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, topological spaces over `M` and `M₂`, and a ring homomorphism `σ` from `R` to `R₂`, if `f` is a summable function from some index set `ι` to `M`, and if `φ` is a continuous linear map from `M` to `M₂` over `σ`, then the continuous linear map of the (infinite) sum of `f` is equal to the (infinite) sum of the continuous linear map of `f`. This essentially asserts that the continuous linear map commutes with the operation of infinite summation.
More concisely: Given semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, topological spaces over `M` and `M₂`, and a ring homomorphism `σ` from `R` to `R₂`, if `f : ι → M` is a summable function, and `φ : M → M₂` is a continuous linear map over `σ`, then `∑ i ∈ ι φ (f i) = φ (∑ i ∈ ι f i)`.
|
AddAction.automorphize_smul_left
theorem AddAction.automorphize_smul_left :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
[inst_2 : T2Space M] {R : Type u_12} [inst_3 : DivisionRing R] [inst_4 : Module R M]
[inst_5 : ContinuousConstSMul R M] [inst_6 : AddGroup α] [inst_7 : AddAction α β] (f : β → M)
(g : Quotient (AddAction.orbitRel α β) → R),
AddAction.automorphize (g ∘ Quotient.mk' • f) = g • AddAction.automorphize f
The theorem `AddAction.automorphize_smul_left` states that for any additive group `α`, any types `β` and `M`, a topological space structure on `M`, an additively commutative monoid structure on `M`, a T2 space (also known as a Hausdorff space) structure on `M`, any type `R`, a division ring structure on `R`, a module structure over `R` on `M`, a group action of `α` on `β`, a function `f` from `β` to `M`, and a function `g` from the quotient of `β` by the orbit relation of `α` to `R`, automorphizing (summing over the `α` orbits of) the scalar multiplication of `f` by the composition of `g` and the quotient map is equal to the scalar multiplication of the automorphized `f` by `g`. In essence, it says that automorphization commutes with scalar multiplication in this scenario.
More concisely: For any additive group α, types β and M, topological space structure on M, additively commutative monoid structure on M, T2 space structure on M, division ring R, M a R-module, group action of α on β, function f from β to M, and function g from the quotient of β by the orbit relation of α to R, the scalar multiplication of the automorphized sum of α-orbits of f by g equals the scalar multiplication of the automorphized f by g.
|