Commit 2019-04-17 15:33 032400bd

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