Operator norm on the space of continuous multilinear maps #
When f
is a continuous multilinear map in finitely many variables, we define its norm ‖f‖
as the
smallest number such that ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
for all m
.
We show that it is indeed a norm, and prove its basic properties.
Main results #
Let f
be a multilinear map in finitely many variables.
exists_bound_of_continuous
asserts that, iff
is continuous, then there existsC > 0
with‖f m‖ ≤ C * ∏ i, ‖m i‖
for allm
.continuous_of_bound
, conversely, asserts that this bound implies continuity.mkContinuous
constructs the associated continuous multilinear map.
Let f
be a continuous multilinear map in finitely many variables.
‖f‖
is its norm, i.e., the smallest number such that‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
for allm
.le_opNorm f m
asserts the fundamental inequality‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
.norm_image_sub_le f m₁ m₂
gives a control of the differencef m₁ - f m₂
in terms of‖f‖
and‖m₁ - m₂‖
.
Implementation notes #
We mostly follow the API (and the proofs) of OperatorNorm.lean
, with the additional complexity
that we should deal with multilinear maps in several variables. The currying/uncurrying
constructions are based on those in Multilinear.lean
.
From the mathematical point of view, all the results follow from the results on operator norm in
one variable, by applying them to one variable after the other through currying. However, this
is only well defined when there is an order on the variables (for instance on Fin n
) although
the final result is independent of the order. While everything could be done following this
approach, it turns out that direct proofs are easier and more efficient.
Type variables #
We use the following type variables in this file:
𝕜
: aNontriviallyNormedField
;ι
,ι'
: finite index types with decidable equality;E
,E₁
: families of normed vector spaces over𝕜
indexed byi : ι
;E'
: a family of normed vector spaces over𝕜
indexed byi' : ι'
;Ei
: a family of normed vector spaces over𝕜
indexed byi : Fin (Nat.succ n)
;G
,G'
: normed vector spaces over𝕜
.
Applying a multilinear map to a vector is continuous in both coordinates.
Continuity properties of multilinear maps #
We relate continuity of multilinear maps to the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖
, in
both directions. Along the way, we prove useful bounds on the difference ‖f m₁ - f m₂‖
.
If f
is a continuous multilinear map in finitely many variables on E
and m
is an element
of ∀ i, E i
such that one of the m i
has norm 0
, then f m
has norm 0
.
Note that we cannot drop the continuity assumption because f (m : Unit → E) = f (m ())
,
where the domain has zero norm and the codomain has a nonzero norm
does not satisfy this condition.
If a continuous multilinear map in finitely many variables on normed spaces satisfies
the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖
on a shell ε i / ‖c i‖ < ‖m i‖ < ε i
for some positive
numbers ε i
and elements c i : 𝕜
, 1 < ‖c i‖
, then it satisfies this inequality for all m
.
If a multilinear map in finitely many variables on normed spaces is continuous, then it
satisfies the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖
, for some C
which can be chosen to be
positive.
If f
satisfies a boundedness property around 0
, one can deduce a bound on f m₁ - f m₂
using the multilinearity. Here, we give a precise but hard to use version. See
norm_image_sub_le_of_bound
for a less precise but more usable version. The bound reads
‖f m - f m'‖ ≤ C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...
,
where the other terms in the sum are the same products where 1
is replaced by any i
.
If f
satisfies a boundedness property around 0
, one can deduce a bound on f m₁ - f m₂
using the multilinearity. Here, we give a usable but not very precise version. See
norm_image_sub_le_of_bound'
for a more precise but less usable version. The bound is
‖f m - f m'‖ ≤ C * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)
.
If a multilinear map satisfies an inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖
, then it is
continuous.
Constructing a continuous multilinear map from a multilinear map satisfying a boundedness condition.
Equations
- f.mkContinuous C H = { toMultilinearMap := f, cont := ⋯ }
Instances For
Given a multilinear map in n
variables, if one restricts it to k
variables putting z
on
the other coordinates, then the resulting restricted function satisfies an inequality
‖f.restr v‖ ≤ C * ‖z‖^(n-k) * Π ‖v i‖
if the original function satisfies ‖f v‖ ≤ C * Π ‖v i‖
.
Continuous multilinear maps #
We define the norm ‖f‖
of a continuous multilinear map f
in finitely many variables as the
smallest number such that ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
for all m
. We show that this
defines a normed space structure on ContinuousMultilinearMap 𝕜 E G
.
The operator norm of a continuous multilinear map is the inf of all its bounds.
Instances For
Equations
- ContinuousMultilinearMap.hasOpNorm = { norm := ContinuousMultilinearMap.opNorm }
An alias of ContinuousMultilinearMap.hasOpNorm
with non-dependent types to help typeclass
search.
Equations
- ContinuousMultilinearMap.hasOpNorm' = ContinuousMultilinearMap.hasOpNorm
Alias of ContinuousMultilinearMap.isLeast_opNorm
.
Alias of ContinuousMultilinearMap.opNorm_nonneg
.
The fundamental property of the operator norm of a continuous multilinear map:
‖f m‖
is bounded by ‖f‖
times the product of the ‖m i‖
.
Alias of ContinuousMultilinearMap.le_opNorm
.
The fundamental property of the operator norm of a continuous multilinear map:
‖f m‖
is bounded by ‖f‖
times the product of the ‖m i‖
.
Alias of ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le
.
Alias of ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le
.
Alias of ContinuousMultilinearMap.le_of_opNorm_le
.
Alias of ContinuousMultilinearMap.ratio_le_opNorm
.
The image of the unit ball under a continuous multilinear map is bounded.
Alias of ContinuousMultilinearMap.unit_le_opNorm
.
The image of the unit ball under a continuous multilinear map is bounded.
If one controls the norm of every f x
, then one controls the norm of f
.
Alias of ContinuousMultilinearMap.opNorm_le_bound
.
If one controls the norm of every f x
, then one controls the norm of f
.
Alias of ContinuousMultilinearMap.opNorm_le_iff
.
The operator norm satisfies the triangle inequality.
Alias of ContinuousMultilinearMap.opNorm_add_le
.
The operator norm satisfies the triangle inequality.
Alias of ContinuousMultilinearMap.opNorm_zero
.
Alias of ContinuousMultilinearMap.opNorm_smul_le
.
Alias of ContinuousMultilinearMap.opNorm_neg
.
Operator seminorm on the space of continuous multilinear maps, as Seminorm
.
We use this seminorm
to define a SeminormedAddCommGroup
structure on ContinuousMultilinearMap 𝕜 E G
,
but we have to override the projection UniformSpace
so that it is definitionally equal to the one coming from the topologies on E
and G
.
Equations
- ContinuousMultilinearMap.seminorm 𝕜 E G = Seminorm.ofSMulLE norm ⋯ ⋯ ⋯
Instances For
Equations
- ContinuousMultilinearMap.instPseudoMetricSpace = SeminormedAddCommGroup.toPseudoMetricSpace.replaceUniformity ⋯
Continuous multilinear maps themselves form a seminormed space with respect to the operator norm.
Equations
- ContinuousMultilinearMap.seminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯
An alias of ContinuousMultilinearMap.seminormedAddCommGroup
with non-dependent types to help
typeclass search.
Equations
- ContinuousMultilinearMap.seminormedAddCommGroup' = ContinuousMultilinearMap.seminormedAddCommGroup
Equations
- ContinuousMultilinearMap.normedSpace = NormedSpace.mk ⋯
An alias of ContinuousMultilinearMap.normedSpace
with non-dependent types to help typeclass
search.
Equations
- ContinuousMultilinearMap.normedSpace' = ContinuousMultilinearMap.normedSpace
The fundamental property of the operator norm of a continuous multilinear map:
‖f m‖
is bounded by ‖f‖
times the product of the ‖m i‖
, nnnorm
version.
Alias of ContinuousMultilinearMap.le_opNNNorm
.
The fundamental property of the operator norm of a continuous multilinear map:
‖f m‖
is bounded by ‖f‖
times the product of the ‖m i‖
, nnnorm
version.
Alias of ContinuousMultilinearMap.opNNNorm_le_iff
.
Alias of ContinuousMultilinearMap.opNNNorm_prod
.
Alias of ContinuousMultilinearMap.opNorm_prod
.
Alias of ContinuousMultilinearMap.opNorm_pi
.
Linear isometry between continuous linear maps from G
to G'
and continuous 1
-multilinear maps from G
to G'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ContinuousMultilinearMap.prod
as a LinearIsometryEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ContinuousMultilinearMap.pi
as a LinearIsometryEquiv
.
Equations
- ContinuousMultilinearMap.piₗᵢ 𝕜 E = { toLinearEquiv := ContinuousMultilinearMap.piLinearEquiv, norm_map' := ⋯ }
Instances For
ContinuousMultilinearMap.restrictScalars
as a LinearIsometry
.
Equations
- ContinuousMultilinearMap.restrictScalarsₗᵢ 𝕜' = { toFun := ContinuousMultilinearMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }
Instances For
The difference f m₁ - f m₂
is controlled in terms of ‖f‖
and ‖m₁ - m₂‖
, precise version.
For a less precise but more usable version, see norm_image_sub_le
. The bound reads
‖f m - f m'‖ ≤ ‖f‖ * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...
,
where the other terms in the sum are the same products where 1
is replaced by any i
.
The difference f m₁ - f m₂
is controlled in terms of ‖f‖
and ‖m₁ - m₂‖
, less precise
version. For a more precise but less usable version, see norm_image_sub_le'
.
The bound is ‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)
.
If a continuous multilinear map is constructed from a multilinear map via the constructor
mkContinuous
, then its norm is bounded by the bound given to the constructor if it is
nonnegative.
If a continuous multilinear map is constructed from a multilinear map via the constructor
mkContinuous
, then its norm is bounded by the bound given to the constructor if it is
nonnegative.
Given a continuous multilinear map f
on n
variables (parameterized by Fin n
) and a subset
s
of k
of these variables, one gets a new continuous multilinear map on Fin k
by varying
these variables, and fixing the other ones equal to a given value z
. It is denoted by
f.restr s hk z
, where hk
is a proof that the cardinality of s
is k
. The implicit
identification between Fin k
and s
that we use is the canonical (increasing) bijection.
Instances For
Continuous bilinear map realizing (f, z) ↦ f.smulRight z
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Continuous multilinear maps on 𝕜^n
with values in G
are in bijection with G
, as such a
continuous multilinear map is completely determined by its value on the constant vector made of
ones. We register this bijection as a linear isometry in
ContinuousMultilinearMap.piFieldEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ContinuousLinearMap.compContinuousMultilinearMap
as a bundled continuous bilinear map.
Equations
- ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G G' = (LinearMap.mk₂ 𝕜 ContinuousLinearMap.compContinuousMultilinearMap ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯
Instances For
ContinuousLinearMap.compContinuousMultilinearMap
as a bundled
continuous linear equiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Flip arguments in f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
to get
ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a map f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
and an estimate
H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
, construct a continuous linear
map from G
to ContinuousMultilinearMap 𝕜 E G'
.
In order to lift, e.g., a map f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G'
to a map (ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G'
,
one can apply this construction to f.comp ContinuousMultilinearMap.toMultilinearMapLinear
which is a linear map from ContinuousMultilinearMap 𝕜 E G
to MultilinearMap 𝕜 E' G'
.
Equations
Instances For
Given a map f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
and an estimate
H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖
, upgrade all MultilinearMap
s in the type to
ContinuousMultilinearMap
s.
Equations
Instances For
ContinuousMultilinearMap.compContinuousLinearMap
as a bundled continuous linear map.
This implementation fixes f : Π i, E i →L[𝕜] E₁ i
.
Actually, the map is multilinear in f
,
see ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
.
For a version fixing g
and varying f
, see compContinuousLinearMapLRight
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ContinuousMultilinearMap.compContinuousLinearMap
as a bundled continuous linear map.
This implementation fixes g : ContinuousMultilinearMap 𝕜 E₁ G
.
Actually, the map is linear in g
,
see ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
.
For a version fixing f
and varying g
, see compContinuousLinearMapL
.
Equations
Instances For
If f
is a collection of continuous linear maps, then the construction
ContinuousMultilinearMap.compContinuousLinearMap
sending a continuous multilinear map g
to g (f₁ ·, ..., fₙ ·)
is continuous-linear in g
and multilinear in f₁, ..., fₙ
.
Equations
- ContinuousMultilinearMap.compContinuousLinearMapMultilinear 𝕜 E E₁ G = { toFun := ContinuousMultilinearMap.compContinuousLinearMapL, map_add' := ⋯, map_smul' := ⋯ }
Instances For
If f
is a collection of continuous linear maps, then the construction
ContinuousMultilinearMap.compContinuousLinearMap
sending a continuous multilinear map g
to g (f₁ ·, ..., fₙ ·)
is continuous-linear in g
and
continuous-multilinear in f₁, ..., fₙ
.
Equations
- ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 E E₁ G = (ContinuousMultilinearMap.compContinuousLinearMapMultilinear 𝕜 E E₁ G).mkContinuous 1 ⋯
Instances For
ContinuousMultilinearMap.compContinuousLinearMap
as a bundled continuous linear equiv,
given f : Π i, E i ≃L[𝕜] E₁ i
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One of the components of the iterated derivative of a continuous multilinear map. Given a
bijection e
between a type α
(typically Fin k
) and a subset s
of ι
, this component is a
continuous multilinear map of k
vectors v₁, ..., vₖ
, mapping them
to f (x₁, (v_{e.symm 2})₂, x₃, ...)
, where at indices i
in s
one uses the i
-th coordinate of
the vector v_{e.symm i}
and otherwise one uses the i
-th coordinate of a reference vector x
.
This is continuous multilinear in the components of x
outside of s
, and in the v_j
.
Instances For
The k
-th iterated derivative of a continuous multilinear map f
at the point x
. It is a
continuous multilinear map of k
vectors v₁, ..., vₖ
(with the same type as x
), mapping them
to ∑ f (x₁, (v_{i₁})₂, x₃, ...)
, where at each index j
one uses either xⱼ
or one
of the (vᵢ)ⱼ
, and each vᵢ
has to be used exactly once.
The sum is parameterized by the embeddings of Fin k
in the index type ι
(or, equivalently,
by the subsets s
of ι
of cardinality k
and then the bijections between Fin k
and s
).
The fact that this is indeed the iterated Fréchet derivative is proved in
ContinuousMultilinearMap.iteratedFDeriv_eq
.
Equations
- f.iteratedFDeriv k x = ∑ e : Fin k ↪ ι, (f.iteratedFDerivComponent e.toEquivRange) ((Pi.compRightL 𝕜 E₁ Subtype.val) x)
Instances For
Controlling the norm of f.iteratedFDeriv
when f
is continuous multilinear. For the same
bound on the iterated derivative of f
in the calculus sense,
see ContinuousMultilinearMap.norm_iteratedFDeriv_le
.
Results that are only true if the target space is a NormedAddCommGroup
(and not just a
SeminormedAddCommGroup
).
A continuous linear map is zero iff its norm vanishes.
Alias of ContinuousMultilinearMap.opNorm_zero_iff
.
A continuous linear map is zero iff its norm vanishes.
Continuous multilinear maps themselves form a normed group with respect to the operator norm.
Equations
- ContinuousMultilinearMap.normedAddCommGroup = NormedAddCommGroup.ofSeparation ⋯
An alias of ContinuousMultilinearMap.normedAddCommGroup
with non-dependent types to help
typeclass search.
Equations
- ContinuousMultilinearMap.normedAddCommGroup' = ContinuousMultilinearMap.normedAddCommGroup
Results that are only true if the source is a NormedAddCommGroup
(and not just a
SeminormedAddCommGroup
).
If a multilinear map in finitely many variables on normed spaces satisfies the inequality
‖f m‖ ≤ C * ∏ i, ‖m i‖
on a shell ε i / ‖c i‖ < ‖m i‖ < ε i
for some positive numbers ε i
and elements c i : 𝕜
, 1 < ‖c i‖
, then it satisfies this inequality for all m
.