-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(data/is_R_or_C,analysis/inner_product_space): review API #18919
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given this PR is so large, I think mixing in the changes to synchronized files is a bad idea. Can you split those out as a precursor PR?
Cherry-picked to new PRs, added as dependencies, removed from PR description. |
/-- Inner product defined by the `inner_product_space.core` structure. -/ | ||
def to_has_inner : has_inner 𝕜 F := { inner := c.inner } | ||
def to_has_inner : has_inner 𝕜 F := c.to_has_inner |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not delete this and use the base-class projection?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For some reason, both inner_product_space
and inner_product_space.core
are defined as @[class] structure
, so the projection takes c
as an explicit argument.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…chwarz (#18938) ## API changes - Add `inner_product_space.to_core`. - Make `inner_product_space.core` extend `has_inner`. - Rename namespace from `inner_product_space.of_core` to `inner_product_space.core`. - Rename `inner_product_space.of_core.inner_norm_sq_eq_inner_self` to `inner_product_space.core.coe_norm_sq_eq_inner_self`. - Add `inner_product_space.core.norm_inner_symm`. - Add `inner_product_space.core.cauchy_schwarz_aux`, use it to golf the proof of the Cauchy-Schwarz inequality and its versions. - Use norm instead of `is_R_or_C.abs` here and there, the rest will migrate in #18919. - Rename `inner_product_space.of_core.abs_inner_le_norm` to `inner_product_space.core.norm_inner_le_norm`, use norm. - Add `norm_inner_eq_norm_tfae` and `inner_eq_norm_mul_iff_div`. - Rename `abs_inner_div_norm_mul_norm_eq_one_iff` to `norm_inner_div_norm_mul_norm_eq_one_iff`, use norm. - Rename `inner_eq_norm_mul_iff_of_norm_one` to `inner_eq_one_iff_of_norm_one`. Co-authored-by: Johan Commelin <johan@commelin.net>
Can you update the description to reflect what was has already been merged, if you haven't done so already? Thanks for the split! |
@eric-wieser I've rewritten the PR description from scratch. |
@[simp, is_R_or_C_simps] lemma bit0_re (z : K) : re (bit0 z) = bit0 (re z) := map_bit0 _ _ | ||
|
||
@[simp, is_R_or_C_simps] lemma bit1_re (z : K) : re (bit1 z) = bit1 (re z) := | ||
by simp only [bit1, map_add, bit0_re, one_re] | ||
|
||
@[simp, is_R_or_C_simps] lemma bit0_im (z : K) : im (bit0 z) = bit0 (im z) := map_bit0 _ _ | ||
|
||
@[simp, is_R_or_C_simps] lemma bit1_im (z : K) : im (bit1 z) = bit0 (im z) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit: could skip adding these spaces
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I prefer to have them because the bit1
lemmas don't fit on 1 line.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…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>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Drop
is_R_or_C.abs
and lemmas about itUse
has_norm.norm
instead. The norm is definitionally equal both toreal.abs
andcomplex.abs
, so it's easier to specialize generictheorems to real numbers. Also, we don't have to convert between norm
and
is_R_or_C.abs
here and there.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
is_R_or_C.of_real_smul
tois_R_or_C.real_smul_of_real
.is_R_or_C.norm_real
,is_R_or_C.norm_of_real
, andis_R_or_C.abs_of_real
intois_R_or_C.norm_of_real
.is_R_or_C.abs_of_nat
andis_R_or_C.abs_cast_nat
intois_R_or_C.norm_nat_cast
, usehas_norm.norm
, make it asimp, priority 900, is_R_or_C_simps, norm_cast
lemma.is_R_or_C.mul_self_abs
tois_R_or_C.mul_self_norm
, usehas_norm.norm
.is_R_or_C.abs_two
tois_R_or_C.norm_two
, usehas_norm.norm
.is_R_or_C.abs_conj
tois_R_or_C.norm_conj
, usehas_norm.norm
.is_R_or_C.abs_re_le_abs
tois_R_or_C.abs_re_le_norm
, usehas_norm.norm
.is_R_or_C.abs_im_le_abs
tois_R_or_C.abs_im_le_norm
, usehas_norm.norm
.is_R_or_C.re_le_abs
andis_R_or_C.im_le_abs
tois_R_or_C.re_le_norm
andis_R_or_C.im_le_norm
, respectively; usehas_norm.norm
.has_norm.norm
inis_R_or_C.im_eq_zero_of_le
andis_R_or_C.re_eq_self_of_le
.is_R_or_C.abs_re_div_abs_le_one
andis_R_or_C.abs_im_div_abs_le_one
tois_R_or_C.abs_re_div_norm_le_one
andis_R_or_C.abs_im_div_norm_le_one
, respectively; usehas_norm.norm
.is_R_or_C.re_eq_abs_of_mul_conj
tois_R_or_C.re_eq_norm_of_mul_conj
, usehas_norm.norm
.is_R_or_C.abs_sq_re_add_conj
andis_R_or_C.abs_sq_re_add_conj'
tois_R_or_C.norm_sq_re_add_conj
and
is_R_or_C.norm_sq_re_conj_add
, respectively; usehas_norm.norm
.has_norm.norm
in all lemmas/definitions aboutis_cau_seq
andcau_seq
sequences ofis_R_or_C
numbers.is_R_or_C.is_cau_seq_abs
tois_R_or_C.is_cau_seq_norm
,use
has_norm.norm
.Inner products
inner_product_space.core.inner_mul_conj_re_abs
toinner_product_space.core.inner_mul_symm_re_eq_norm
, usehas_norm.norm
.inner_self_re_abs
toinner_self_re_eq_norm
, usehas_norm.norm
.inner_self_abs_to_K
toinner_self_norm_to_K
, usehas_norm.norm
.abs_inner_symm
tonorm_inner_symm
, usehas_norm.norm
.abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
tonorm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
, usehas_norm.norm
.Add lemmas
is_R_or_C.is_real_tfae
andis_real_tfae.conj_eq_iff_im
.is_R_or_C.norm_sq_apply
.Change attributes
is_R_or_C.zero_re'
is no longer asimp
lemmais_R_or_C.norm_conj
is now asimp
lemma.Misc
abs_norm_eq_norm
toabs_norm
#18921eq_conj_iff_*
lemmas #18922