Bounded linear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
is_bounded_linear_map: Class stating that a map
f : E → Fis linear and has
‖f x‖bounded by a multiple of
is_bounded_bilinear_map: 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‖
is_bounded_bilinear_map.linear_deriv: Derivative of a continuous bilinear map as a linear map.
is_bounded_bilinear_map.deriv: Derivative of a continuous bilinear map as a continuous linear map. The proof that it is indeed the derivative is
Main theorems #
is_bounded_bilinear_map.continuous: A bounded bilinear map is continuous.
continuous_linear_equiv.is_open: 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
is_bounded_bilinear_map. The file
already expounds the theory of multilinear maps, but the
2-variables case is sufficiently simpler
to currently deserve its own treatment.
is_bounded_linear_map is effectively an unbundled version of
topology.algebra.module.basic, theory over normed spaces developed in
analysis.normed_space.operator_norm), albeit the name disparity. A bundled
continuous_linear_map is to be preferred over a
is_bounded_linear_map hypothesis. Historical
is_bounded_linear_map 𝕜 f if it is linear and satisfies the
‖f x‖ ≤ M * ‖x‖ for some positive constant
A continuous linear map satisfies
Construct a linear map from a function
is_bounded_linear_map 𝕜 f.
Construct a continuous linear map from is_bounded_linear_map
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 continuuous 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
continuous_linear_map.to_normed_add_comm_group, but we don't need to assume this for the first
- add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
- smul_left : ∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)
- add_right : ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
- smul_right : ∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)
- bound : ∃ (C : ℝ) (H : C > 0), ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
f : E × F → G satisfies
is_bounded_bilinear_map 𝕜 f if it is bilinear and
Useful to use together with
Useful to use together with
continuous_linear_map.smul_right, 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
continuous_linear_map.mul_left_right : 𝕜' × 𝕜' → (𝕜' →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.