Commit 2022-07-19 18:28 65a44e6f

feat(analysis/normed_space/operator_norm): add 2 new versions of op_norm_le_* (#15417)

• continuous_linear_map.op_norm_le_bound' requires an estimate on ∥f x∥ for any x, ∥x∥ ≠ 0;
• continuous_linear_map.op_norm_le_of_unit_norm works only for real linear map and requires that ∥f x∥ ≤ C for all x, ∥x∥ = 1.