Continuous 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 declarations #
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
linear_map.norm_apply_of_isometry: A linear isometry preserves the norm.
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, 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
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.
- 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
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
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
p is itself a bounded linear map.
Construct a continuous linear equiv from a linear map that is also an isometry with full range.