mathlibdocumentation

topology.algebra.module.multilinear

Continuous multilinear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define continuous multilinear maps as maps from `Π(i : ι), M₁ i` to `M₂` which are multilinear and continuous, by extending the space of multilinear maps with a continuity assumption. Here, `M₁ i` and `M₂` are modules over a ring `R`, and `ι` is an arbitrary type, and all these spaces are also topological spaces.

Main definitions #

• `continuous_multilinear_map R M₁ M₂` is the space of continuous multilinear maps from `Π(i : ι), M₁ i` to `M₂`. We show that it is an `R`-module.

Implementation notes #

We mostly follow the API of multilinear maps.

Notation #

We introduce the notation `M [×n]→L[R] M'` for the space of continuous `n`-multilinear maps from `M^n` to `M'`. This is a particular case of the general notion (where we allow varying dependent types as the arguments of our continuous multilinear maps), but arguably the most important one, especially when defining iterated derivatives.

structure continuous_multilinear_map (R : Type u) {ι : Type v} (M₁ : ι Type w₁) (M₂ : Type w₂) [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
Type (max v w₁ w₂)
• to_multilinear_map : M₁ M₂
• cont :

Continuous multilinear maps over the ring `R`, from `Πi, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules over `R` with a topological structure. In applications, there will be compatibility conditions between the algebraic and the topological structures, but this is not needed for the definition.

Instances for `continuous_multilinear_map`
theorem continuous_multilinear_map.to_multilinear_map_injective {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
@[protected, instance]
def continuous_multilinear_map.continuous_map_class {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
(Π (i : ι), M₁ i) M₂
Equations
@[protected, instance]
def continuous_multilinear_map.has_coe_to_fun {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
has_coe_to_fun M₂) (λ (_x : M₂), (Π (i : ι), M₁ i) M₂)
Equations
def continuous_multilinear_map.simps.apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (L₁ : M₂) (v : Π (i : ι), M₁ i) :
M₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
@[continuity]
theorem continuous_multilinear_map.coe_continuous {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) :
@[simp]
theorem continuous_multilinear_map.coe_coe {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) :
@[ext]
theorem continuous_multilinear_map.ext {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] {f f' : M₂} (H : (x : Π (i : ι), M₁ i), f x = f' x) :
f = f'
theorem continuous_multilinear_map.ext_iff {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] {f f' : M₂} :
f = f' (x : Π (i : ι), M₁ i), f x = f' x
@[simp]
theorem continuous_multilinear_map.map_add {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f i (x + y)) = f i x) + f i y)
@[simp]
theorem continuous_multilinear_map.map_smul {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i) :
f i (c x)) = c f i x)
theorem continuous_multilinear_map.map_coord_zero {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) {m : Π (i : ι), M₁ i} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem continuous_multilinear_map.map_zero {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [nonempty ι] :
f 0 = 0
@[protected, instance]
def continuous_multilinear_map.has_zero {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
has_zero M₂)
Equations
@[protected, instance]
def continuous_multilinear_map.inhabited {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
inhabited M₂)
Equations
@[simp]
theorem continuous_multilinear_map.zero_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (m : Π (i : ι), M₁ i) :
0 m = 0
@[simp]
theorem continuous_multilinear_map.to_multilinear_map_zero {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
@[protected, instance]
def continuous_multilinear_map.has_smul {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] :
has_smul R' M₂)
Equations
@[simp]
theorem continuous_multilinear_map.smul_apply {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] (f : M₂) (c : R') (m : Π (i : ι), M₁ i) :
(c f) m = c f m
@[simp]
theorem continuous_multilinear_map.to_multilinear_map_smul {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] (c : R') (f : M₂) :
@[protected, instance]
def continuous_multilinear_map.smul_comm_class {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [monoid R'] [monoid R''] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] [ M₂] [ M₂] [ R'' M₂] [ R'' M₂] :
R'' M₂)
@[protected, instance]
def continuous_multilinear_map.is_scalar_tower {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [monoid R'] [monoid R''] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] [ M₂] [ M₂] [ R'' M₂] [has_smul R' R''] [ R'' M₂] :
R'' M₂)
@[protected, instance]
def continuous_multilinear_map.is_central_scalar {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] [ M₂] [ M₂] :
M₂)
@[protected, instance]
def continuous_multilinear_map.mul_action {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂] :
M₂)
Equations
@[protected, instance]
def continuous_multilinear_map.has_add {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
Equations
@[simp]
theorem continuous_multilinear_map.add_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f f' : M₂) (m : Π (i : ι), M₁ i) :
(f + f') m = f m + f' m
@[simp]
theorem continuous_multilinear_map.to_multilinear_map_add {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f g : M₂) :
@[protected, instance]
def continuous_multilinear_map.add_comm_monoid {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
Equations
def continuous_multilinear_map.apply_add_hom {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (m : Π (i : ι), M₁ i) :
M₂ →+ M₂

Evaluation of a `continuous_multilinear_map` at a vector as an `add_monoid_hom`.

Equations
@[simp]
theorem continuous_multilinear_map.sum_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] {α : Type u_1} (f : α M₂) (m : Π (i : ι), M₁ i) {s : finset α} :
(s.sum (λ (a : α), f a)) m = s.sum (λ (a : α), (f a) m)
def continuous_multilinear_map.to_continuous_linear_map {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) :
M₁ i →L[R] M₂

If `f` is a continuous multilinear map, then `f.to_continuous_linear_map m i` is the continuous linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate.

Equations
def continuous_multilinear_map.prod {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] [Π (i : ι), topological_space (M₁ i)] (f : M₂) (g : M₃) :
(M₂ × M₃)

The cartesian product of two continuous multilinear maps, as a continuous multilinear map.

Equations
@[simp]
theorem continuous_multilinear_map.prod_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] [Π (i : ι), topological_space (M₁ i)] (f : M₂) (g : M₃) (m : Π (i : ι), M₁ i) :
(f.prod g) m = (f m, g m)
def continuous_multilinear_map.pi {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), (M' i)) :
(Π (i : ι'), M' i)

Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a continuous multilinear map taking values in the space of functions `Π i, M' i`.

Equations
@[simp]
theorem continuous_multilinear_map.coe_pi {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), (M' i)) :
= λ (m : Π (i : ι), M₁ i) (j : ι'), (f j) m
theorem continuous_multilinear_map.pi_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), (M' i)) (m : Π (i : ι), M₁ i) (j : ι') :
= (f j) m
@[simp]
theorem continuous_multilinear_map.of_subsingleton_apply (R : Type u) {ι : Type v} (M₂ : Type w₂) [semiring R] [add_comm_monoid M₂] [ M₂] [subsingleton ι] (i' : ι) (f : Π (x : ι), (λ (i : ι), M₂) x) :
f = f i'
@[simp]
theorem continuous_multilinear_map.of_subsingleton_to_multilinear_map (R : Type u) {ι : Type v} (M₂ : Type w₂) [semiring R] [add_comm_monoid M₂] [ M₂] [subsingleton ι] (i' : ι) :
def continuous_multilinear_map.of_subsingleton (R : Type u) {ι : Type v} (M₂ : Type w₂) [semiring R] [add_comm_monoid M₂] [ M₂] [subsingleton ι] (i' : ι) :
(λ (_x : ι), M₂) M₂

The evaluation map from `ι → M₂` to `M₂` is multilinear at a given `i` when `ι` is subsingleton.

Equations
@[simp]
theorem continuous_multilinear_map.const_of_is_empty_to_multilinear_map (R : Type u) {ι : Type v} (M₁ : ι Type w₁) {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [is_empty ι] (m : M₂) :
def continuous_multilinear_map.const_of_is_empty (R : Type u) {ι : Type v} (M₁ : ι Type w₁) {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [is_empty ι] (m : M₂) :
M₂

The constant map is multilinear when `ι` is empty.

Equations
@[simp]
theorem continuous_multilinear_map.const_of_is_empty_apply (R : Type u) {ι : Type v} (M₁ : ι Type w₁) {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [is_empty ι] (m : M₂) (ᾰ : Π (i : ι), M₁ i) :
= m
def continuous_multilinear_map.comp_continuous_linear_map {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₁' : ι Type w₁'} {M₄ : Type w₄} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), add_comm_monoid (M₁' i)] [add_comm_monoid M₄] [Π (i : ι), (M₁ i)] [Π (i : ι), (M₁' i)] [ M₄] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), topological_space (M₁' i)] (g : M₄) (f : Π (i : ι), M₁ i →L[R] M₁' i) :
M₄

If `g` is continuous multilinear and `f` is a collection of continuous linear maps, then `g (f₁ m₁, ..., fₙ mₙ)` is again a continuous multilinear map, that we call `g.comp_continuous_linear_map f`.

Equations
@[simp]
theorem continuous_multilinear_map.comp_continuous_linear_map_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₁' : ι Type w₁'} {M₄ : Type w₄} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), add_comm_monoid (M₁' i)] [add_comm_monoid M₄] [Π (i : ι), (M₁ i)] [Π (i : ι), (M₁' i)] [ M₄] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), topological_space (M₁' i)] (g : M₄) (f : Π (i : ι), M₁ i →L[R] M₁' i) (m : Π (i : ι), M₁ i) :
m = g (λ (i : ι), (f i) (m i))
def continuous_linear_map.comp_continuous_multilinear_map {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] [Π (i : ι), topological_space (M₁ i)] (g : M₂ →L[R] M₃) (f : M₂) :
M₃

Composing a continuous multilinear map with a continuous linear map gives again a continuous multilinear map.

Equations
@[simp]
theorem continuous_linear_map.comp_continuous_multilinear_map_coe {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] [Π (i : ι), topological_space (M₁ i)] (g : M₂ →L[R] M₃) (f : M₂) :
@[simp]
theorem continuous_multilinear_map.pi_equiv_symm_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] (f : (Π (i : ι'), M' i)) (i : ι') :
def continuous_multilinear_map.pi_equiv {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] :
(Π (i : ι'), (M' i)) (Π (i : ι'), M' i)

`continuous_multilinear_map.pi` as an `equiv`.

Equations
@[simp]
theorem continuous_multilinear_map.pi_equiv_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] [Π (i : ι), topological_space (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), ((λ (i : ι'), M' i) i)) :
theorem continuous_multilinear_map.cons_add {R : Type u} {n : } {M : fin n.succ Type w} {M₂ : Type w₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] [Π (i : fin n.succ), topological_space (M i)] (f : 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)

In the specific case of continuous multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the additivity of a multilinear map along the first variable.

theorem continuous_multilinear_map.cons_smul {R : Type u} {n : } {M : fin n.succ Type w} {M₂ : Type w₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] [Π (i : fin n.succ), topological_space (M i)] (f : 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)

In the specific case of continuous multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the multiplicativity of a multilinear map along the first variable.

theorem continuous_multilinear_map.map_piecewise_add {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (m m' : Π (i : ι), M₁ i) (t : finset ι) :
f (t.piecewise (m + m') m') = t.powerset.sum (λ (s : finset ι), f (s.piecewise m m'))
theorem continuous_multilinear_map.map_add_univ {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] [fintype ι] (m m' : Π (i : ι), M₁ i) :
f (m + m') = finset.univ.sum (λ (s : finset ι), f (s.piecewise m m'))

Additivity of a continuous multilinear map along all coordinates at the same time, writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`.

theorem continuous_multilinear_map.map_sum_finset {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) {α : ι Type u_1} [fintype ι] (g : Π (i : ι), α i M₁ i) (A : Π (i : ι), finset (α i)) [decidable_eq ι] :
f (λ (i : ι), (A i).sum (λ (j : α i), g i j)) = .sum (λ (r : Π (a : ι), α a), f (λ (i : ι), g i (r i)))

If `f` is continuous multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ..., `r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each coordinate.

theorem continuous_multilinear_map.map_sum {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) {α : ι Type u_1} [fintype ι] (g : Π (i : ι), α i M₁ i) [decidable_eq ι] [Π (i : ι), fintype (α i)] :
f (λ (i : ι), finset.univ.sum (λ (j : α i), g i j)) = finset.univ.sum (λ (r : Π (i : ι), α i), f (λ (i : ι), g i (r i)))

If `f` is continuous multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from multilinearity by expanding successively with respect to each coordinate.

def continuous_multilinear_map.restrict_scalars (R : Type u) {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] {A : Type u_1} [semiring A] [ A] [Π (i : ι), (M₁ i)] [ M₂] [ (i : ι), (M₁ i)] [ M₂] (f : M₂) :
M₂

Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R` and their actions on all involved modules agree with the action of `R` on `A`.

Equations
@[simp]
theorem continuous_multilinear_map.coe_restrict_scalars (R : Type u) {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] {A : Type u_1} [semiring A] [ A] [Π (i : ι), (M₁ i)] [ M₂] [ (i : ι), (M₁ i)] [ M₂] (f : M₂) :
@[simp]
theorem continuous_multilinear_map.map_sub {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f i (x - y)) = f i x) - f i y)
@[protected, instance]
def continuous_multilinear_map.has_neg {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
has_neg M₂)
Equations
@[simp]
theorem continuous_multilinear_map.neg_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) (m : Π (i : ι), M₁ i) :
(-f) m = -f m
@[protected, instance]
def continuous_multilinear_map.has_sub {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
has_sub M₂)
Equations
@[simp]
theorem continuous_multilinear_map.sub_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f f' : M₂) (m : Π (i : ι), M₁ i) :
(f - f') m = f m - f' m
@[protected, instance]
def continuous_multilinear_map.add_comm_group {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)]  :
Equations
theorem continuous_multilinear_map.map_piecewise_smul {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [decidable_eq ι] (c : ι R) (m : Π (i : ι), M₁ i) (s : finset ι) :
f (s.piecewise (λ (i : ι), c i m i) m) = s.prod (λ (i : ι), c i) f m
theorem continuous_multilinear_map.map_smul_univ {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] (f : M₂) [fintype ι] (c : ι R) (m : Π (i : ι), M₁ i) :
f (λ (i : ι), c i m i) = finset.univ.prod (λ (i : ι), c i) f m

Multiplicativity of a continuous multilinear map along all coordinates at the same time, writing `f (λ i, c i • m i)` as `(∏ i, c i) • f m`.

@[protected, instance]
def continuous_multilinear_map.distrib_mul_action {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_3} [monoid R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ M₂] [ R' M₂]  :
M₂)
Equations
@[protected, instance]
def continuous_multilinear_map.module {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] [ M₂] [module R' M₂] [ M₂] [ R' M₂] :
module R' M₂)

The space of continuous multilinear maps over an algebra over `R` is a module over `R`, for the pointwise addition and scalar multiplication.

Equations
def continuous_multilinear_map.to_multilinear_map_linear {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] [ M₂] [module R' M₂] [ M₂] [ R' M₂] :
M₂ →ₗ[R'] M₁ M₂

Linear map version of the map `to_multilinear_map` associating to a continuous multilinear map the corresponding multilinear map.

Equations
@[simp]
theorem continuous_multilinear_map.to_multilinear_map_linear_apply {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] [ M₂] [module R' M₂] [ M₂] [ R' M₂] (self : M₂) :
@[simp]
theorem continuous_multilinear_map.pi_linear_equiv_apply {ι : Type v} {M₁ : ι Type w₁} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] {ι' : Type u_3} {M' : ι' Type u_4} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [ (i : ι'), has_continuous_add (M' i)] [Π (i : ι'), module R' (M' i)] [Π (i : ι'), (M' i)] [ (i : ι'), R' (M' i)] [ (i : ι'), (M' i)] (ᾰ : Π (i : ι'), (M' i)) :
@[simp]
theorem continuous_multilinear_map.pi_linear_equiv_symm_apply {ι : Type v} {M₁ : ι Type w₁} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] {ι' : Type u_3} {M' : ι' Type u_4} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [ (i : ι'), has_continuous_add (M' i)] [Π (i : ι'), module R' (M' i)] [Π (i : ι'), (M' i)] [ (i : ι'), R' (M' i)] [ (i : ι'), (M' i)] (ᾰ : (Π (i : ι'), M' i)) (i : ι') :
def continuous_multilinear_map.pi_linear_equiv {ι : Type v} {M₁ : ι Type w₁} {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), (M₁ i)] {ι' : Type u_3} {M' : ι' Type u_4} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), topological_space (M' i)] [ (i : ι'), has_continuous_add (M' i)] [Π (i : ι'), module R' (M' i)] [Π (i : ι'), (M' i)] [ (i : ι'), R' (M' i)] [ (i : ι'), (M' i)] :
(Π (i : ι'), (M' i)) ≃ₗ[R'] (Π (i : ι'), M' i)

`continuous_multilinear_map.pi` as a `linear_equiv`.

Equations
@[protected]
def continuous_multilinear_map.mk_pi_algebra (R : Type u) (ι : Type v) (A : Type u_1) [fintype ι] [ A]  :
(λ (i : ι), A) A

The continuous multilinear map on `A^ι`, where `A` is a normed commutative algebra over `𝕜`, associating to `m` the product of all the `m i`.

See also `continuous_multilinear_map.mk_pi_algebra_fin`.

Equations
@[simp]
theorem continuous_multilinear_map.mk_pi_algebra_apply (R : Type u) (ι : Type v) (A : Type u_1) [fintype ι] [ A] (m : ι A) :
= finset.univ.prod (λ (i : ι), m i)
@[protected]
def continuous_multilinear_map.mk_pi_algebra_fin (R : Type u) (n : ) (A : Type u_1) [semiring A] [ A]  :
(λ (i : fin n), A) A

The continuous multilinear map on `A^n`, where `A` is a normed algebra over `𝕜`, associating to `m` the product of all the `m i`.

See also: `continuous_multilinear_map.mk_pi_algebra`.

Equations
@[simp]
theorem continuous_multilinear_map.mk_pi_algebra_fin_apply {R : Type u} {n : } {A : Type u_1} [semiring A] [ A] (m : fin n A) :
@[simp]
theorem continuous_multilinear_map.smul_right_to_multilinear_map {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [ M₂] (f : R) (z : M₂) :
@[simp]
theorem continuous_multilinear_map.smul_right_apply {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [ M₂] (f : R) (z : M₂) (ᾰ : Π (i : ι), M₁ i) :
(f.smul_right z) = f ᾰ z
def continuous_multilinear_map.smul_right {R : Type u} {ι : Type v} {M₁ : ι Type w₁} {M₂ : Type w₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [Π (i : ι), topological_space (M₁ i)] [ M₂] (f : R) (z : M₂) :
M₂

Given a continuous `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the continuous multilinear map sending `m` to `f m • z`.

Equations