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

feat(analysis/transcendental): e is transcendental #15954

Closed
wants to merge 97 commits into from
Closed

feat(analysis/transcendental): e is transcendental #15954

wants to merge 97 commits into from

Commits on Aug 5, 2022

  1. transcendental_things

    @jjaassoonn @Ruben-VandeVelde
    jjaassoonn authored and Ruben-VandeVelde committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    ee3654c View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2022

  1. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 6, 2022
    Configuration menu
    Copy the full SHA
    738328b View commit details
    Browse the repository at this point in the history

  2. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 6, 2022
    Configuration menu
    Copy the full SHA
    d96a007 View commit details
    Browse the repository at this point in the history

  3. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 6, 2022
    Configuration menu
    Copy the full SHA
    862b8b1 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2022

  1. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 7, 2022
    Configuration menu
    Copy the full SHA
    060adef View commit details
    Browse the repository at this point in the history

  2. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 7, 2022
    Configuration menu
    Copy the full SHA
    b28e267 View commit details
    Browse the repository at this point in the history

  3. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 7, 2022
    Configuration menu
    Copy the full SHA
    915b447 View commit details
    Browse the repository at this point in the history

  4. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 7, 2022
    Configuration menu
    Copy the full SHA
    ce92f28 View commit details
    Browse the repository at this point in the history

  5. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 7, 2022
    Configuration menu
    Copy the full SHA
    3d4835a View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2022

  1. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    67922a2 View commit details
    Browse the repository at this point in the history

  2. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    0caf9ad View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2022

  1. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    c59a814 View commit details
    Browse the repository at this point in the history

  2. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    dfe2728 View commit details
    Browse the repository at this point in the history

  3. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    661dd40 View commit details
    Browse the repository at this point in the history

  4. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    2b6f97c View commit details
    Browse the repository at this point in the history

  5. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    18bf971 View commit details
    Browse the repository at this point in the history

  6. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    5b4962f View commit details
    Browse the repository at this point in the history

  7. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    8c35ca3 View commit details
    Browse the repository at this point in the history

  8. fixup! transcendental_things

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    2867e5f View commit details
    Browse the repository at this point in the history

  9. Gather deriv lemmas

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    4788025 View commit details
    Browse the repository at this point in the history

  10. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    389828a View commit details
    Browse the repository at this point in the history

  11. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 9, 2022
    Configuration menu
    Copy the full SHA
    3c3d4cc View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2022

  1. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 10, 2022
    Configuration menu
    Copy the full SHA
    74c1c4d View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2022

  1. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    c45b08d View commit details
    Browse the repository at this point in the history

  2. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    6990782 View commit details
    Browse the repository at this point in the history

  3. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    e213d3b View commit details
    Browse the repository at this point in the history

  4. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    1d6faaf View commit details
    Browse the repository at this point in the history

  5. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    b515d69 View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2022

  1. Remove deriv_n lemmas.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    dd58637 View commit details
    Browse the repository at this point in the history

  2. chore(data/polynomial/derivative): merge iterated_deriv.lean into der… 

    …ivative.lean

iterated_deriv.lean was not used anywhere, and derivative.lean already had independent variants of several of the lemmas there, without the `iterated_deriv` indirecion. It seems better to consolidate these results.
    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    00377e1 View commit details
    Browse the repository at this point in the history

  3. feat(data/polynomial/derivative): add more lemmas 

    Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
    @Ruben-VandeVelde @jjaassoonn
    Ruben-VandeVelde and jjaassoonn committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    281a625 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'polynomial-deriv-more' into some_transcendental_things-2

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    5233857 View commit details
    Browse the repository at this point in the history

  5. fix

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    b0a96ae View commit details
    Browse the repository at this point in the history

  6. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    12f6103 View commit details
    Browse the repository at this point in the history

  7. fixup! feat(data/polynomial/derivative): add more lemmas

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    ea00d84 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'polynomial-deriv-more' into some_transcendental_things-2

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    38d9e4a View commit details
    Browse the repository at this point in the history

  9. fixes

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    0b7100d View commit details
    Browse the repository at this point in the history

  10. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    1c45134 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2022

  1. pow_transcendental

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 13, 2022
    Configuration menu
    Copy the full SHA
    f9aa2eb View commit details
    Browse the repository at this point in the history

  2. Simplify pow_transcendental.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 13, 2022
    Configuration menu
    Copy the full SHA
    47a1128 View commit details
    Browse the repository at this point in the history

  3. generalize

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 13, 2022
    Configuration menu
    Copy the full SHA
    4f3aaa8 View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2022

  1. move

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    0875dc2 View commit details
    Browse the repository at this point in the history

  2. tidy

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    51638dc View commit details
    Browse the repository at this point in the history

  3. tidy

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    d494f35 View commit details
    Browse the repository at this point in the history

  4. simplify

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    6ea1fda View commit details
    Browse the repository at this point in the history

  5. Simplify deg_f_p

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    0afdd52 View commit details
    Browse the repository at this point in the history

  6. Simplify.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    35210b2 View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2022

  1. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    dcba37d View commit details
    Browse the repository at this point in the history

  2. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5f27a7d View commit details
    Browse the repository at this point in the history

  3. Golf transform_eq

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    9fe8505 View commit details
    Browse the repository at this point in the history

  4. fact_grows_fast'

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    46725c0 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2022

  1. Merge remote-tracking branch 'origin/master' into some_transcendental… 

    …_things-2
    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    a935e07 View commit details
    Browse the repository at this point in the history

  2. braces

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    3d282d5 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2022

  1. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    e060bec View commit details
    Browse the repository at this point in the history

  2. golf

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    55dceaf View commit details
    Browse the repository at this point in the history

  3. fix

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    b89853d View commit details
    Browse the repository at this point in the history

  4. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    233f603 View commit details
    Browse the repository at this point in the history

  5. move

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    6f17fe6 View commit details
    Browse the repository at this point in the history

  6. remove

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    5421c45 View commit details
    Browse the repository at this point in the history

  7. tidy

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    e0fccc7 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2022

  1. tidy

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    14ec768 View commit details
    Browse the repository at this point in the history

  2. Drop deriv_n

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    dcb7ecc View commit details
    Browse the repository at this point in the history

  3. Start removing f_eval_on_ℝ

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    df49f59 View commit details
    Browse the repository at this point in the history

  4. feat(data/polynomial/derivative): add more lemmas 

    Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
    @Ruben-VandeVelde @jjaassoonn
    Ruben-VandeVelde and jjaassoonn committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    607926d View commit details
    Browse the repository at this point in the history

  5. Merge branch 'polynomial-deriv-more' into some_transcendental_things-2

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 18, 2022
    Configuration menu
    Copy the full SHA
    931dfa7 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2022

  1. Remove f_eval_on_ℝ

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 19, 2022
    Configuration menu
    Copy the full SHA
    bf725e0 View commit details
    Browse the repository at this point in the history

  2. Drop integral_le_max_times_length

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 19, 2022
    Configuration menu
    Copy the full SHA
    9c00418 View commit details
    Browse the repository at this point in the history

  3. Drop p_le.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 19, 2022
    Configuration menu
    Copy the full SHA
    09e9cd5 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2022

  1. Drop f_p_n_succ

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    557f85f View commit details
    Browse the repository at this point in the history

  2. work

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    cfabcd9 View commit details
    Browse the repository at this point in the history

  3. work

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    52c67e2 View commit details
    Browse the repository at this point in the history

  4. work

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    f246439 View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2022

  1. wip

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    9dc839c View commit details
    Browse the repository at this point in the history

  2. Use nat.desc_factorial.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    9569813 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'polynomial-deriv-more' into some_transcendental_things-2

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    9573e56 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2022

  1. update

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 25, 2022
    Configuration menu
    Copy the full SHA
    06ab09b View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2022

  1. Drop deriv_exp_t_x'

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    2a49d9b View commit details
    Browse the repository at this point in the history

  2. Golf.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    441be4f View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2022

  1. Golf.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 28, 2022
    Configuration menu
    Copy the full SHA
    a707c17 View commit details
    Browse the repository at this point in the history

  2. Move more lemmas about f_bar.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 28, 2022
    Configuration menu
    Copy the full SHA
    161e61e View commit details
    Browse the repository at this point in the history

  3. Golf.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 28, 2022
    Configuration menu
    Copy the full SHA
    2590748 View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2022

  1. Merge branch 'master' into some_transcendental_things-2

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    287b10c View commit details
    Browse the repository at this point in the history

  2. Fix

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    371ccdf View commit details
    Browse the repository at this point in the history

  3. Golf.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    b8667a1 View commit details
    Browse the repository at this point in the history

  4. Golf.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    fa5add2 View commit details
    Browse the repository at this point in the history

  5. import

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    3018771 View commit details
    Browse the repository at this point in the history

  6. open polynomial

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    847d7b4 View commit details
    Browse the repository at this point in the history

  7. Better proof

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    9f843eb View commit details
    Browse the repository at this point in the history

  8. Whitespace.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    5ac77d5 View commit details
    Browse the repository at this point in the history

  9. Whitespace.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    b963bbf View commit details
    Browse the repository at this point in the history

  10. Tidy.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    8a8e171 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2022

  1. lint

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    ea13260 View commit details
    Browse the repository at this point in the history

  2. Tidy.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    15632e1 View commit details
    Browse the repository at this point in the history

  3. Tidy.

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    0c0c19e View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2022

  1. f_bar_ineq

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 5, 2022
    Configuration menu
    Copy the full SHA
    3988ddb View commit details
    Browse the repository at this point in the history

  2. f_bar_ineq

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 5, 2022
    Configuration menu
    Copy the full SHA
    64193b6 View commit details
    Browse the repository at this point in the history

  3. reorganize

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Sep 5, 2022
    Configuration menu
    Copy the full SHA
    449126f View commit details
    Browse the repository at this point in the history