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_continuousasserts that, iffis continuous, then there existsC > 0with∥f m∥ ≤ C * ∏ i, ∥m i∥for allm.continuous_of_bound, conversely, asserts that this bound implies continuity.mk_continuousconstructs 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_op_norm f masserts the fundamental inequality∥f m∥ ≤ ∥f∥ * ∏ i, ∥m i∥.norm_image_sub_le_of_bound f m₁ m₂gives a control of the differencef m₁ - f m₂in terms of∥f∥and∥m₁ - m₂∥.
We also register isomorphisms corresponding to currying or uncurrying variables, transforming a
continuous multilinear function f in n+1 variables into a continuous linear function taking
values in continuous multilinear functions in n variables, and also into a continuous multilinear
function in n variables taking values in continuous linear functions. These operations are called
f.curry_left and f.curry_right respectively (with inverses f.uncurry_left and
f.uncurry_right). They induce continuous linear equivalences between spaces of
continuous multilinear functions in n+1 variables and spaces of continuous linear functions into
continuous multilinear functions in n variables (resp. continuous multilinear functions in n
variables taking values in continuous linear functions), called respectively
continuous_multilinear_curry_left_equiv and continuous_multilinear_curry_right_equiv.
Implementation notes
We mostly follow the API (and the proofs) of operator_norm.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.
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 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.mk_continuous C H = {to_multilinear_map := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, cont := _}
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 continuous_multilinear_map 𝕜 E₁ E₂.
The operator norm of a continuous multilinear map is the inf of all its bounds.
Equations
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∥.
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.
The operator norm satisfies the triangle inequality.
A continuous linear map is zero iff its norm vanishes.
Continuous multilinear maps themselves form a normed space with respect to the operator norm.
Equations
- continuous_multilinear_map.to_normed_group = normed_group.of_core (continuous_multilinear_map 𝕜 E₁ E₂) continuous_multilinear_map.to_normed_group._proof_1
Equations
- continuous_multilinear_map.to_normed_space = {to_semimodule := continuous_multilinear_map.semimodule continuous_multilinear_map.to_normed_space._proof_1, norm_smul_le := _}
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_of_bound. 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_of_bound'.
The bound is ∥f m - f m'∥ ≤ ∥f∥ * card ι * ∥m - m'∥ * (max ∥m∥ ∥m'∥) ^ (card ι - 1).
Applying a multilinear map to a vector is continuous in both coordinates.
If the target space is complete, the space of continuous multilinear maps with its norm is also
complete. The proof is essentially the same as for the space of continuous linear maps (modulo the
addition of finset.prod where needed. The duplication could be avoided by deducing the linear
case from the multilinear case via a currying isomorphism. However, this would mess up imports,
and it is more satisfactory to have the simplest case as a standalone proof.
Equations
If a continuous multilinear map is constructed from a multilinear map via the constructor
mk_continuous, 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.
The canonical continuous multilinear map on 𝕜^ι, associating to m the product of all the
m i (multiplied by a fixed reference element z in the target module)
Equations
- continuous_multilinear_map.mk_pi_field 𝕜 ι z = (multilinear_map.mk_pi_ring 𝕜 ι z).mk_continuous ∥z∥ _
Continuous multilinear maps on 𝕜^n with values in E₂ are in bijection with E₂, 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 equivalence in
continuous_multilinear_map.pi_field_equiv_aux. The continuous linear equivalence is
continuous_multilinear_map.pi_field_equiv.
Equations
- continuous_multilinear_map.pi_field_equiv_aux 𝕜 ι E₂ = {to_fun := λ (z : E₂), continuous_multilinear_map.mk_pi_field 𝕜 ι z, map_add' := _, map_smul' := _, inv_fun := λ (f : continuous_multilinear_map 𝕜 (λ (i : ι), 𝕜) E₂), ⇑f (λ (i : ι), 1), left_inv := _, right_inv := _}
Continuous multilinear maps on 𝕜^n with values in E₂ are in bijection with E₂, 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 continuous linear equivalence in
continuous_multilinear_map.pi_field_equiv.
Equations
- continuous_multilinear_map.pi_field_equiv 𝕜 ι E₂ = {to_linear_equiv := {to_fun := (continuous_multilinear_map.pi_field_equiv_aux 𝕜 ι E₂).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_multilinear_map.pi_field_equiv_aux 𝕜 ι E₂).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Currying
We associate to a continuous multilinear map in n+1 variables (i.e., based on fin n.succ) two
curried functions, named f.curry_left (which is a continuous linear map on E 0 taking values
in continuous multilinear maps in n variables) and f.curry_right (which is a continuous
multilinear map in n variables taking values in continuous linear maps on E (last n)).
The inverse operations are called uncurry_left and uncurry_right.
We also register continuous linear equiv versions of these correspondences, in
continuous_multilinear_curry_left_equiv and continuous_multilinear_curry_right_equiv.
Left currying
Given a continuous linear map f from E 0 to continuous multilinear maps on n variables,
construct the corresponding continuous multilinear map on n+1 variables obtained by concatenating
the variables, given by m ↦ f (m 0) (tail m)
Given a continuous multilinear map f in n+1 variables, split the first variable to obtain
a continuous linear map into continuous multilinear maps in n variables, given by
x ↦ (m ↦ f (cons x m)).
Equations
- f.curry_left = {to_fun := λ (x : E 0), (⇑(f.to_multilinear_map.curry_left) x).mk_continuous (∥f∥ * ∥x∥) _, map_add' := _, map_smul' := _}.mk_continuous ∥f∥ _
The space of continuous multilinear maps on Π(i : fin (n+1)), E i is canonically isomorphic to
the space of continuous linear maps from E 0 to the space of continuous multilinear maps on
Π(i : fin n), E i.succ, by separating the first variable. We register this isomorphism as a
linear isomorphism in continuous_multilinear_curry_left_equiv_aux 𝕜 E E₂.
The algebraic version (without continuity assumption on the maps) is
multilinear_curry_left_equiv 𝕜 E E₂, and the topological isomorphism (registering
additionally that the isomorphism is continuous) is
continuous_multilinear_curry_left_equiv 𝕜 E E₂.
The direct and inverse maps are given by f.uncurry_left and f.curry_left. Use these
unless you need the full framework of linear equivs.
Equations
- continuous_multilinear_curry_left_equiv_aux 𝕜 E E₂ = {to_fun := continuous_linear_map.uncurry_left _inst_11, map_add' := _, map_smul' := _, inv_fun := continuous_multilinear_map.curry_left _inst_11, left_inv := _, right_inv := _}
The space of continuous multilinear maps on Π(i : fin (n+1)), E i is canonically isomorphic to
the space of continuous linear maps from E 0 to the space of continuous multilinear maps on
Π(i : fin n), E i.succ, by separating the first variable. We register this isomorphism in
continuous_multilinear_curry_left_equiv 𝕜 E E₂. The algebraic version (without topology) is given
in multilinear_curry_left_equiv 𝕜 E E₂.
The direct and inverse maps are given by f.uncurry_left and f.curry_left. Use these
unless you need the full framework of continuous linear equivs.
Equations
- continuous_multilinear_curry_left_equiv 𝕜 E E₂ = {to_linear_equiv := {to_fun := (continuous_multilinear_curry_left_equiv_aux 𝕜 E E₂).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_multilinear_curry_left_equiv_aux 𝕜 E E₂).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Right currying
Given a continuous linear map f from continuous multilinear maps on n variables to
continuous linear maps on E 0, construct the corresponding continuous multilinear map on n+1
variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n)).
Equations
- f.uncurry_right = let f' : multilinear_map 𝕜 (λ (i : fin n), E i.cast_succ) (E (fin.last n) →ₗ[𝕜] E₂) := {to_fun := λ (m : Π (i : fin n), E i.cast_succ), (⇑f m).to_linear_map, map_add' := _, map_smul' := _} in f'.uncurry_right.mk_continuous ∥f∥ _
Given a continuous multilinear map f in n+1 variables, split the last variable to obtain
a continuous multilinear map in n variables into continuous linear maps, given by
m ↦ (x ↦ f (snoc m x)).
Equations
- f.curry_right = let f' : multilinear_map 𝕜 (λ (i : fin n), E i.cast_succ) (E (fin.last n) →L[𝕜] E₂) := {to_fun := λ (m : Π (i : fin n), E i.cast_succ), (⇑(f.to_multilinear_map.curry_right) m).mk_continuous (∥f∥ * finset.univ.prod (λ (i : fin n), ∥m i∥)) _, map_add' := _, map_smul' := _} in f'.mk_continuous ∥f∥ _
The space of continuous multilinear maps on Π(i : fin (n+1)), E i is canonically isomorphic to
the space of continuous multilinear maps on Π(i : fin n), E i.cast_succ with values in the space
of continuous linear maps on E (last n), by separating the last variable. We register this
isomorphism as a linear equiv in continuous_multilinear_curry_right_equiv_aux 𝕜 E E₂.
The algebraic version (without continuity assumption on the maps) is
multilinear_curry_right_equiv 𝕜 E E₂, and the topological isomorphism (registering
additionally that the isomorphism is continuous) is
continuous_multilinear_curry_right_equiv 𝕜 E E₂.
The direct and inverse maps are given by f.uncurry_right and f.curry_right. Use these
unless you need the full framework of linear equivs.
Equations
- continuous_multilinear_curry_right_equiv_aux 𝕜 E E₂ = {to_fun := continuous_multilinear_map.uncurry_right _inst_11, map_add' := _, map_smul' := _, inv_fun := continuous_multilinear_map.curry_right _inst_11, left_inv := _, right_inv := _}
The space of continuous multilinear maps on Π(i : fin (n+1)), E i is canonically isomorphic to
the space of continuous multilinear maps on Π(i : fin n), E i.cast_succ with values in the space
of continuous linear maps on E (last n), by separating the last variable. We register this
isomorphism as a continuous linear equiv in continuous_multilinear_curry_right_equiv 𝕜 E E₂.
The algebraic version (without topology) is given in multilinear_curry_right_equiv 𝕜 E E₂.
The direct and inverse maps are given by f.uncurry_right and f.curry_right. Use these
unless you need the full framework of continuous linear equivs.
Equations
- continuous_multilinear_curry_right_equiv 𝕜 E E₂ = {to_linear_equiv := {to_fun := (continuous_multilinear_curry_right_equiv_aux 𝕜 E E₂).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_multilinear_curry_right_equiv_aux 𝕜 E E₂).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Currying with 0 variables
The space of multilinear maps with 0 variables is trivial: such a multilinear map is just an
arbitrary constant (note that multilinear maps in 0 variables need not map 0 to 0!).
Therefore, the space of continuous multilinear maps on (fin 0) → G with values in E₂ is
isomorphic (and even isometric) to E₂. As this is the zeroth step in the construction of iterated
derivatives, we register this isomorphism.
Associating to a continuous multilinear map in 0 variables the unique value it takes.
Associating to an element x of a vector space E₂ the continuous multilinear map in 0
variables taking the (unique) value x
Equations
- continuous_multilinear_map.curry0 𝕜 G x = {to_multilinear_map := {to_fun := λ (m : fin 0 → G), x, map_add' := _, map_smul' := _}, cont := _}
The linear isomorphism between elements of a normed space, and continuous multilinear maps in
0 variables with values in this normed space. The continuous version is given in
continuous_multilinear_curry_fin0.
The direct and inverse maps are uncurry0 and curry0. Use these unless you need the full
framework of linear equivs.
Equations
- continuous_multilinear_curry_fin0_aux 𝕜 G E₂ = {to_fun := λ (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂), f.uncurry0, map_add' := _, map_smul' := _, inv_fun := λ (f : E₂), continuous_multilinear_map.curry0 𝕜 G f, left_inv := _, right_inv := _}
The continuous linear isomorphism between elements of a normed space, and continuous multilinear
maps in 0 variables with values in this normed space.
The direct and inverse maps are uncurry0 and curry0. Use these unless you need the full
framework of continuous linear equivs.
Equations
- continuous_multilinear_curry_fin0 𝕜 G E₂ = {to_linear_equiv := {to_fun := (continuous_multilinear_curry_fin0_aux 𝕜 G E₂).to_fun, map_add' := _, map_smul' := _, inv_fun := (continuous_multilinear_curry_fin0_aux 𝕜 G E₂).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
With 1 variable
Continuous multilinear maps from G^1 to E₂ are isomorphic with continuous linear maps from
G to E₂.
Equations
- continuous_multilinear_curry_fin1 𝕜 G E₂ = (continuous_multilinear_curry_right_equiv 𝕜 (λ (i : fin 1), G) E₂).symm.trans (continuous_multilinear_curry_fin0 𝕜 G (G →L[𝕜] E₂))