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

Commits on Aug 15, 2020

  1. Added sinh.lean

    @jamesa9283
    jamesa9283 committed Aug 15, 2020
    Configuration menu
    Copy the full SHA
    38ab7a0 View commit details
    Browse the repository at this point in the history

  2. Rejigged some lemmas

    @jamesa9283
    jamesa9283 committed Aug 15, 2020
    Configuration menu
    Copy the full SHA
    ada137d View commit details
    Browse the repository at this point in the history

  3. Removed arsinh from notation and added it to results

    @jamesa9283
    jamesa9283 committed Aug 15, 2020
    Configuration menu
    Copy the full SHA
    3bc5e7c View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2020

  1. Update src/data/complex/exponential.lean 

    Renamed `sinh_def` to `sinh_eq`

Co-authored-by: Johan Commelin <johan@commelin.net>
    @jamesa9283 @jcommelin
    jamesa9283 and jcommelin committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    dee5af0 View commit details
    Browse the repository at this point in the history

  2. Update src/analysis/special_functions/arsinh.lean 

    added space after `sqrt` in `b_lt_sqrt_b_sq_add_one`

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    0c06846 View commit details
    Browse the repository at this point in the history

  3. added @[pp_nodot] to log

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    1a06848 View commit details
    Browse the repository at this point in the history

  4. Removed .sqrt in favour of the sqrt (f x)

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    a312928 View commit details
    Browse the repository at this point in the history

  5. added def to arsinh docstring

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    24923cf View commit details
    Browse the repository at this point in the history

  6. Update src/analysis/special_functions/arsinh.lean 

    removed braces around apply `pow_two_nonneg`

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    c1a06f3 View commit details
    Browse the repository at this point in the history

  7. Update src/analysis/special_functions/arsinh.lean 

    Moved braces on line 95

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    f4bbe0d View commit details
    Browse the repository at this point in the history

  8. Update src/analysis/special_functions/arsinh.lean 

    Replaced `sinm` with `sihn`

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    238a190 View commit details
    Browse the repository at this point in the history

  9. Updated sinh/cosh_def to sinh/cosh_eq

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    8ecda92 View commit details
    Browse the repository at this point in the history

  10. Added braces and commas to sinh/cosh_eq

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    3d7a6a5 View commit details
    Browse the repository at this point in the history

  11. removed braces after single command haves

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    53e8231 View commit details
    Browse the repository at this point in the history

  12. added extra tags

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    2071494 View commit details
    Browse the repository at this point in the history

  13. Update src/analysis/special_functions/arsinh.lean 

    Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
    @jamesa9283 @fpvandoorn
    jamesa9283 and fpvandoorn committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    79bb7b6 View commit details
    Browse the repository at this point in the history

  14. Merge branch 'arsinh' of https://github.com/leanprover-community/mathlib 

     into arsinh
    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    97555a6 View commit details
    Browse the repository at this point in the history

  15. replaced sinm with sinh

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    a69e47e View commit details
    Browse the repository at this point in the history

  16. updared aux_lemma to remove error

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    c6a8bc8 View commit details
    Browse the repository at this point in the history

  17. moved real.cosh_sq_add_sinh_sq

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    0a3d084 View commit details
    Browse the repository at this point in the history

  18. reduced imports

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    e643c7d View commit details
    Browse the repository at this point in the history

  19. added braces to aux_lemma

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    457af70 View commit details
    Browse the repository at this point in the history

  20. added braces to b_lt_b_sq_add_one

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    9752231 View commit details
    Browse the repository at this point in the history

  21. updated sinh_surjective

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    46486eb View commit details
    Browse the repository at this point in the history

  22. relocated real.cosh_sq_sub_sinh_sq

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    2eee37a View commit details
    Browse the repository at this point in the history

  23. relocated arsinh

    @jamesa9283
    jamesa9283 committed Aug 16, 2020
    Configuration menu
    Copy the full SHA
    2ed1a1a View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2020

  1. Update src/analysis/special_functions/arsinh.lean 

    Removed local attribute

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    e8566a2 View commit details
    Browse the repository at this point in the history

  2. Update src/data/complex/exponential.lean 

    Renamed

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    cf37673 View commit details
    Browse the repository at this point in the history

  3. Update src/analysis/special_functions/arsinh.lean 

    Removed `ring`

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    04bbe11 View commit details
    Browse the repository at this point in the history

  4. Update src/analysis/special_functions/arsinh.lean 

    Replaced G.symm with \l G

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    92666be View commit details
    Browse the repository at this point in the history

  5. Update src/analysis/special_functions/arsinh.lean 

    Updated the names in Key Results

Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    72c83b9 View commit details
    Browse the repository at this point in the history

  6. moved defs

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    25a685f View commit details
    Browse the repository at this point in the history

  7. Merge branch 'arsinh' of https://github.com/leanprover-community/mathlib 

     into arsinh
    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    ef483cf View commit details
    Browse the repository at this point in the history

  8. Trying to make lean happy

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    78e5600 View commit details
    Browse the repository at this point in the history

  9. removed real on cosh_sq_sih_sq

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    d0df08b View commit details
    Browse the repository at this point in the history

  10. Update src/analysis/special_functions/arsinh.lean 

    Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    fefc5bb View commit details
    Browse the repository at this point in the history

  11. Update src/data/complex/exponential.lean 

    Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    23e01e1 View commit details
    Browse the repository at this point in the history

  12. Update src/data/complex/exponential.lean 

    Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    13d337a View commit details
    Browse the repository at this point in the history

  13. Update src/data/complex/exponential.lean 

    Co-authored-by: Shing Tak Lam <shingtaklam1324@gmail.com>
    @jamesa9283 @shingtaklam1324
    jamesa9283 and shingtaklam1324 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    beb7269 View commit details
    Browse the repository at this point in the history

  14. removed docstring on cosh_sq_sub_sinh_sq

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    7287108 View commit details
    Browse the repository at this point in the history

  15. Merge branch 'arsinh' of https://github.com/leanprover-community/mathlib 

     into arsinh
    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    41b05c8 View commit details
    Browse the repository at this point in the history

  16. Moved code into one rw on line 78

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    827ae2c View commit details
    Browse the repository at this point in the history

  17. Update src/analysis/special_functions/arsinh.lean 

    Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @jamesa9283 @kckennylau
    jamesa9283 and kckennylau committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    8167571 View commit details
    Browse the repository at this point in the history

  18. Update src/analysis/special_functions/arsinh.lean 

    add full stop and space

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    d566198 View commit details
    Browse the repository at this point in the history

  19. Update src/analysis/special_functions/arsinh.lean 

    Added full stop

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    5bb4ec4 View commit details
    Browse the repository at this point in the history

  20. Update src/analysis/special_functions/arsinh.lean 

    added full stop

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    a7b0f13 View commit details
    Browse the repository at this point in the history

  21. Update src/analysis/special_functions/trigonometric.lean 

    added spaces and removed semi colon

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    5fb85ac View commit details
    Browse the repository at this point in the history

  22. Update src/analysis/special_functions/trigonometric.lean 

    added full stop and space

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    ffa53ea View commit details
    Browse the repository at this point in the history

  23. Update src/data/complex/exponential.lean 

    added spaces

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    a2078af View commit details
    Browse the repository at this point in the history

  24. Update src/analysis/special_functions/arsinh.lean 

    added space after sqrt

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    3a99cd6 View commit details
    Browse the repository at this point in the history

  25. Update src/analysis/special_functions/arsinh.lean 

    removed new line brace

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
    @jamesa9283 @TwoFX
    jamesa9283 and TwoFX committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    c010972 View commit details
    Browse the repository at this point in the history

  26. Update src/analysis/special_functions/arsinh.lean 

    added spaces around `^`

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @jamesa9283 @kckennylau
    jamesa9283 and kckennylau committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    1f9edf5 View commit details
    Browse the repository at this point in the history

  27. Update src/analysis/special_functions/arsinh.lean 

    rewritten proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @jamesa9283 @kckennylau
    jamesa9283 and kckennylau committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    d15b088 View commit details
    Browse the repository at this point in the history

  28. Update src/data/complex/exponential.lean 

    rewritten proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @jamesa9283 @kckennylau
    jamesa9283 and kckennylau committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    3cf9ff0 View commit details
    Browse the repository at this point in the history

  29. Update src/analysis/special_functions/arsinh.lean 

    simplifies proof

Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @jamesa9283 @kckennylau
    jamesa9283 and kckennylau committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    8851ea6 View commit details
    Browse the repository at this point in the history

  30. added Kenny's code

    @jamesa9283
    jamesa9283 committed Aug 17, 2020
    Configuration menu
    Copy the full SHA
    5dfa6d5 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2020

  1. updated cosh_eq with a Kenny esc proof

    @jamesa9283
    jamesa9283 committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    b75ab5f View commit details
    Browse the repository at this point in the history

  2. added full stops and spaces to docstrings

    @jamesa9283
    jamesa9283 committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    d9f645c View commit details
    Browse the repository at this point in the history

  3. swapped the names of arinh_sinh and sinh_arsinh

    @jamesa9283
    jamesa9283 committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    745acc1 View commit details
    Browse the repository at this point in the history

  4. forgot to swap names

    @jamesa9283
    jamesa9283 committed Aug 18, 2020
    Configuration menu
    Copy the full SHA
    c8ec108 View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2020

  1. Added namespace real and @[pp_nodot]

    @jamesa9283
    jamesa9283 committed Aug 20, 2020
    Configuration menu
    Copy the full SHA
    04ffedd View commit details
    Browse the repository at this point in the history

  2. Update src/analysis/special_functions/arsinh.lean

    @robertylewis
    robertylewis committed Aug 20, 2020
    Configuration menu
    Copy the full SHA
    694e47e View commit details
    Browse the repository at this point in the history