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] - feat(analysis/special_functions/complex/arg): review, golf, lemmas #10365
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.
I am glad to see that the ugly continuous_at_arg_of_re_zero
is gone! Thanks.
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Looks like a lemma you used does not exist? My review was too hasty. |
…b into YK-arg-review
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@RemyDegenne It exists in |
…/mathlib into YK-arg-review
…b into YK-arg-review
bors r+ |
…10365) * add `|z| * exp (arg z * I) = z`; * reorder theorems to help golfing; * prove formulas for `arg z` in terms of `arccos (re z / abs z)` in cases `0 < im z` and `im z < 0`; * use them to golf continuity of `arg`.
Pull request successfully merged into master. Build succeeded: |
…10365) * add `|z| * exp (arg z * I) = z`; * reorder theorems to help golfing; * prove formulas for `arg z` in terms of `arccos (re z / abs z)` in cases `0 < im z` and `im z < 0`; * use them to golf continuity of `arg`.
…10365) * add `|z| * exp (arg z * I) = z`; * reorder theorems to help golfing; * prove formulas for `arg z` in terms of `arccos (re z / abs z)` in cases `0 < im z` and `im z < 0`; * use them to golf continuity of `arg`.
…10365) * add `|z| * exp (arg z * I) = z`; * reorder theorems to help golfing; * prove formulas for `arg z` in terms of `arccos (re z / abs z)` in cases `0 < im z` and `im z < 0`; * use them to golf continuity of `arg`.
Add lemmas about the value of `arg (-x)`: one each for positive and negative sign of `x.im`, two `iff` lemmas saying exactly when it's equal to `arg x - π` or `arg x + π`, and a simpler lemma giving the value of `(arg (-x) : real.angle)` for any nonzero `x`. These replace the previous lemmas `arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg` and `arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg`, which are strictly less general (they have a hypothesis `x.re < 0` that's not needed unless the imaginary part is 0). Those two lemmas are unused in current mathlib (they were used in the proof of `cos_arg` before the golfing in #10365) and it seems reasonable to me to replace them with the more general lemmas.
Add lemmas about the value of `arg (-x)`: one each for positive and negative sign of `x.im`, two `iff` lemmas saying exactly when it's equal to `arg x - π` or `arg x + π`, and a simpler lemma giving the value of `(arg (-x) : real.angle)` for any nonzero `x`. These replace the previous lemmas `arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg` and `arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg`, which are strictly less general (they have a hypothesis `x.re < 0` that's not needed unless the imaginary part is 0). Those two lemmas are unused in current mathlib (they were used in the proof of `cos_arg` before the golfing in #10365) and it seems reasonable to me to replace them with the more general lemmas.
|z| * exp (arg z * I) = z
;arg z
in terms ofarccos (re z / abs z)
in cases0 < im z
andim z < 0
;arg
.