mathlib3

3f655f52 - refactor(data/is_R_or_C,analysis/inner_product_space): review API (#18919)

refactor(data/is_R_or_C,analysis/inner_product_space): review API (#18919) ## Drop `is_R_or_C.abs` and lemmas about it Use `has_norm.norm` instead. The norm is definitionally equal both to `real.abs` and `complex.abs`, so it's easier to specialize generic theorems to real numbers. Also, we don't have to convert between norm and `is_R_or_C.abs` here and there. - Drop `is_R_or_C.abs`, `is_R_or_C.norm_eq_abs`, `is_R_or_C.abs_of_nonneg`, `is_R_or_C.abs_zero`, `is_R_or_C.abs_one`, `is_R_or_C.abs_nonneg`, `is_R_or_C.abs_eq_zero`, `is_R_or_C.abs_ne_zero`, `is_R_or_C.abs_mul`, `is_R_or_C.abs_add`, `is_R_or_C.is_absolute_value`, `is_R_or_C.abs_abs`, `is_R_or_C.abs_pos`, `is_R_or_C.abs_neg`, `is_R_or_C.abs_inv`, `is_R_or_C.abs_div`, `is_R_or_C.abs_abs_sub_le_abs_sub`, `is_R_or_C.norm_sq_eq_abs`, `is_R_or_C.abs_to_real`, `is_R_or_C.continuous_abs`, `is_R_or_C.abs_to_complex`, `inner_product_space.core.abs_inner_symm`, `abs_inner_le_norm`. ## Rename/merge lemmas ### `is_R_or_C` - Rename `is_R_or_C.of_real_smul` to `is_R_or_C.real_smul_of_real`. - Merge `is_R_or_C.norm_real`, `is_R_or_C.norm_of_real`, and `is_R_or_C.abs_of_real` into `is_R_or_C.norm_of_real`. - Merge `is_R_or_C.abs_of_nat` and `is_R_or_C.abs_cast_nat` into `is_R_or_C.norm_nat_cast`, use `has_norm.norm`, make it a `simp, priority 900, is_R_or_C_simps, norm_cast` lemma. - Rename `is_R_or_C.mul_self_abs` to `is_R_or_C.mul_self_norm`, use `has_norm.norm`. - Rename `is_R_or_C.abs_two` to `is_R_or_C.norm_two`, use `has_norm.norm`. - Rename `is_R_or_C.abs_conj` to `is_R_or_C.norm_conj`, use `has_norm.norm`. - Rename `is_R_or_C.abs_re_le_abs` to `is_R_or_C.abs_re_le_norm`, use `has_norm.norm`. - Rename `is_R_or_C.abs_im_le_abs` to `is_R_or_C.abs_im_le_norm`, use `has_norm.norm`. - Rename `is_R_or_C.re_le_abs` and `is_R_or_C.im_le_abs` to `is_R_or_C.re_le_norm` and `is_R_or_C.im_le_norm`, respectively; use `has_norm.norm`. - Use `has_norm.norm` in `is_R_or_C.im_eq_zero_of_le` and `is_R_or_C.re_eq_self_of_le`. - Rename `is_R_or_C.abs_re_div_abs_le_one` and `is_R_or_C.abs_im_div_abs_le_one` to `is_R_or_C.abs_re_div_norm_le_one` and `is_R_or_C.abs_im_div_norm_le_one`, respectively; use `has_norm.norm`. - Rename `is_R_or_C.re_eq_abs_of_mul_conj` to `is_R_or_C.re_eq_norm_of_mul_conj`, use `has_norm.norm`. - Rename `is_R_or_C.abs_sq_re_add_conj` and `is_R_or_C.abs_sq_re_add_conj'` to `is_R_or_C.norm_sq_re_add_conj` and `is_R_or_C.norm_sq_re_conj_add`, respectively; use `has_norm.norm`. - Use `has_norm.norm` in all lemmas/definitions about `is_cau_seq` and `cau_seq` sequences of `is_R_or_C` numbers. - Rename `is_R_or_C.is_cau_seq_abs` to `is_R_or_C.is_cau_seq_norm`, use `has_norm.norm`. ### Inner products - Rename `inner_product_space.core.inner_mul_conj_re_abs` to `inner_product_space.core.inner_mul_symm_re_eq_norm`, use `has_norm.norm`. - Do the same in the root NS. - Rename `inner_self_re_abs` to `inner_self_re_eq_norm`, use `has_norm.norm`. - Rename `inner_self_abs_to_K` to `inner_self_norm_to_K`, use `has_norm.norm`. - Rename `abs_inner_symm` to `norm_inner_symm`, use `has_norm.norm`. - Rename `abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul` to `norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul`, use `has_norm.norm`. ## Add lemmas - Add `is_R_or_C.is_real_tfae` and `is_real_tfae.conj_eq_iff_im`. - Add `is_R_or_C.norm_sq_apply`. ## Change attributes - `is_R_or_C.zero_re'` is no longer a `simp` lemma - `is_R_or_C.norm_conj` is now a `simp` lemma. ## Misc - Reorder lemmas here and there to golf. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>