ContinuousMultilinearMap.map_sum
theorem ContinuousMultilinearMap.map_sum :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [inst_7 : Fintype ι] (g : (i : ι) → α i → M₁ i)
[inst_8 : DecidableEq ι] [inst_9 : (i : ι) → Fintype (α i)],
(f fun i => Finset.univ.sum fun j => g i j) = Finset.univ.sum fun r => f fun i => g i (r i)
The theorem `ContinuousMultilinearMap.map_sum` states that for a continuous multilinear map `f` from an `R`-module `M₁` to an `R`-module `M₂`, the map applied to the sum of vectors `g₁,...,gₙ`, each sum taken over all elements in a finite set, is equal to the sum of `f` applied to the vectors `(g₁ (r 1), ..., gₙ (r n))`, where the sum is taken over all possible functions `r`. This is a generalization of the distributive property for multilinear maps, and the result is obtained by repeatedly expanding the map with respect to each coordinate.
Here, `R` is a semiring, `M₁` and `M₂` are modules over `R` with `M₁` being a family of modules indexed by `ι`, `f` is a continuous multilinear map from `M₁` to `M₂`, and `g` is a family of functions mapping elements of `α` to `M₁`, where `ι` and `α` are finite types. The theorem assumes that each `M₁ i` and `M₂` are equipped with a topological space structure and that equality on `ι` is decidable.
More concisely: Given a continuous multilinear map `f` from a family of `R`-modules `M₁(ι)` to an `R`-module `M₂`, and a family `g` of functions mapping elements of a finite set `α` to `M₁(ι)`, the map `f` applied to the sum of `g(r)(i)` for all `i ∈ ι` and `r ∈ α`, is equal to the sum of `f(g(r))` for all `r ∈ α`.
|
ContinuousMultilinearMap.cont
theorem ContinuousMultilinearMap.cont :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
(self : ContinuousMultilinearMap R M₁ M₂), Continuous self.toFun
This theorem states that for any semiring `R`, any type `ι`, any types `M₁ : ι → Type` and `M₂ : Type`, under the conditions that for any `i : ι`, `M₁ i` forms an additive commutative monoid and is a module over `R`, and `M₂` forms an additive commutative monoid and is a module over `R`, and moreover, for any `i : ι`, `M₁ i` and `M₂` both have a topological structure, then, any continuous multilinear map from `∀ i, M₁ i` to `M₂` over the ring `R` is guaranteed to have a continuous function associated with it. In other words, the function corresponding to a continuous multilinear map is itself continuous.
More concisely: Given a semiring `R`, a type `ι`, types `M₁ : ι → Type` and `M₂ : Type` such that for all `i : ι`, `M₁ i` is an additive commutative monoid, a `R`-module, and topological space, `M₂` is an additive commutative monoid and `R`-module, and a topological space; any continuous multilinear map from `∀ i, M₁ i` to `M₂` over `R` has a continuous function associate.
|
ContinuousMultilinearMap.toMultilinearMap_injective
theorem ContinuousMultilinearMap.toMultilinearMap_injective :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂],
Function.Injective ContinuousMultilinearMap.toMultilinearMap
The theorem `ContinuousMultilinearMap.toMultilinearMap_injective` states that for any semiring `R`, any type `ι`, any type families `M₁ : ι → Type` and `M₂ : Type`, where `M₁ i` and `M₂` are additively commutative monoids and `R` modules, and `M₁ i` and `M₂` are topological spaces, the function `ContinuousMultilinearMap.toMultilinearMap` is injective. In other words, if two continuous multilinear maps between these spaces become the same after applying the function `toMultilinearMap` to them, then they were already the same to begin with.
More concisely: For any semiring `R`, given type families `M₁ : ι → Type`, `M₂ : Type` of additively commutative monoids and `R`-modules, and topological spaces `M₁ i` and `M₂`, the function `ContinuousMultilinearMap.toMultilinearMap` from continuous multilinear maps between them to multilinear maps is injective.
|
ContinuousMultilinearMap.ext
theorem ContinuousMultilinearMap.ext :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
{f f' : ContinuousMultilinearMap R M₁ M₂}, (∀ (x : (i : ι) → M₁ i), f x = f' x) → f = f'
The theorem states that for any semiring `R`, any type `ι`, and types `M₁` and `M₂` indexed by `ι` where each `M₁` is a module over `R` with an additive commutative monoid structure and a topology, and `M₂` is also a module over `R` with an additive commutative monoid structure and a topology, if `f` and `f'` are continuous multilinear maps from `M₁` to `M₂` over `R`, then `f` and `f'` are equal if and only if they are pointwise equal, i.e., `f x = f' x` for all `x` in the domain.
More concisely: Given any semiring `R`, types `ι`, `M₁`, and `M₂` indexed by `ι` with `M₁` and `M₂` being commutative `R`-modules with additive topologies, and continuous multilinear maps `f` and `f'` from `M₁` to `M₂` over `R`, `f` equals `f'` if and only if they are pointwise equal, i.e., `f x = f' x` for all `x` in the domain.
|
ContinuousMultilinearMap.map_smul_univ
theorem ContinuousMultilinearMap.map_smul_univ :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : CommSemiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : Fintype ι] (c : ι → R) (m : (i : ι) → M₁ i),
(f fun i => c i • m i) = (Finset.univ.prod fun i => c i) • f m
The theorem `ContinuousMultilinearMap.map_smul_univ` states that if `f` is a continuous multilinear map over a commutative semiring `R`, where the input space `M₁` is a module over `R` and is equipped with a topology (for each index `i` in `ι`), and the output space `M₂` is also a module over `R` and is equipped with a topology, then for any function `c` mapping each index to a scalar in `R` and any function `m` mapping each index to an element in the respective `M₁ i`, the value of `f` at the point obtained by scaling each `m i` by `c i` is equal to the result obtained by scaling the value of `f` at `m` by the product of all `c i`. This is an expression of the multiplicative behavior of `f` where scalars are moved outside of `f` with the caveat that they are all multiplied together.
More concisely: If `f` is a continuous multilinear map between modules over a commutative semiring, then for any scalars `ci` and vectors `mi` in the respective modules, `f(map (λ i, ci * mi) (map i m)) = prod ci * f m`.
|
ContinuousMultilinearMap.toMultilinearMap_add
theorem ContinuousMultilinearMap.toMultilinearMap_add :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
[inst_7 : ContinuousAdd M₂] (f g : ContinuousMultilinearMap R M₁ M₂),
(f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap
This theorem states that for any semiring `R`, any type `ι`, any type functions `M₁` from `ι` to some type `w₁`, any type `M₂`, under the conditions that for any `i` in `ι`, `M₁ i` forms an additive commutative monoid, `M₂` is also an additive commutative monoid, `M₁ i` and `M₂` are both `R`-modules, `M₁ i` and `M₂` both have a topological space structure, `M₂` supports continuous addition, and given two continuous multilinear maps `f` and `g` from `R` in the `M₁` space to the `M₂` space, the sum of `f` and `g` as a multilinear map equals the sum of `f` and `g` as multilinear maps separately. In other words, the process of converting a continuous multilinear map to a multilinear map commutes with the operation of addition.
More concisely: Given any semiring `R`, type `ι`, type functions `M₁ : ι → AddCommMonoid (R-Module topological_space)`, `M₂ : AddCommMonoid (R-Module topological_space)`, and continuous multilinear maps `f, g : R → M₁ i → M₂`, the sum of `f` and `g` as multilinear maps equals their pointwise sum.
|
ContinuousMultilinearMap.map_sum_finset
theorem ContinuousMultilinearMap.map_sum_finset :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [inst_7 : Fintype ι] (g : (i : ι) → α i → M₁ i)
(A : (i : ι) → Finset (α i)) [inst_8 : DecidableEq ι],
(f fun i => (A i).sum fun j => g i j) = (Fintype.piFinset A).sum fun r => f fun i => g i (r i)
This theorem states that if `f` is a continuous multilinear map, then the application of `f` on the sum of functions `g₁`, ..., `gₙ`, where each `gᵢ` sums over a finite set `Aᵢ`, is equal to the sum of `f` applied on the function `gᵢ` at every point `rᵢ` in `Aᵢ`. Here, the sum of `f (g₁ (r 1), ..., gₙ (r n))` is taken over all functions `r` such that `rᵢ` is in `Aᵢ` for every `i`. This result follows from the multilinearity of `f`, and the proof expands successively with respect to each coordinate. The theorem holds for any semiring `R`, any type `ι`, any modules `M₁` and `M₂` over `R`, and any topological spaces on `M₁` and `M₂`. The functions `gᵢ` map from type `αᵢ` to `M₁ᵢ`, and `Aᵢ` is a finite set of `αᵢ`.
More concisely: If `f` is a continuous multilinear map and `g₁, …, gₙ` are functions, each the sum over a finite set in their respective domains, then `f (∑xi∈Ai gi xi) = ∑i=1 to n ∑x∈Ai f gi xi`.
|
ContinuousMultilinearMap.cons_add
theorem ContinuousMultilinearMap.cons_add :
∀ {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
[inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (x y : M 0),
f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
This theorem states that for a continuous multilinear map `f`, defined over a semiring `R` and acting on spaces indexed by `Fin (n + 1)`, if we add two elements `x` and `y` from the initial space `M 0` and cons this sum to a tuple `m : (i : Fin n) → M i.succ` (where `succ` means the successor function in `Fin n`), this is equivalent to consing `x` and `y` individually to `m` and applying `f` to each, then adding these two results. This demonstrates the additivity of the multilinear map with respect to the first variable. The spaces `M i` and `M₂` have additional structures: they are modules over `R` and topological spaces.
More concisely: For a continuous multilinear map `f` over a semiring `R` with domains `M i` (finite-dimensional `R`-modules and topological spaces), the map `i => f (x i :: y :: m i.some_notion_of_cons)` equals `f (x :: m) + f (y :: m)`, where `x` and `y` are in `M 0` and `+` denotes the addition on `R`.
|
ContinuousMultilinearMap.cons_smul
theorem ContinuousMultilinearMap.cons_smul :
∀ {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
[inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (c : R) (x : M 0),
f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
This theorem states that for a certain kind of multilinear map, namely continuous multilinear maps on spaces indexed by `Fin (n+1)`, the map respects scalar multiplication along the first variable. Specifically, if we have such a multilinear map `f`, an `n`-tuple `m`, a scalar `c`, and an element `x` of the space at index 0, then applying `f` to the `n+1`-tuple constructed by consing `c • x` onto `m` gives the same result as first applying `f` to the `n+1`-tuple constructed by consing `x` onto `m`, and then scaling the result by `c`. This is a continuity property where the multilinear map commutes with the operation of scalar multiplication.
More concisely: For continuous multilinear maps on spaces indexed by `Fin (n+1)`, scalar multiplication along the first variable is commutative: `f (x :: m) * c = c * f (x :: m)`, where `f` is the multilinear map, `x` is an element in the space at index 0, `m` is an `n`-tuple, and `*` represents both scalar multiplication and function application.
|
ContinuousMultilinearMap.map_add_univ
theorem ContinuousMultilinearMap.map_add_univ :
∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
(f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (m m' : (i : ι) → M₁ i),
f (m + m') = Finset.univ.sum fun s => f (s.piecewise m m')
The theorem `ContinuousMultilinearMap.map_add_univ` says that for any semiring `R`, type `ι`, types `M₁` and `M₂` which are dependent on `ι`, with `M₁` and `M₂` having the structure of an additive commutative monoid, a module over `R`, and a topological space. If we also have a continuous multilinear map `f` from `M₁` to `M₂`, a decidable equality on `ι`, and `ι` is a finite type, then for any two functions `m` and `m'` from `ι` to `M₁`, the map applied to the sum of `m` and `m'` is equal to the sum, over all sets `s` in the universal set of `ι`, of `f` applied to `s` chosen piecewise from `m` and `m'`. In other words, the theorem states the additivity of a continuous multilinear map along all coordinates simultaneously.
More concisely: Given a semiring `R`, types `M₁` and `M₂` over `R` and a topological space, a decidable equality on a finite type `ι`, and a continuous multilinear map from `M₁` to `M₂`, for any functions `m` and `m'` from `ι` to `M₁`, the map applied to the sum of `m` and `m'` is equal to the sum of the maps applied to each function.
|