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.

Construct a continuous linear map from is_bounded_linear_map

A map f : E × F → G satisfies is_bounded_bilinear_map 𝕜 f if it is bilinear and continuous.

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 a bounded linear map from E × F to G. The fact that this is indeed the derivative of f is proved in is_bounded_bilinear_map.has_fderiv_at in deriv.lean

The derivative of a bounded bilinear map at a point p : E × F, as a continuous linear map from E × F to G.

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.