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

source
structure ContinuousMultilinearMap (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) (M₂ : Type w₂) [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] extends MultilinearMap R M₁ M₂ :
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_update_add' [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i) : self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)
- map_update_smul' [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) : self.toFun (Function.update m i (c • x)) = c • self.toFun (Function.update m i x)
- 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

source
def «term_[×_]→L[_]_» :
Lean.TrailingParserDescr

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

source
theorem ContinuousMultilinearMap.toMultilinearMap_injective {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
Function.Injective toMultilinearMap
source
instance ContinuousMultilinearMap.funLike {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
FunLike (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
Equations

- ContinuousMultilinearMap.funLike = { coe := fun (f : ContinuousMultilinearMap R M₁ M₂) => f.toFun, coe_injective' := ⋯ }

source
instance ContinuousMultilinearMap.continuousMapClass {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
source
def ContinuousMultilinearMap.Simps.apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (L₁ : ContinuousMultilinearMap R M₁ 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

- ContinuousMultilinearMap.Simps.apply L₁ v = L₁ v

Instances For

source
theorem ContinuousMultilinearMap.coe_continuous {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) :
Continuous ⇑f
source
@[simp]
theorem ContinuousMultilinearMap.coe_coe {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) :
⇑f.toMultilinearMap = ⇑f
source
theorem ContinuousMultilinearMap.ext {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {f f' : ContinuousMultilinearMap R M₁ M₂} (H : ∀ (x : (i : ι) → M₁ i), f x = f' x) :
f = f'
source
theorem ContinuousMultilinearMap.ext_iff {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {f f' : ContinuousMultilinearMap R M₁ M₂} :
f = f' ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
source
@[simp]
theorem ContinuousMultilinearMap.map_update_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i) :
f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
source
@[simp]
theorem ContinuousMultilinearMap.map_update_smul {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (Function.update m i (c • x)) = c • f (Function.update m i x)
source
theorem ContinuousMultilinearMap.map_coord_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι) (h : m i = 0) :
f m = 0
source
@[simp]
theorem ContinuousMultilinearMap.map_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [Nonempty ι] :
f 0 = 0
source
instance ContinuousMultilinearMap.instZero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
Zero (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.instZero = { zero := let __src := 0; { toMultilinearMap := __src, cont := ⋯ } }

source
instance ContinuousMultilinearMap.instInhabited {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
Inhabited (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.instInhabited = { default := 0 }

source
@[simp]
theorem ContinuousMultilinearMap.zero_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (m : (i : ι) → M₁ i) :
0 m = 0
source
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] :
toMultilinearMap 0 = 0
source
instance ContinuousMultilinearMap.instSMul {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] :
SMul R' (ContinuousMultilinearMap A M₁ M₂)
Equations

- ContinuousMultilinearMap.instSMul = { smul := fun (c : R') (f : ContinuousMultilinearMap A M₁ M₂) => let __src := c • f.toMultilinearMap; { toMultilinearMap := __src, cont := ⋯ } }

source
@[simp]
theorem ContinuousMultilinearMap.smul_apply {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] (f : ContinuousMultilinearMap A M₁ M₂) (c : R') (m : (i : ι) → M₁ i) :
(c • f) m = c • f m
source
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_smul {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] (c : R') (f : ContinuousMultilinearMap A M₁ M₂) :
(c • f).toMultilinearMap = c • f.toMultilinearMap
source
instance ContinuousMultilinearMap.instSMulCommClass {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [Monoid R'] [Monoid R''] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] [DistribMulAction R'' M₂] [ContinuousConstSMul R'' M₂] [SMulCommClass A R'' M₂] [SMulCommClass R' R'' M₂] :
SMulCommClass R' R'' (ContinuousMultilinearMap A M₁ M₂)
source
instance ContinuousMultilinearMap.instIsScalarTower {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {R'' : Type u_2} {A : Type u_3} [Monoid R'] [Monoid R''] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul 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'' (ContinuousMultilinearMap A M₁ M₂)
source
instance ContinuousMultilinearMap.instIsCentralScalar {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] [DistribMulAction R'ᵐᵒᵖ M₂] [IsCentralScalar R' M₂] :
IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂)
source
instance ContinuousMultilinearMap.instMulAction {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] :
MulAction R' (ContinuousMultilinearMap A M₁ M₂)
Equations

- ContinuousMultilinearMap.instMulAction = Function.Injective.mulAction ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯

source
instance ContinuousMultilinearMap.instAdd {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] :
Add (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.instAdd = { add := fun (f f' : ContinuousMultilinearMap R M₁ M₂) => { toMultilinearMap := f.toMultilinearMap + f'.toMultilinearMap, cont := ⋯ } }

source
@[simp]
theorem ContinuousMultilinearMap.add_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f f' : ContinuousMultilinearMap R M₁ M₂) [ContinuousAdd M₂] (m : (i : ι) → M₁ i) :
(f + f') m = f m + f' m
source
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMap_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] (f g : ContinuousMultilinearMap R M₁ M₂) :
(f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap
source
instance ContinuousMultilinearMap.addCommMonoid {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] :
AddCommMonoid (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.addCommMonoid = Function.Injective.addCommMonoid ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯ ⋯ ⋯

source
def ContinuousMultilinearMap.applyAddHom {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] (m : (i : ι) → M₁ i) :
ContinuousMultilinearMap R M₁ M₂ →+ M₂

Evaluation of a `ContinuousMultilinearMap` at a vector as an `AddMonoidHom`.

Equations

- ContinuousMultilinearMap.applyAddHom m = { toFun := fun (f : ContinuousMultilinearMap R M₁ M₂) => f m, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.sum_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] {α : Type u_1} (f : α → ContinuousMultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) {s : Finset α} :
(∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m
source
def ContinuousMultilinearMap.toContinuousLinearMap {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (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

- f.toContinuousLinearMap m i = { toLinearMap := f.toLinearMap m i, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.toContinuousLinearMap_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) :
(f.toContinuousLinearMap m i) x = f (Function.update m i x)
source
def ContinuousMultilinearMap.prod {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
ContinuousMultilinearMap R M₁ (M₂ × M₃)

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

Equations

- f.prod g = { toMultilinearMap := f.prod g.toMultilinearMap, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.prod_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) (m : (i : ι) → M₁ i) :
(f.prod g) m = (f m, g m)
source
def ContinuousMultilinearMap.pi {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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

- ContinuousMultilinearMap.pi f = { toMultilinearMap := MultilinearMap.pi fun (i : ι') => (f i).toMultilinearMap, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.coe_pi {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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)) :
⇑(pi f) = fun (m : (i : ι) → M₁ i) (j : ι') => (f j) m
source
theorem ContinuousMultilinearMap.pi_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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 : ι') :
(pi f) m j = (f j) m
source
def ContinuousMultilinearMap.codRestrict {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p) :
ContinuousMultilinearMap R M₁ ↥p

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

Equations

- f.codRestrict p h = { toMultilinearMap := f.codRestrict p h, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.codRestrict_toMultilinearMap {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p) :
(f.codRestrict p h).toMultilinearMap = f.codRestrict p h
source
@[simp]
theorem ContinuousMultilinearMap.codRestrict_apply_coe {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p) (v : (i : ι) → M₁ i) :
↑((f.codRestrict p h) v) = f v
source
def ContinuousMultilinearMap.ofSubsingleton (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] [Subsingleton ι] (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

source
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] [Subsingleton ι] (i : ι) (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) (x : M₂) :
((ofSubsingleton R M₂ M₃ i).symm f) x = f fun (x_1 : ι) => x
source
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] [Subsingleton ι] (i : ι) (f : M₂ →L[R] M₃) :
((ofSubsingleton R M₂ M₃ i) f).toMultilinearMap = (MultilinearMap.ofSubsingleton R M₂ M₃ i) ↑f
source
@[simp]
theorem ContinuousMultilinearMap.ofSubsingleton_apply_apply (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] [Subsingleton ι] (i : ι) (f : M₂ →L[R] M₃) (x : ι → M₂) :
((ofSubsingleton R M₂ M₃ i) f) x = f (x i)
source
def ContinuousMultilinearMap.constOfIsEmpty (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsEmpty ι] (m : M₂) :
ContinuousMultilinearMap R M₁ M₂

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

Equations

- ContinuousMultilinearMap.constOfIsEmpty R M₁ m = { toMultilinearMap := MultilinearMap.constOfIsEmpty R M₁ m, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.constOfIsEmpty_apply (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsEmpty ι] (m : M₂) (a✝ : (i : ι) → M₁ i) :
(constOfIsEmpty R M₁ m) a✝ = m
source
@[simp]
theorem ContinuousMultilinearMap.constOfIsEmpty_toMultilinearMap (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsEmpty ι] (m : M₂) :
(constOfIsEmpty R M₁ m).toMultilinearMap = MultilinearMap.constOfIsEmpty R M₁ m
source
def ContinuousMultilinearMap.compContinuousLinearMap {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₁' : ι → Type w₁'} {M₄ : Type w₄} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → AddCommMonoid (M₁' i)] [AddCommMonoid M₄] [(i : ι) → Module R (M₁ i)] [(i : ι) → Module R (M₁' i)] [Module R M₄] [(i : ι) → TopologicalSpace (M₁ i)] [(i : ι) → TopologicalSpace (M₁' i)] [TopologicalSpace M₄] (g : ContinuousMultilinearMap R M₁' M₄) (f : (i : ι) → M₁ i →L[R] M₁' i) :
ContinuousMultilinearMap R M₁ 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.compContinuousLinearMap f`.

Equations

- g.compContinuousLinearMap f = { toMultilinearMap := g.compLinearMap fun (i : ι) => ↑(f i), cont := ⋯ }

Instances For

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

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

Equations

- g.compContinuousMultilinearMap f = { toMultilinearMap := (↑g).compMultilinearMap f.toMultilinearMap, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearMap.compContinuousMultilinearMap_coe {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (g : M₂ →L[R] M₃) (f : ContinuousMultilinearMap R M₁ M₂) :
⇑(g.compContinuousMultilinearMap f) = ⇑g ∘ ⇑f
source
def ContinuousMultilinearMap.prodEquiv {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] :
ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃ ≃ ContinuousMultilinearMap R M₁ (M₂ × M₃)

`ContinuousMultilinearMap.prod` as an `Equiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.prodEquiv_symm_apply_fst {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)) :
(prodEquiv.symm f).1 = (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f
source
@[simp]
theorem ContinuousMultilinearMap.prodEquiv_symm_apply_snd {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)) :
(prodEquiv.symm f).2 = (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f
source
@[simp]
theorem ContinuousMultilinearMap.prodEquiv_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃) :
prodEquiv f = f.1.prod f.2
source
theorem ContinuousMultilinearMap.prodEquiv_symm_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)) :
prodEquiv.symm f = ((ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f, (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f)
source
theorem ContinuousMultilinearMap.prod_ext_iff {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} :
f = g ↔ (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f = (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g ∧ (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f = (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g
source
theorem ContinuousMultilinearMap.prod_ext {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] {f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)} (h₁ : (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f = (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g) (h₂ : (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f = (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g) :
f = g
source
theorem ContinuousMultilinearMap.eq_prod_iff {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] {f : ContinuousMultilinearMap R M₁ (M₂ × M₃)} {g : ContinuousMultilinearMap R M₁ M₂} {h : ContinuousMultilinearMap R M₁ M₃} :
f = g.prod h ↔ (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f = g ∧ (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f = h
source
theorem ContinuousMultilinearMap.add_prod_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] [ContinuousAdd M₂] [ContinuousAdd M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
(f₁ + f₂).prod (g₁ + g₂) = f₁.prod g₁ + f₂.prod g₂
source
theorem ContinuousMultilinearMap.smul_prod_smul {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] {S : Type u_1} [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃] [ContinuousConstSMul S M₂] [SMulCommClass R S M₂] [ContinuousConstSMul S M₃] [SMulCommClass R S M₃] (c : S) (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
(c • f).prod (c • g) = c • f.prod g
source
@[simp]
theorem ContinuousMultilinearMap.zero_prod_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [AddCommMonoid M₃] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [TopologicalSpace M₃] :
prod 0 0 = 0
source
def ContinuousMultilinearMap.piEquiv {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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

source
@[simp]
theorem ContinuousMultilinearMap.piEquiv_symm_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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 : ι') :
piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap f
source
@[simp]
theorem ContinuousMultilinearMap.piEquiv_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [Semiring R] [(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)) :
piEquiv f = pi f
source
def ContinuousMultilinearMap.domDomCongr {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace 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

- ContinuousMultilinearMap.domDomCongr e f = { toMultilinearMap := MultilinearMap.domDomCongr e f.toMultilinearMap, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.domDomCongr_toMultilinearMap {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) :
(domDomCongr e f).toMultilinearMap = MultilinearMap.domDomCongr e f.toMultilinearMap
source
@[simp]
theorem ContinuousMultilinearMap.domDomCongr_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) (v : ι' → M₂) :
(domDomCongr e f) v = f fun (i : ι) => v (e i)
source
def ContinuousMultilinearMap.domDomCongrEquiv {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace 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

- ContinuousMultilinearMap.domDomCongrEquiv e = { toFun := ContinuousMultilinearMap.domDomCongr e, invFun := ContinuousMultilinearMap.domDomCongr e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.domDomCongrEquiv_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun (x : ι) => M₂) M₃) :
(domDomCongrEquiv e) f = domDomCongr e f
source
@[simp]
theorem ContinuousMultilinearMap.domDomCongrEquiv_symm_apply {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [Semiring R] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] [TopologicalSpace M₂] [TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun (x : ι') => M₂) M₃) :
(domDomCongrEquiv e).symm f = domDomCongr e.symm f
source
def ContinuousMultilinearMap.linearDeriv {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [ContinuousAdd M₂] [DecidableEq ι] [Fintype ι] (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

- f.linearDeriv x = ∑ i : ι, (f.toContinuousLinearMap x i).comp (ContinuousLinearMap.proj i)

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.linearDeriv_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [ContinuousAdd M₂] [DecidableEq ι] [Fintype ι] (x y : (i : ι) → M₁ i) :
(f.linearDeriv x) y = ∑ i : ι, f (Function.update x i (y i))
source
theorem ContinuousMultilinearMap.cons_add {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] [(i : Fin n.succ) → TopologicalSpace (M i)] [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)

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.

source
theorem ContinuousMultilinearMap.cons_smul {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [Semiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] [(i : Fin n.succ) → TopologicalSpace (M i)] [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)

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.

source
theorem ContinuousMultilinearMap.map_piecewise_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (m m' : (i : ι) → M₁ i) (t : Finset ι) :
f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
source
theorem ContinuousMultilinearMap.map_add_univ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] [Fintype ι] (m m' : (i : ι) → M₁ i) :
f (m + m') = ∑ 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`.

source
theorem ContinuousMultilinearMap.map_sum_finset {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [Fintype ι] (g : (i : ι) → α i → M₁ i) (A : (i : ι) → Finset (α i)) [DecidableEq ι] :
(f fun (i : ι) => ∑ j ∈ A i, g i j) = ∑ r ∈ Fintype.piFinset 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.

source
theorem ContinuousMultilinearMap.map_sum {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [Fintype ι] (g : (i : ι) → α i → M₁ i) [DecidableEq ι] [(i : ι) → Fintype (α i)] :
(f fun (i : ι) => ∑ j : α i, g i j) = ∑ 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.

source
def ContinuousMultilinearMap.restrictScalars (R : Type u) {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {A : Type u_1} [Semiring A] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : ContinuousMultilinearMap A M₁ M₂) :
ContinuousMultilinearMap R 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

- ContinuousMultilinearMap.restrictScalars R f = { toMultilinearMap := MultilinearMap.restrictScalars R f.toMultilinearMap, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.coe_restrictScalars (R : Type u) {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Semiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] {A : Type u_1} [Semiring A] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : ContinuousMultilinearMap A M₁ M₂) :
⇑(restrictScalars R f) = ⇑f
source
@[simp]
theorem ContinuousMultilinearMap.map_update_sub {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i) :
f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
source
instance ContinuousMultilinearMap.instNeg {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsTopologicalAddGroup M₂] :
Neg (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.instNeg = { neg := fun (f : ContinuousMultilinearMap R M₁ M₂) => let __src := -f.toMultilinearMap; { toMultilinearMap := __src, cont := ⋯ } }

source
@[simp]
theorem ContinuousMultilinearMap.neg_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [IsTopologicalAddGroup M₂] (m : (i : ι) → M₁ i) :
(-f) m = -f m
source
instance ContinuousMultilinearMap.instSub {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsTopologicalAddGroup M₂] :
Sub (ContinuousMultilinearMap R M₁ M₂)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem ContinuousMultilinearMap.sub_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f f' : ContinuousMultilinearMap R M₁ M₂) [IsTopologicalAddGroup M₂] (m : (i : ι) → M₁ i) :
(f - f') m = f m - f' m
source
instance ContinuousMultilinearMap.instAddCommGroup {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsTopologicalAddGroup M₂] :
AddCommGroup (ContinuousMultilinearMap R M₁ M₂)
Equations

- ContinuousMultilinearMap.instAddCommGroup = Function.Injective.addCommGroup ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source
theorem ContinuousMultilinearMap.neg_prod_neg {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsTopologicalAddGroup M₂] [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [IsTopologicalAddGroup M₃] (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
(-f).prod (-g) = -f.prod g
source
theorem ContinuousMultilinearMap.sub_prod_sub {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [Ring R] [(i : ι) → AddCommGroup (M₁ i)] [AddCommGroup M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [IsTopologicalAddGroup M₂] [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [IsTopologicalAddGroup M₃] (f₁ f₂ : ContinuousMultilinearMap R M₁ M₂) (g₁ g₂ : ContinuousMultilinearMap R M₁ M₃) :
(f₁ - f₂).prod (g₁ - g₂) = f₁.prod g₁ - f₂.prod g₂
source
theorem ContinuousMultilinearMap.map_piecewise_smul {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [DecidableEq ι] (c : ι → R) (m : (i : ι) → M₁ i) (s : Finset ι) :
f (s.piecewise (fun (i : ι) => c i • m i) m) = (∏ i ∈ s, c i) • f m
source
theorem ContinuousMultilinearMap.map_smul_univ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] (f : ContinuousMultilinearMap R M₁ M₂) [Fintype ι] (c : ι → R) (m : (i : ι) → M₁ i) :
(f fun (i : ι) => c i • m i) = (∏ 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`.

source
theorem ContinuousMultilinearMap.ext_ring {R : Type u} {ι : Type v} {M₂ : Type w₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [TopologicalSpace M₂] [Finite ι] [TopologicalSpace R] ⦃f g : ContinuousMultilinearMap R (fun (x : ι) => R) M₂⦄ (h : (f fun (x : ι) => 1) = g fun (x : ι) => 1) :
f = g

If two continuous `R`-multilinear maps from `R` are equal on 1, then they are equal.

This is the multilinear version of `ContinuousLinearMap.ext_ring`.

source
theorem ContinuousMultilinearMap.ext_ring_iff {R : Type u} {ι : Type v} {M₂ : Type w₂} [CommSemiring R] [AddCommMonoid M₂] [Module R M₂] [TopologicalSpace M₂] [Finite ι] [TopologicalSpace R] {f g : ContinuousMultilinearMap R (fun (x : ι) => R) M₂} :
f = g ↔ (f fun (x : ι) => 1) = g fun (x : ι) => 1
source
instance ContinuousMultilinearMap.instDistribMulAction {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_3} [Monoid R'] [Semiring A] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [(i : ι) → Module A (M₁ i)] [Module A M₂] [DistribMulAction R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] [ContinuousAdd M₂] :
DistribMulAction R' (ContinuousMultilinearMap A M₁ M₂)
Equations

- ContinuousMultilinearMap.instDistribMulAction = Function.Injective.distribMulAction { toFun := ContinuousMultilinearMap.toMultilinearMap, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

source
instance ContinuousMultilinearMap.instModule {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] :
Module R' (ContinuousMultilinearMap A M₁ 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

- ContinuousMultilinearMap.instModule = Function.Injective.module R' { toFun := ContinuousMultilinearMap.toMultilinearMap, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

source
def ContinuousMultilinearMap.toMultilinearMapLinear {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] :
ContinuousMultilinearMap A M₁ 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 = { toFun := ContinuousMultilinearMap.toMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.toMultilinearMapLinear_apply {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousAdd M₂] [(i : ι) → Module A (M₁ i)] [Module A M₂] [Module R' M₂] [ContinuousConstSMul R' M₂] [SMulCommClass A R' M₂] (self : ContinuousMultilinearMap A M₁ M₂) :
toMultilinearMapLinear self = self.toMultilinearMap
source
def ContinuousMultilinearMap.piLinearEquiv {ι : Type v} {M₁ : ι → Type w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(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

source
@[simp]
theorem ContinuousMultilinearMap.piLinearEquiv_apply {ι : Type v} {M₁ : ι → Type w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(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)) :
piLinearEquiv a✝ = pi a✝
source
@[simp]
theorem ContinuousMultilinearMap.piLinearEquiv_symm_apply {ι : Type v} {M₁ : ι → Type w₁} {R' : Type u_1} {A : Type u_2} [Semiring R'] [Semiring A] [(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 : ι') :
piLinearEquiv.symm a✝ i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap a✝
source
def ContinuousMultilinearMap.mkPiAlgebraFin (R : Type u) (n : ℕ) (A : Type u_1) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [ContinuousMul 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

- ContinuousMultilinearMap.mkPiAlgebraFin R n A = { toMultilinearMap := MultilinearMap.mkPiAlgebraFin R n A, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.mkPiAlgebraFin_apply {R : Type u} {n : ℕ} {A : Type u_1} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [ContinuousMul A] (m : Fin n → A) :
(ContinuousMultilinearMap.mkPiAlgebraFin R n A) m = (List.ofFn m).prod
source
def ContinuousMultilinearMap.mkPiAlgebra (R : Type u) (ι : Type v) (A : Type u_1) [Fintype ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [TopologicalSpace A] [ContinuousMul 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

- ContinuousMultilinearMap.mkPiAlgebra R ι A = { toMultilinearMap := MultilinearMap.mkPiAlgebra R ι A, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.mkPiAlgebra_apply (R : Type u) (ι : Type v) (A : Type u_1) [Fintype ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [TopologicalSpace A] [ContinuousMul A] (m : ι → A) :
(ContinuousMultilinearMap.mkPiAlgebra R ι A) m = ∏ i : ι, m i
source
theorem ContinuousMultilinearMap.mkPiAlgebra_eq_mkPiAlgebraFin (R : Type u) (A : Type u_1) [CommSemiring R] [CommSemiring A] [Algebra R A] [TopologicalSpace A] [ContinuousMul A] {n : ℕ} :
ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A = ContinuousMultilinearMap.mkPiAlgebraFin R n A
source
def ContinuousMultilinearMap.smulRight {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [TopologicalSpace R] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousSMul R M₂] (f : ContinuousMultilinearMap R M₁ R) (z : M₂) :
ContinuousMultilinearMap R M₁ 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

- f.smulRight z = { toMultilinearMap := f.smulRight z, cont := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.smulRight_toMultilinearMap {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [TopologicalSpace R] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousSMul R M₂] (f : ContinuousMultilinearMap R M₁ R) (z : M₂) :
(f.smulRight z).toMultilinearMap = f.smulRight z
source
@[simp]
theorem ContinuousMultilinearMap.smulRight_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [CommSemiring R] [(i : ι) → AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [(i : ι) → Module R (M₁ i)] [Module R M₂] [TopologicalSpace R] [(i : ι) → TopologicalSpace (M₁ i)] [TopologicalSpace M₂] [ContinuousSMul R M₂] (f : ContinuousMultilinearMap R M₁ R) (z : M₂) (a✝ : (i : ι) → M₁ i) :
(f.smulRight z) a✝ = f a✝ • z
source
def ContinuousMultilinearMap.mkPiRing (R : Type u) (ι : Type v) {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul 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

- ContinuousMultilinearMap.mkPiRing R ι z = (ContinuousMultilinearMap.mkPiAlgebra R ι R).smulRight z

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.mkPiRing_apply {R : Type u} {ι : Type v} {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul R M] (z : M) (m : ι → R) :
(ContinuousMultilinearMap.mkPiRing R ι z) m = (∏ i : ι, m i) • z
source
theorem ContinuousMultilinearMap.mkPiRing_apply_one_eq_self {R : Type u} {ι : Type v} {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul R M] (f : ContinuousMultilinearMap R (fun (x : ι) => R) M) :
ContinuousMultilinearMap.mkPiRing R ι (f fun (x : ι) => 1) = f
source
theorem ContinuousMultilinearMap.mkPiRing_eq_iff {R : Type u} {ι : Type v} {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul R M] {z₁ z₂ : M} :
ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
source
theorem ContinuousMultilinearMap.mkPiRing_zero {R : Type u} {ι : Type v} {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul R M] :
ContinuousMultilinearMap.mkPiRing R ι 0 = 0
source
theorem ContinuousMultilinearMap.mkPiRing_eq_zero_iff {R : Type u} {ι : Type v} {M : Type u_1} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [TopologicalSpace R] [TopologicalSpace M] [ContinuousMul R] [ContinuousSMul R M] (z : M) :
ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0