Bounded linear maps #
This file defines a class stating that a map between normed vector spaces is (bi)linear and
continuous.
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 mapf : E → F
is linear and has∥f x∥
bounded by a multiple of∥x∥
.is_bounded_bilinear_map
: Class stating that a mapf : E × F → G
is 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 isis_bounded_bilinear_map.has_fderiv_at
inanalysis.calculus.fderiv
.
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 usesis_bounded_bilinear_map.continuous
.
Notes #
The main use of this file is is_bounded_bilinear_map
. The file analysis.normed_space.multilinear
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 continuous_linear_map
(defined
in 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
artifact, really.
A function f
satisfies is_bounded_linear_map 𝕜 f
if it is linear and satisfies the
inequality ∥f x∥ ≤ M * ∥x∥
for some positive constant M
.
A continuous linear map satisfies is_bounded_linear_map
Construct a linear map from a function f
satisfying is_bounded_linear_map 𝕜 f
.
Equations
Construct a continuous linear map from is_bounded_linear_map
Equations
- hf.to_continuous_linear_map = {to_linear_map := {to_fun := (is_bounded_linear_map.to_linear_map f hf).to_fun, map_add' := _, map_smul' := _}, cont := _}
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 f
the
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.
If 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 F
and 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
argument of f
.
- 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∥
A map f : E × F → G
satisfies is_bounded_bilinear_map 𝕜 f
if it is bilinear and
continuous.
Useful to use together with continuous.comp₂
.
Useful to use together with continuous.comp₂
.
The function 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 E
to
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 p
by
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 is_bounded_bilinear_map.deriv
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
from E × F
to G
. The statement that this is indeed the derivative of f
is
is_bounded_bilinear_map.has_fderiv_at
in analysis.calculus.fderiv
.
Equations
- h.deriv p = (h.linear_deriv p).mk_continuous_of_exists_bound _
The function lmul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')
is a bounded bilinear map.
Given a bounded bilinear map f
, the map associating to a point p
the derivative of f
at
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.