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_add' : ∀ [inst : 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_smul' : ∀ [inst : 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.
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.
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
Equations
- ContinuousMultilinearMap.funLike = { coe := fun (f : ContinuousMultilinearMap R M₁ M₂) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
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
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
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ContinuousMultilinearMap.instMulAction = Function.Injective.mulAction ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯
Equations
- ContinuousMultilinearMap.instAdd = { add := fun (f f' : ContinuousMultilinearMap R M₁ M₂) => { toMultilinearMap := f.toMultilinearMap + f'.toMultilinearMap, cont := ⋯ } }
Equations
- ContinuousMultilinearMap.addCommMonoid = Function.Injective.addCommMonoid ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯ ⋯ ⋯
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
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
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
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
Restrict the codomain of a continuous multilinear map to a submodule.
Equations
- f.codRestrict p h = { toMultilinearMap := f.codRestrict p h, cont := ⋯ }
Instances For
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
The constant map is multilinear when ι
is empty.
Equations
- ContinuousMultilinearMap.constOfIsEmpty R M₁ m = { toMultilinearMap := MultilinearMap.constOfIsEmpty R M₁ m, cont := ⋯ }
Instances For
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
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
ContinuousMultilinearMap.pi
as an Equiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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 := ⋯ }
Instances For
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.
Equations
- ContinuousMultilinearMap.instAddCommGroup = Function.Injective.addCommGroup ContinuousMultilinearMap.toMultilinearMap ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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' := ⋯ }
Instances For
ContinuousMultilinearMap.pi
as a LinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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