Continuous multilinear maps #

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 #

• ContinuousMultilinearMap 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 ContinuousMultilinearMap (R : Type u) {ι : Type v} (M₁ : ιType w₁) (M₂ : Type w₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] extends :
Type (max (max v w₁) w₂)

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.

• toFun : ((i : ι) → M₁ i)M₂
• map_add' : ∀ [inst : ] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), self.toFun (Function.update m i (x + y)) = self.toFun () + self.toFun ()
• map_smul' : ∀ [inst : ] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), self.toFun (Function.update m i (c x)) = c self.toFun ()
• cont : Continuous self.toFun

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 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ContinuousMultilinearMap.toMultilinearMap_injective {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
Function.Injective ContinuousMultilinearMap.toMultilinearMap
instance ContinuousMultilinearMap.funLike {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
FunLike () ((i : ι) → M₁ i) M₂
Equations
• ContinuousMultilinearMap.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance ContinuousMultilinearMap.continuousMapClass {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
ContinuousMapClass () ((i : ι) → M₁ i) M₂
Equations
• =
instance ContinuousMultilinearMap.instCoeFunContinuousMultilinearMapForAllForAll {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
CoeFun () fun (x : ) => ((i : ι) → M₁ i)M₂
Equations
• ContinuousMultilinearMap.instCoeFunContinuousMultilinearMapForAllForAll = { coe := fun (f : ) => f }
def ContinuousMultilinearMap.Simps.apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (L₁ : ) (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
Instances For
theorem ContinuousMultilinearMap.coe_continuous {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) :
@[simp]
theorem ContinuousMultilinearMap.coe_coe {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) :
f.toMultilinearMap = f
theorem ContinuousMultilinearMap.ext {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] {f : } {f' : } (H : ∀ (x : (i : ι) → M₁ i), f x = f' x) :
f = f'
theorem ContinuousMultilinearMap.ext_iff {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] {f : } {f' : } :
f = f' ∀ (x : (i : ι) → M₁ i), f x = f' x
@[simp]
theorem ContinuousMultilinearMap.map_add {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
f (Function.update m i (x + y)) = f () + f ()
@[simp]
theorem ContinuousMultilinearMap.map_smul {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (Function.update m i (c x)) = c f ()
theorem ContinuousMultilinearMap.map_coord_zero {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) {m : (i : ι) → M₁ i} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem ContinuousMultilinearMap.map_zero {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] :
f 0 = 0
instance ContinuousMultilinearMap.instZeroContinuousMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
Zero ()
Equations
• ContinuousMultilinearMap.instZeroContinuousMultilinearMap = { zero := let __src := 0; { toMultilinearMap := __src, cont := } }
instance ContinuousMultilinearMap.instInhabitedContinuousMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
Equations
• ContinuousMultilinearMap.instInhabitedContinuousMultilinearMap = { default := 0 }
@[simp]
theorem ContinuousMultilinearMap.zero_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (m : (i : ι) → M₁ i) :
0 m = 0
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_zero {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] :
0.toMultilinearMap = 0
instance ContinuousMultilinearMap.instSMulContinuousMultilinearMap {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {A : Type u_3} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] :
SMul R' ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ContinuousMultilinearMap.smul_apply {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {A : Type u_3} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] (f : ) (c : R') (m : (i : ι) → M₁ i) :
(c f) m = c f m
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_smul {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {A : Type u_3} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] (c : R') (f : ) :
(c f).toMultilinearMap = c f.toMultilinearMap
instance ContinuousMultilinearMap.instSMulCommClassContinuousMultilinearMapInstSMulContinuousMultilinearMapInstSMulContinuousMultilinearMap {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [Monoid R'] [Monoid R''] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] [DistribMulAction R'' M₂] [ContinuousConstSMul R'' M₂] [SMulCommClass A R'' M₂] [SMulCommClass R' R'' M₂] :
SMulCommClass R' R'' ()
Equations
• =
instance ContinuousMultilinearMap.instIsScalarTowerContinuousMultilinearMapInstSMulContinuousMultilinearMapInstSMulContinuousMultilinearMap {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [Monoid R'] [Monoid R''] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] [DistribMulAction R'' M₂] [ContinuousConstSMul R'' M₂] [SMulCommClass A R'' M₂] [SMul R' R''] [IsScalarTower R' R'' M₂] :
IsScalarTower R' R'' ()
Equations
• =
instance ContinuousMultilinearMap.instMulActionContinuousMultilinearMap {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] {R' : Type u_1} {A : Type u_3} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] :
MulAction R' ()
Equations
instance ContinuousMultilinearMap.instAddContinuousMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ContinuousMultilinearMap.add_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) (f' : ) [] (m : (i : ι) → M₁ i) :
(f + f') m = f m + f' m
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_add {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (g : ) :
(f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap
instance ContinuousMultilinearMap.addCommMonoid {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] :
Equations
def ContinuousMultilinearMap.applyAddHom {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (m : (i : ι) → M₁ i) :
→+ M₂

Evaluation of a ContinuousMultilinearMap at a vector as an AddMonoidHom.

Equations
• = { toZeroHom := { toFun := fun (f : ) => f m, map_zero' := }, map_add' := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.sum_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] {α : Type u_1} (f : α) (m : (i : ι) → M₁ i) {s : } :
(Finset.sum s fun (a : α) => f a) m = Finset.sum s fun (a : α) => (f a) m
def ContinuousMultilinearMap.toContinuousLinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) (i : ι) :
M₁ i →L[R] M₂

If f is a continuous multilinear map, then f.toContinuousLinearMap 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
Instances For
def ContinuousMultilinearMap.prod {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {M₃ : Type w₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (g : ) :
ContinuousMultilinearMap R M₁ (M₂ × M₃)

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

Equations
• = let __src := MultilinearMap.prod f.toMultilinearMap g.toMultilinearMap; { toMultilinearMap := __src, cont := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.prod_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {M₃ : Type w₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (g : ) (m : (i : ι) → M₁ i) :
= (f m, g m)
def ContinuousMultilinearMap.pi {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)) :
ContinuousMultilinearMap R M₁ ((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
• = { toMultilinearMap := MultilinearMap.pi fun (i : ι') => (f i).toMultilinearMap, cont := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.coe_pi {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)) :
= fun (m : (i : ι) → M₁ i) (j : ι') => (f j) m
theorem ContinuousMultilinearMap.pi_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)) (m : (i : ι) → M₁ i) (j : ι') :
= (f j) m
@[simp]
theorem ContinuousMultilinearMap.codRestrict_apply_coe {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) (v : (i : ι) → M₁ i) :
( v) = f v
@[simp]
theorem ContinuousMultilinearMap.codRestrict_toMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :
.toMultilinearMap = MultilinearMap.codRestrict f.toMultilinearMap p h
def ContinuousMultilinearMap.codRestrict {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :

Restrict the codomain of a continuous multilinear map to a submodule.

Equations
Instances For
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_apply_apply (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [] [] [] [Module R M₂] [Module R M₃] [] [] [] (i : ι) (f : M₂ →L[R] M₃) (x : ιM₂) :
(() f) x = f (x i)
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [] [] [] [Module R M₂] [Module R M₃] [] [] [] (i : ι) (f : M₂ →L[R] M₃) :
(() f).toMultilinearMap = () f
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [] [] [] [Module R M₂] [Module R M₃] [] [] [] (i : ι) (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) (x : M₂) :
(().symm f) x = f fun (x_1 : ι) => x
def ContinuousMultilinearMap.ofSubsingleton (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [] [] [] [Module R M₂] [Module R M₃] [] [] [] (i : ι) :
(M₂ →L[R] M₃) ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃

The natural equivalence between continuous linear maps from M₂ to M₃ and continuous 1-multilinear maps from M₂ to M₃.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousMultilinearMap.constOfIsEmpty_apply (R : Type u) {ι : Type v} (M₁ : ιType w₁) {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (m : M₂) :
∀ (a : (i : ι) → M₁ i), a = m
@[simp]
theorem ContinuousMultilinearMap.constOfIsEmpty_toMultilinearMap (R : Type u) {ι : Type v} (M₁ : ιType w₁) {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (m : M₂) :
.toMultilinearMap =
def ContinuousMultilinearMap.constOfIsEmpty (R : Type u) {ι : Type v} (M₁ : ιType w₁) {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (m : M₂) :

The constant map is multilinear when ι is empty.

Equations
• = { toMultilinearMap := , cont := }
Instances For
def ContinuousMultilinearMap.compContinuousLinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₁' : ιType w₁'} {M₄ : Type w₄} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → AddCommMonoid (M₁' i)] [] [(i : ι) → Module R (M₁ i)] [(i : ι) → Module R (M₁' i)] [Module R M₄] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → TopologicalSpace (M₁' i)] [] (g : ContinuousMultilinearMap R M₁' M₄) (f : (i : ι) → M₁ i →L[R] M₁' i) :

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.compContinuousLinearMap f.

Equations
Instances For
@[simp]
theorem ContinuousMultilinearMap.compContinuousLinearMap_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₁' : ιType w₁'} {M₄ : Type w₄} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → AddCommMonoid (M₁' i)] [] [(i : ι) → Module R (M₁ i)] [(i : ι) → Module R (M₁' i)] [Module R M₄] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → TopologicalSpace (M₁' i)] [] (g : ContinuousMultilinearMap R M₁' M₄) (f : (i : ι) → M₁ i →L[R] M₁' i) (m : (i : ι) → M₁ i) :
= g fun (i : ι) => (f i) (m i)
def ContinuousLinearMap.compContinuousMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {M₃ : Type w₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (g : M₂ →L[R] M₃) (f : ) :

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

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.compContinuousMultilinearMap_coe {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {M₃ : Type w₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (g : M₂ →L[R] M₃) (f : ) :
= g f
@[simp]
theorem ContinuousMultilinearMap.piEquiv_symm_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)) (i : ι') :
ContinuousMultilinearMap.piEquiv.symm f i =
@[simp]
theorem ContinuousMultilinearMap.piEquiv_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)) :
ContinuousMultilinearMap.piEquiv f =
def ContinuousMultilinearMap.piEquiv {R : Type u} {ι : Type v} {M₁ : ιType w₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [(i : ι') → Module R (M' i)] :
((i : ι') → ContinuousMultilinearMap R M₁ (M' i)) ContinuousMultilinearMap R M₁ ((i : ι') → M' i)

ContinuousMultilinearMap.pi as an Equiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousMultilinearMap.domDomCongr_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) (v : ι'M₂) :
= f fun (i : ι) => v (e i)
@[simp]
theorem ContinuousMultilinearMap.domDomCongr_toMultilinearMap {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) :
.toMultilinearMap = MultilinearMap.domDomCongr e f.toMultilinearMap
def ContinuousMultilinearMap.domDomCongr {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) :
ContinuousMultilinearMap R (fun (x : ι') => M₂) M₃

An equivalence of the index set defines an equivalence between the spaces of continuous multilinear maps. This is the forward map of this equivalence.

Equations
Instances For
@[simp]
theorem ContinuousMultilinearMap.domDomCongrEquiv_symm_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') (f : ContinuousMultilinearMap R (fun (x : ι') => M₂) M₃) :
=
@[simp]
theorem ContinuousMultilinearMap.domDomCongrEquiv_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) :
def ContinuousMultilinearMap.domDomCongrEquiv {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [] [] [] [Module R M₂] [Module R M₃] [] [] {ι' : Type u_1} (e : ι ι') :
ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃ ContinuousMultilinearMap R (fun (x : ι') => M₂) M₃

An equivalence of the index set defines an equivalence between the spaces of continuous multilinear maps. In case of normed spaces, this is a linear isometric equivalence, see ContinuousMultilinearMap.domDomCongrₗᵢ.

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
def ContinuousMultilinearMap.linearDeriv {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] [] [] (x : (i : ι) → M₁ i) :
((i : ι) → M₁ i) →L[R] M₂

The derivative of a continuous multilinear map, as a continuous linear map from ∀ i, M₁ i to M₂; see ContinuousMultilinearMap.hasFDerivAt.

Equations
Instances For
@[simp]
theorem ContinuousMultilinearMap.linearDeriv_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] [] [] (x : (i : ι) → M₁ i) (y : (i : ι) → M₁ i) :
= Finset.sum Finset.univ fun (i : ι) => f (Function.update x i (y i))
theorem ContinuousMultilinearMap.cons_add {R : Type u} {n : } {M : Fin ()Type w} {M₂ : Type w₂} [] [(i : Fin ()) → AddCommMonoid (M i)] [] [(i : Fin ()) → Module R (M i)] [Module R M₂] [(i : Fin ()) → TopologicalSpace (M i)] [] (f : ) (m : (i : Fin n) → M ()) (x : M 0) (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 ContinuousMultilinearMap.cons_smul {R : Type u} {n : } {M : Fin ()Type w} {M₂ : Type w₂} [] [(i : Fin ()) → AddCommMonoid (M i)] [] [(i : Fin ()) → Module R (M i)] [Module R M₂] [(i : Fin ()) → TopologicalSpace (M i)] [] (f : ) (m : (i : Fin n) → M ()) (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 ContinuousMultilinearMap.map_piecewise_add {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) (t : ) :
f (Finset.piecewise t (m + m') m') = Finset.sum () fun (s : ) => f (Finset.piecewise s m m')
theorem ContinuousMultilinearMap.map_add_univ {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] [] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) :
f (m + m') = Finset.sum Finset.univ fun (s : ) => f (Finset.piecewise s 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 ContinuousMultilinearMap.map_sum_finset {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) {α : ιType u_1} [] (g : (i : ι) → α iM₁ i) (A : (i : ι) → Finset (α i)) [] :
(f fun (i : ι) => Finset.sum (A i) fun (j : α i) => g i j) = Finset.sum () fun (r : (a : ι) → α a) => f fun (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 ContinuousMultilinearMap.map_sum {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) {α : ιType u_1} [] (g : (i : ι) → α iM₁ i) [] [(i : ι) → Fintype (α i)] :
(f fun (i : ι) => Finset.sum Finset.univ fun (j : α i) => g i j) = Finset.sum Finset.univ fun (r : (i : ι) → α i) => f fun (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 ContinuousMultilinearMap.restrictScalars (R : Type u) {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] {A : Type u_1} [] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : ) :

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
Instances For
@[simp]
theorem ContinuousMultilinearMap.coe_restrictScalars (R : Type u) {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] {A : Type u_1} [] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : ) :
@[simp]
theorem ContinuousMultilinearMap.map_sub {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
f (Function.update m i (x - y)) = f () - f ()
instance ContinuousMultilinearMap.instNegContinuousMultilinearMapToSemiringToAddCommMonoidToAddCommMonoid {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] :
Neg ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ContinuousMultilinearMap.neg_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (m : (i : ι) → M₁ i) :
(-f) m = -f m
instance ContinuousMultilinearMap.instSubContinuousMultilinearMapToSemiringToAddCommMonoidToAddCommMonoid {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] :
Sub ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ContinuousMultilinearMap.sub_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) (f' : ) [] (m : (i : ι) → M₁ i) :
(f - f') m = f m - f' m
instance ContinuousMultilinearMap.instAddCommGroupContinuousMultilinearMapToSemiringToAddCommMonoidToAddCommMonoid {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] [] :
Equations
theorem ContinuousMultilinearMap.map_piecewise_smul {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (c : ιR) (m : (i : ι) → M₁ i) (s : ) :
f (Finset.piecewise s (fun (i : ι) => c i m i) m) = (Finset.prod s fun (i : ι) => c i) f m
theorem ContinuousMultilinearMap.map_smul_univ {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [] (f : ) [] (c : ιR) (m : (i : ι) → M₁ i) :
(f fun (i : ι) => c i m i) = (Finset.prod Finset.univ fun (i : ι) => c i) f m

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

instance ContinuousMultilinearMap.instDistribMulActionContinuousMultilinearMapToAddMonoidAddCommMonoid {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_3} [Monoid R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [] [SMulCommClass A R' M₂] [] :
Equations
• One or more equations did not get rendered due to their size.
instance ContinuousMultilinearMap.instModuleContinuousMultilinearMapAddCommMonoid {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [] [SMulCommClass A R' M₂] :
Module R' ()

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMapLinear_apply {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [] [SMulCommClass A R' M₂] (self : ) :
ContinuousMultilinearMap.toMultilinearMapLinear self = self.toMultilinearMap
def ContinuousMultilinearMap.toMultilinearMapLinear {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [] [SMulCommClass A R' M₂] :
→ₗ[R'] MultilinearMap A M₁ M₂

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

Equations
• ContinuousMultilinearMap.toMultilinearMapLinear = { toAddHom := { toFun := ContinuousMultilinearMap.toMultilinearMap, map_add' := }, map_smul' := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.piLinearEquiv_apply {ι : Type v} {M₁ : ιType w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → Module A (M₁ i)] {ι' : Type u_3} {M' : ι'Type u_4} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R' (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R' (M' i)] [∀ (i : ι'), ContinuousConstSMul R' (M' i)] :
∀ (a : (i : ι') → ContinuousMultilinearMap A M₁ (M' i)), ContinuousMultilinearMap.piLinearEquiv a =
@[simp]
theorem ContinuousMultilinearMap.piLinearEquiv_symm_apply {ι : Type v} {M₁ : ιType w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → Module A (M₁ i)] {ι' : Type u_3} {M' : ι'Type u_4} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R' (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R' (M' i)] [∀ (i : ι'), ContinuousConstSMul R' (M' i)] :
∀ (a : ContinuousMultilinearMap A M₁ ((i : ι') → M' i)) (i : ι'), (LinearEquiv.symm ContinuousMultilinearMap.piLinearEquiv) a i =
def ContinuousMultilinearMap.piLinearEquiv {ι : Type v} {M₁ : ιType w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → Module A (M₁ i)] {ι' : Type u_3} {M' : ι'Type u_4} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → TopologicalSpace (M' i)] [∀ (i : ι'), ContinuousAdd (M' i)] [(i : ι') → Module R' (M' i)] [(i : ι') → Module A (M' i)] [∀ (i : ι'), SMulCommClass A R' (M' i)] [∀ (i : ι'), ContinuousConstSMul R' (M' i)] :
((i : ι') → ContinuousMultilinearMap A M₁ (M' i)) ≃ₗ[R'] ContinuousMultilinearMap A M₁ ((i : ι') → M' i)

ContinuousMultilinearMap.pi as a LinearEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def ContinuousMultilinearMap.mkPiAlgebra (R : Type u) (ι : Type v) (A : Type u_1) [] [] [] [Algebra R A] [] [] :
ContinuousMultilinearMap R (fun (x : ι) => 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 ContinuousMultilinearMap.mkPiAlgebraFin.

Equations
• = { toMultilinearMap := , cont := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.mkPiAlgebra_apply (R : Type u) (ι : Type v) (A : Type u_1) [] [] [] [Algebra R A] [] [] (m : ιA) :
m = Finset.prod Finset.univ fun (i : ι) => m i
def ContinuousMultilinearMap.mkPiAlgebraFin (R : Type u) (n : ) (A : Type u_1) [] [] [Algebra R A] [] [] :
ContinuousMultilinearMap R (fun (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: ContinuousMultilinearMap.mkPiAlgebra.

Equations
• = { toMultilinearMap := , cont := }
Instances For
@[simp]
theorem ContinuousMultilinearMap.mkPiAlgebraFin_apply {R : Type u} {n : } {A : Type u_1} [] [] [Algebra R A] [] [] (m : Fin nA) :
=
@[simp]
theorem ContinuousMultilinearMap.smulRight_apply {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (z : M₂) :
∀ (a : (i : ι) → M₁ i), = f a z
@[simp]
theorem ContinuousMultilinearMap.smulRight_toMultilinearMap {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (z : M₂) :
.toMultilinearMap = MultilinearMap.smulRight f.toMultilinearMap z
def ContinuousMultilinearMap.smulRight {R : Type u} {ι : Type v} {M₁ : ιType w₁} {M₂ : Type w₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] [(i : ι) → TopologicalSpace (M₁ i)] [] [] (f : ) (z : M₂) :

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

Equations
Instances For
def ContinuousMultilinearMap.mkPiRing (R : Type u) (ι : Type v) {M : Type u_1} [] [] [] [Module R M] [] [] [] [] (z : M) :
ContinuousMultilinearMap R (fun (x : ι) => R) M

The canonical continuous multilinear map on R^ι, associating to m the product of all the m i (multiplied by a fixed reference element z in the target module)

Equations
Instances For
@[simp]
theorem ContinuousMultilinearMap.mkPiRing_apply {R : Type u} {ι : Type v} {M : Type u_1} [] [] [] [Module R M] [] [] [] [] (z : M) (m : ιR) :
m = (Finset.prod Finset.univ fun (i : ι) => m i) z
theorem ContinuousMultilinearMap.mkPiRing_apply_one_eq_self {R : Type u} {ι : Type v} {M : Type u_1} [] [] [] [Module R M] [] [] [] [] (f : ContinuousMultilinearMap R (fun (x : ι) => R) M) :
ContinuousMultilinearMap.mkPiRing R ι (f fun (x : ι) => 1) = f
theorem ContinuousMultilinearMap.mkPiRing_eq_iff {R : Type u} {ι : Type v} {M : Type u_1} [] [] [] [Module R M] [] [] [] [] {z₁ : M} {z₂ : M} :
z₁ = z₂
theorem ContinuousMultilinearMap.mkPiRing_zero {R : Type u} {ι : Type v} {M : Type u_1} [] [] [] [Module R M] [] [] [] [] :
theorem ContinuousMultilinearMap.mkPiRing_eq_zero_iff {R : Type u} {ι : Type v} {M : Type u_1} [] [] [] [Module R M] [] [] [] [] (z : M) :
z = 0