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): real.log is infinitely smooth away from zero #5116

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat(analysis/special_functions): real.log is infinitely smooth away from zero #5116

wants to merge 21 commits into from

Commits on Nov 25, 2020

  1. chore(order/basic): add strict_mono_??cr_on.dual and dual_right 

    We can use these to avoid `@strict_mono_??cr_on (order_dual α) (order_dual β)`.
    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    944d6fd View commit details
    Browse the repository at this point in the history

  2. chore(order/rel_iso): add a few lemmas 

    * add lemmas `order_iso.apply_eq_iff_eq` etc;
* define `order_iso.symm`.
    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    6606ec5 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'order-iso-lemmas' into order-iso-to-homeomorph

    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    2a62e32 View commit details
    Browse the repository at this point in the history

  4. Snapshot

    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    b9a6ae1 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into order-iso-to-homeomorph

    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    e8bc99e View commit details
    Browse the repository at this point in the history

  6. Log is infinitely smooth

    @urkud
    urkud committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    d033d0d View commit details
    Browse the repository at this point in the history

Commits on Dec 3, 2020

  1. Merge branch 'master' into log-tcd2

    @urkud
    urkud committed Dec 3, 2020
    Configuration menu
    Copy the full SHA
    697bd09 View commit details
    Browse the repository at this point in the history

  2. Fix

    @urkud
    urkud committed Dec 3, 2020
    Configuration menu
    Copy the full SHA
    489d8c4 View commit details
    Browse the repository at this point in the history

  3. snapshot

    @urkud
    urkud committed Dec 3, 2020
    Configuration menu
    Copy the full SHA
    768bb19 View commit details
    Browse the repository at this point in the history

  4. Fix

    @urkud
    urkud committed Dec 3, 2020
    Configuration menu
    Copy the full SHA
    4c7f68d View commit details
    Browse the repository at this point in the history

  5. More lemmas

    @urkud
    urkud committed Dec 3, 2020
    Configuration menu
    Copy the full SHA
    ee5e7f1 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2020

  1. Merge branch 'master' into log-tcd2

    @urkud
    urkud committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    85cb18f View commit details
    Browse the repository at this point in the history

Commits on Dec 5, 2020

  1. Snapshot

    @urkud
    urkud committed Dec 5, 2020
    Configuration menu
    Copy the full SHA
    84967dd View commit details
    Browse the repository at this point in the history

Commits on Dec 6, 2020

  1. Merge branch 'master' into log-tcd2

    @urkud
    urkud committed Dec 6, 2020
    Configuration menu
    Copy the full SHA
    6b16c6e View commit details
    Browse the repository at this point in the history

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

    Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
    @urkud @hrmacbeth
    urkud and hrmacbeth committed Dec 6, 2020
    Configuration menu
    Copy the full SHA
    d8bc43f View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2020

  1. Merge branch 'master' into log-tcd2

    @urkud
    urkud committed Dec 7, 2020
    Configuration menu
    Copy the full SHA
    50e2658 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'log-tcd2' of git://github.com/leanprover-community/math… 

    …lib into log-tcd2
    @urkud
    urkud committed Dec 7, 2020
    Configuration menu
    Copy the full SHA
    792b997 View commit details
    Browse the repository at this point in the history

Commits on Dec 8, 2020

  1. Rewrite the proof

    @urkud
    urkud committed Dec 8, 2020
    Configuration menu
    Copy the full SHA
    e5e3672 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into log-tcd2

    @urkud
    urkud committed Dec 8, 2020
    Configuration menu
    Copy the full SHA
    1684add View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2020

  1. Fix

    @urkud
    urkud committed Dec 9, 2020
    Configuration menu
    Copy the full SHA
    3aa365b View commit details
    Browse the repository at this point in the history

  2. Snapshot

    @urkud
    urkud committed Dec 9, 2020
    Configuration menu
    Copy the full SHA
    969703c View commit details
    Browse the repository at this point in the history