-
Notifications
You must be signed in to change notification settings - Fork 297
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(data/is_R_or_C,analysis/inner_product_space): review API (#1…
…8919) ## 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>
- Loading branch information
1 parent
b1c0175
commit 3f655f5
Showing
16 changed files
with
197 additions
and
328 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.