Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(analysis/special_functions/arsinh): inverse hyperbolic sine function #3801

Closed
wants to merge 62 commits into from
Closed

[Merged by Bors] - feat(analysis/special_functions/arsinh): inverse hyperbolic sine function #3801

wants to merge 62 commits into from

Conversation

jamesa9283
Copy link
Collaborator

Added the following lemmas and definitions:
cosh_def
sinh_def
cosh_pos
sinh_strict_mono
sinh_injective
sinh_surjective
sinh_bijective
real.cosh_sq_sub_sinh_sq
sqrt_one_add_sinh_sq
sinh_arsinh
arsinh_sin

This is from the list of UG not in lean. cosh coming soon.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 15, 2020
@jamesa9283 jamesa9283 changed the title Arsinh feat(analysis/special_functions/arsinh) - arsinh code Aug 15, 2020
@jamesa9283
Copy link
Collaborator Author

Its decided to commit the docstrings from earlier aswell... help!

@jamesa9283 jamesa9283 added easy < 20s of review time. See the lifecycle page for guidelines. help-wanted The author needs attention to resolve issues labels Aug 15, 2020
@jcommelin
Copy link
Member

I think you did git checkout -b arsinh while you were still on your docstring branch.
If you are interested in learning how to fix this using git, you can read a tutorial on how to git rebase onto master.

Also... I'm not sure if all these functions should go into a file named arsinh.lean. Isn't there a better name that covers these?

@rwdrich
Copy link

rwdrich commented Aug 15, 2020

Would you like to make a pull request for just c7efc79, and not 88e9a35 ?

If so, I think you want to use git rebase here.

If so, I think you will want to use git rebase -i HEAD~2. This will open up your git editor (I think the default is nano) for you to rebase.
You will then probably want to edit the word 'pick' in front of the commit you no longer want, and then save and exit the file. You'll then need to force push those changes to this branch

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 15, 2020
@jamesa9283
Copy link
Collaborator Author

Thanks! All dealt with! I may rejig some of the lemmas

@jamesa9283 jamesa9283 removed the help-wanted The author needs attention to resolve issues label Aug 15, 2020
TwoFX
TwoFX reviewed Aug 15, 2020
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have added some stylistic comments, nothing of substance.

src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/data/complex/exponential.lean Outdated Show resolved Hide resolved
src/data/complex/exponential.lean Outdated Show resolved Hide resolved
@digama0
Copy link
Member

digama0 commented Aug 15, 2020

I've never heard the name arsinh before. This is the inverse hyperbolic sine, right? How about arcsinh?

@jamesa9283
Copy link
Collaborator Author

WRT arsinh, if you look at the nomenclature, with arc in arcsin refers to the latin arcus, as you are referring to an arc in a circle. However with sinh there isnt an arc to refer to, it's an area, so its shortened to arsinh

shingtaklam1324
shingtaklam1324 reviewed Aug 16, 2020
View reviewed changes
Copy link
Collaborator

@shingtaklam1324 shingtaklam1324 left a comment •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some comments here.

You seem to have a lot of

have foo := bar,
linarith

and then foo is never used again. You can probably refactor these and pass in the proofs to linarith as linarith [bar], but it's not a major issue imo.

src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
@shingtaklam1324 shingtaklam1324 added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 16, 2020
jamesa9283 and others added 7 commits August 16, 2020 12:17
@jamesa9283 @jcommelin
Update src/data/complex/exponential.lean
dee5af0 
Renamed `sinh_def` to `sinh_eq`

Co-authored-by: Johan Commelin <johan@commelin.net>
@jamesa9283 @TwoFX
Update src/analysis/special_functions/arsinh.lean
0c06846 
added space after `sqrt` in `b_lt_sqrt_b_sq_add_one`

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@jamesa9283
added @[pp_nodot] to log
1a06848
@jamesa9283
Removed .sqrt in favour of the sqrt (f x)
a312928
@jamesa9283
added def to arsinh docstring
24923cf
@jamesa9283 @TwoFX
Update src/analysis/special_functions/arsinh.lean
c1a06f3 
removed braces around apply `pow_two_nonneg`

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@jamesa9283 @TwoFX
Update src/analysis/special_functions/arsinh.lean
f4bbe0d 
Moved braces on line 95

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
@jamesa9283 @TwoFX
Update src/analysis/special_functions/arsinh.lean
c010972 
removed new line brace

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
kckennylau
kckennylau requested changes Aug 17, 2020
View reviewed changes
Copy link
Collaborator

@kckennylau kckennylau left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

kill all rings

src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/data/complex/exponential.lean Outdated Show resolved Hide resolved
src/data/complex/exponential.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
jamesa9283 and others added 4 commits August 17, 2020 14:39
@jamesa9283 @kckennylau
Update src/analysis/special_functions/arsinh.lean
1f9edf5 
added spaces around `^`

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
@jamesa9283 @kckennylau
Update src/analysis/special_functions/arsinh.lean
d15b088 
rewritten proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
@jamesa9283 @kckennylau
Update src/data/complex/exponential.lean
3cf9ff0 
rewritten proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
@jamesa9283 @kckennylau
Update src/analysis/special_functions/arsinh.lean
8851ea6 
simplifies proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
@kckennylau
Copy link
Collaborator

You can commit all the suggestions together if go to the "files changed" tab

jamesa9283
jamesa9283 commented Aug 18, 2020
View reviewed changes
Copy link
Collaborator Author

@jamesa9283 jamesa9283 left a comment •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it builds nicely, I think I've implemented all the changes! :)

@jamesa9283 jamesa9283 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 18, 2020
shingtaklam1324
shingtaklam1324 reviewed Aug 19, 2020
View reviewed changes
Copy link
Collaborator

@shingtaklam1324 shingtaklam1324 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One final comment. Otherwise LGTM.

src/analysis/special_functions/arsinh.lean Outdated Show resolved Hide resolved
@robertylewis
Copy link
Member

@shingtaklam1324 @TwoFX @kckennylau thank you all for the careful reviewing, and @jamesa9283 thank you for the PR!

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 21, 2020
@jamesa9283
Copy link
Collaborator Author

jamesa9283 commented Aug 21, 2020 •
edited

It's ok :D

bors bot pushed a commit that referenced this pull request Aug 21, 2020
@jamesa9283
feat(analysis/special_functions/arsinh): inverse hyperbolic sine func…
4921be9 
…tion (#3801)

Added the following lemmas and definitions:
`cosh_def`
`sinh_def`
`cosh_pos`
`sinh_strict_mono`
`sinh_injective`
`sinh_surjective`
`sinh_bijective`
`real.cosh_sq_sub_sinh_sq`
`sqrt_one_add_sinh_sq`
`sinh_arsinh`
`arsinh_sin`

This is from the list of UG not in lean. `cosh` coming soon.
@bors
Copy link

bors bot commented Aug 21, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions/arsinh): inverse hyperbolic sine function [Merged by Bors] - feat(analysis/special_functions/arsinh): inverse hyperbolic sine function Aug 21, 2020
@bors bors bot closed this Aug 21, 2020
@bors bors bot deleted the arsinh branch August 21, 2020 12:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rwbarton rwbarton rwbarton left review comments

@TwoFX TwoFX TwoFX left review comments

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@jcommelin jcommelin jcommelin left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

@jsm28 jsm28 jsm28 left review comments

@shingtaklam1324 shingtaklam1324 shingtaklam1324 left review comments

@kckennylau kckennylau kckennylau approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet