[Merged by Bors] - refactor(data/is_R_or_C,analysis/inner_product_space): review API by urkud · Pull Request #18919 · leanprover-community/mathlib3

urkud · 2023-05-02T20:00:46Z

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.

eric-wieser

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?

urkud · 2023-05-02T20:58:26Z

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.

eric-wieser · 2023-05-02T22:14:29Z

src/analysis/inner_product_space/basic.lean

 /-- 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


Why not delete this and use the base-class projection?

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.

src/analysis/inner_product_space/basic.lean

src/linear_algebra/matrix/hermitian.lean

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>

eric-wieser · 2023-05-05T08:16:11Z

Can you update the description to reflect what was has already been merged, if you haven't done so already? Thanks for the split!

urkud · 2023-05-06T02:16:37Z

@eric-wieser I've rewritten the PR description from scratch.

eric-wieser · 2023-05-07T21:48:13Z

src/data/is_R_or_C/basic.lean

 @[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) :=


nit: could skip adding these spaces

I prefer to have them because the bit1 lemmas don't fit on 1 line.

eric-wieser

bors d+

Thanks!

bors · 2023-05-07T21:50:07Z

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

urkud · 2023-05-08T01:59:55Z

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>

bors · 2023-05-08T03:39:35Z

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

urkud added 9 commits April 30, 2023 02:27

Snapshot

c0244b3

Update

fba7467

Update

1178bf4

Snapshot

53d1728

Update

ad694d7

Update

04353c2

Fix compile

ee3e91d

Fix 100.yaml

31b7d49

Fix typos etc

44d775c

urkud requested a review from a team as a code owner May 2, 2023 20:00

github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 2, 2023

urkud added awaiting-review The author would like community review of the PR mathport For compatibility with Lean 4 changes, to simplify porting t-analysis Analysis (normed *, calculus) labels May 2, 2023

eric-wieser suggested changes May 2, 2023

View reviewed changes

ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 2, 2023

Update

a8371b6

eric-wieser reviewed May 2, 2023

View reviewed changes

src/analysis/inner_product_space/basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 2, 2023

View reviewed changes

src/analysis/inner_product_space/basic.lean Show resolved Hide resolved

eric-wieser reviewed May 2, 2023

View reviewed changes

src/linear_algebra/matrix/hermitian.lean Outdated Show resolved Hide resolved

eric-wieser mentioned this pull request May 2, 2023

[Merged by Bors] - chore(data/{complex,is_R_or_C}/basic): fix name of eq_conj_iff_* lemmas #18922

Closed

urkud and others added 6 commits May 2, 2023 21:09

Update src/analysis/inner_product_space/basic.lean

00362c8

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Merge branch 'master' into YK-isrc

6db2da6

Snapshot

4da05c3

Merge branch 'master' into YK-R-or-C-golf

0f6148c

Drop a simp

8c7bc32

Merge branch 'YK-R-or-C-golf' into YK-isrc

07faf23

ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 4, 2023

Merge branch 'master' into YK-isrc

d143d1b

urkud mentioned this pull request May 4, 2023

[Merged by Bors] - chore(analysis/inner_product_space/basic): golf the proof of Cauchy-Schwarz #18938

Closed

urkud added 8 commits May 4, 2023 09:08

Merge branch 'master' into YK-isrc

1ecf609

Snapshot

1350fac

Fix

2013354

Merge branch 'YK-conj-mul' into YK-isrc

a6cf067

Update

91bf6d9

Merge branch 'master' into YK-conj-mul

f222162

Merge branch 'YK-conj-mul' into YK-isrc

c867492

Fix merge

aecd465

urkud added 2 commits May 5, 2023 19:33

Drop some simps

d2ba7d9

Fix names

0920400

urkud removed the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 6, 2023

urkud mentioned this pull request May 7, 2023

[Merged by Bors] - feat: port Data.IsROrC.Basic leanprover-community/mathlib4#3654

Closed

1 task

Merge remote-tracking branch 'origin/master' into YK-isrc

02b6763

eric-wieser reviewed May 7, 2023

View reviewed changes

eric-wieser approved these changes May 7, 2023

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels May 7, 2023

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label May 8, 2023

bors bot changed the title ~~refactor(data/is_R_or_C,analysis/inner_product_space): review API~~ [Merged by Bors] - refactor(data/is_R_or_C,analysis/inner_product_space): review API May 8, 2023

bors bot closed this May 8, 2023

bors bot deleted the YK-isrc branch May 8, 2023 03:39

Conversation

urkud commented May 2, 2023 • edited by Parcly-Taxel Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Drop is_R_or_C.abs and lemmas about it

Rename/merge lemmas

is_R_or_C

Inner products

Add lemmas

Change attributes

Misc

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

urkud commented May 2, 2023

Uh oh!

eric-wieser May 2, 2023

Choose a reason for hiding this comment

Uh oh!

urkud May 3, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented May 5, 2023

Uh oh!

urkud commented May 6, 2023

Uh oh!

eric-wieser May 7, 2023

Choose a reason for hiding this comment

Uh oh!

urkud May 8, 2023

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

bors bot commented May 7, 2023

Uh oh!

urkud commented May 8, 2023

Uh oh!

bors bot commented May 8, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

urkud commented May 2, 2023 •

edited by Parcly-Taxel

Loading

Drop `is_R_or_C.abs` and lemmas about it

`is_R_or_C`