# mathlibdocumentation

analysis.normed_space.bounded_linear_maps

# 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 map f : E → F is linear and has ∥f x∥ bounded by a multiple of ∥x∥.
• is_bounded_bilinear_map: Class stating that a map f : 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 is is_bounded_bilinear_map.has_fderiv_at in analysis.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 uses is_bounded_bilinear_map.continuous.

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, 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.