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
toM₂
. We show that it is anR
-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.
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
toM₂
whereM₁ i
andM₂
are modules overR
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.
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.
Equations
- ContinuousMultilinearMap.funLike = { coe := fun (f : ContinuousMultilinearMap R M₁ M₂) => f.toFun, coe_injective' := ⋯ }
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
Alias of ContinuousMultilinearMap.map_update_add
.
Alias of ContinuousMultilinearMap.map_update_smul
.
Equations
- ContinuousMultilinearMap.instZero = { zero := let __src := 0; { toMultilinearMap := __src, cont := ⋯ } }
Equations
- ContinuousMultilinearMap.instInhabited = { default := 0 }
Equations
- ContinuousMultilinearMap.instSMul = { smul := fun (c : R') (f : ContinuousMultilinearMap A M₁ M₂) => let __src := c • f.toMultilinearMap; { toMultilinearMap := __src, cont := ⋯ } }
Equations
- ContinuousMultilinearMap.instAdd = { add := fun (f f' : ContinuousMultilinearMap R M₁ M₂) => { toMultilinearMap := f.toMultilinearMap + f'.toMultilinearMap, cont := ⋯ } }
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' := ⋯ }
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 := ⋯ }
The cartesian product of two continuous multilinear maps, as a continuous multilinear map.
Equations
- f.prod g = { toMultilinearMap := f.prod g.toMultilinearMap, cont := ⋯ }
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 := ⋯ }
Restrict the codomain of a continuous multilinear map to a submodule.
Equations
- f.codRestrict p h = { toMultilinearMap := f.codRestrict p h, cont := ⋯ }
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.
The constant map is multilinear when ι
is empty.
Equations
- ContinuousMultilinearMap.constOfIsEmpty R M₁ m = { toMultilinearMap := MultilinearMap.constOfIsEmpty R M₁ m, cont := ⋯ }
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 := ⋯ }
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 := ⋯ }
ContinuousMultilinearMap.prod
as an Equiv
.
Equations
- One or more equations did not get rendered due to their size.
ContinuousMultilinearMap.pi
as an Equiv
.
Equations
- One or more equations did not get rendered due to their size.
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 := ⋯ }
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 := ⋯ }
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)
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.
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.
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
.
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.
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.
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 := ⋯ }
Alias of ContinuousMultilinearMap.map_update_sub
.
Equations
- ContinuousMultilinearMap.instNeg = { neg := fun (f : ContinuousMultilinearMap R M₁ M₂) => let __src := -f.toMultilinearMap; { toMultilinearMap := __src, cont := ⋯ } }
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- ContinuousMultilinearMap.instDistribMulAction = Function.Injective.distribMulAction { toFun := ContinuousMultilinearMap.toMultilinearMap, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
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' := ⋯ } ⋯ ⋯
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' := ⋯ }
ContinuousMultilinearMap.pi
as a LinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
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 := ⋯ }
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 := ⋯ }
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 := ⋯ }
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