Commit 2023-05-08 02:00 3f655f52

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.