mathlib3

032400bd - feat(analysis/normed_space): more facts about operator norm (#927)

feat(analysis/normed_space): more facts about operator norm (#927) * refactor(analysis/normed_space): refactor and additional lemmas - rename `bounded_linear_maps` to `bounded_linear_map`, `operator_norm` to `op_norm`. - refactor operator norm with an equivalent definition. - change some names and notation to be more consistent with conventions elsewhere in mathlib: replace `bounded_by_*` with `le_*`, `operator_norm_homogeneous` with `op_norm_smul`. - more simp lemmas for bounded_linear_map. - additional results: lipschitz continuity of the operator norm, also that it is submultiplicative. * chore(analysis/normed_space/operator_norm): add attribution * style(analysis/normed_space/operator_norm): use namespace `real` - open `real` instead of `lattice` and omit spurious prefixes. * feat(analysis/normed_space/operator_norm): coercion to linear_map * style(analysis/normed_space/bounded_linear_maps): minor edits - extract variables for brevity of theorem statements. - more consistent naming of variables. * feat(analysis/normed_space/operator_norm): add constructor of bounded_linear_map from is_bounded_linear_map * fix(analysis/normed_space/operator_norm): remove spurious explicit argument * fix(analysis/normed_space): type of bounded linear maps - change the definition of bounded_linear_map to be a type rather than the corresponding subspace, and mark it for unfolding. - rename `bounded_linear_map.from_is_bounded_linear_map` to `is_bounded_linear_map.to_bounded_linear_map`. * feat(analysis/normed_space): analysis results for bounded_linear_maps