Bounded linear maps #
This file defines a class stating that a map between normed vector spaces is (bi)linear and
Instead of asking for continuity, the definition takes the equivalent condition (because the space
is normed) that
‖f x‖ is bounded by a multiple of
‖x‖. Hence the "bounded" in the name refers to
‖f x‖/‖x‖ rather than
‖f x‖ itself.
Main definitions #
IsBoundedLinearMap: Class stating that a map
f : E → Fis linear and has
‖f x‖bounded by a multiple of
IsBoundedBilinearMap: Class stating that a map
f : E × F → Gis bilinear and continuous, but through the simpler to provide statement that
‖f (x, y)‖is bounded by a multiple of
‖x‖ * ‖y‖
IsBoundedBilinearMap.linearDeriv: Derivative of a continuous bilinear map as a linear map.
IsBoundedBilinearMap.deriv: Derivative of a continuous bilinear map as a continuous linear map. The proof that it is indeed the derivative is
Main theorems #
IsBoundedBilinearMap.continuous: A bounded bilinear map is continuous.
ContinuousLinearEquiv.isOpen: The continuous linear equivalences are an open subset of the set of continuous linear maps between a pair of Banach spaces. Placed in this file because its proof uses
The main use of this file is
IsBoundedBilinearMap. The file
already expounds the theory of multilinear maps, but the
2-variables case is sufficiently simpler
to currently deserve its own treatment.
IsBoundedLinearMap is effectively an unbundled version of
Topology.Algebra.Module.Basic, theory over normed spaces developed in
Analysis.NormedSpace.OperatorNorm), albeit the name disparity. A bundled
ContinuousLinearMap is to be preferred over an
IsBoundedLinearMap hypothesis. Historical
IsBoundedLinearMap 𝕜 f if it is linear and satisfies the
‖f x‖ ≤ M * ‖x‖ for some positive constant
Construct a linear map from a function
IsBoundedLinearMap 𝕜 f.
Construct a continuous linear map from
Taking the cartesian product of two continuous multilinear maps is a bounded linear operation.
Given a fixed continuous linear map
g, associating to a continuous multilinear map
continuous multilinear map
f (g m₁, ..., g mₙ) is a bounded linear operation.
We prove some computation rules for continuous (semi-)bilinear maps in their first argument.
f is a continuous bilinear map, to use the corresponding rules for the second argument, use
(f _).map_add and similar.
We have to assume that
G are normed spaces in this section, to use
ContinuousLinearMap.toNormedAddCommGroup, but we don't need to assume this for the first
f : E × F → G satisfies
IsBoundedBilinearMap 𝕜 f if it is bilinear and
A bounded bilinear map
f : E × F → G defines a continuous linear map
f : E →L[𝕜] F →L[𝕜] G.
Useful to use together with
Useful to use together with
ContinuousLinearMap.smulRight, associating to a continuous linear map
f : E → 𝕜 and a scalar
c : F the tensor product
f ⊗ c as a continuous linear map from
F, is a bounded bilinear map.
The composition of a continuous linear map with a continuous multilinear map is a bounded bilinear operation.
Definition of the derivative of a bilinear map
f, given at a point
q ↦ f(p.1, q.2) + f(q.1, p.2) as in the standard formula for the derivative of a product.
We define this function here as a linear map
E × F →ₗ[𝕜] G, then
strengthens it to a continuous linear map
E × F →L[𝕜] G.
The derivative of a bounded bilinear map at a point
p : E × F, as a continuous linear map
E × F to
G. The statement that this is indeed the derivative of
ContinuousLinearMap.mulLeftRight : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜') is a bounded
Given a bounded bilinear map
f, the map associating to a point
p the derivative of
p is itself a bounded linear map.
The set of continuous linear equivalences between two Banach spaces is open #
In this section we establish that the set of continuous linear equivalences between two Banach spaces is an open subset of the space of linear maps between them.