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 a bounded linear map from
E × F to
G. The fact that this
is indeed the derivative of
f is proved in
The derivative of a bounded bilinear map at a point
p : E × F, as a continuous linear map
E × F to
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.