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: define logarithmic derivatives #12804

Closed
wants to merge 50 commits into from
Closed

[Merged by Bors] - feat: define logarithmic derivatives #12804

wants to merge 50 commits into from

Commits on May 10, 2024

  1. WIP logarithmic derivatives

    @CBirkbeck
    CBirkbeck committed May 10, 2024
    Configuration menu
    Copy the full SHA
    c32039f View commit details
    Browse the repository at this point in the history

Commits on May 24, 2024

  1. save

    @CBirkbeck
    CBirkbeck committed May 24, 2024
    Configuration menu
    Copy the full SHA
    4842302 View commit details
    Browse the repository at this point in the history

Commits on May 27, 2024

  1. golf and move diff.prod lemma

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    aefad56 View commit details
    Browse the repository at this point in the history

  2. some doc strings

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    11625c0 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into logarithmic_derivat… 

    …ives
    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    c3c87e6 View commit details
    Browse the repository at this point in the history

  4. lintr fix

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    b3bee69 View commit details
    Browse the repository at this point in the history

  5. mathlib file

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    6553f9a View commit details
    Browse the repository at this point in the history

  6. add differenitableAt.product

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    11caae8 View commit details
    Browse the repository at this point in the history

  7. fix mathlib

    @CBirkbeck
    CBirkbeck committed May 27, 2024
    Configuration menu
    Copy the full SHA
    1e0f0b9 View commit details
    Browse the repository at this point in the history

Commits on May 28, 2024

  1. rev update

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    c4e9ec1 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into differentiableAt_pr… 

    …oduct
    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    0dd6291 View commit details
    Browse the repository at this point in the history

  3. fix error

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    92424f0 View commit details
    Browse the repository at this point in the history

  4. add diffOn version

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    ce25b56 View commit details
    Browse the repository at this point in the history

  5. deviv version

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    5e41144 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Analysis/Calculus/Deriv/Mul.lean 

    Co-authored-by: David Loeffler <[email protected]>
    @CBirkbeck @loefflerd
    CBirkbeck and loefflerd authored May 28, 2024
    Configuration menu
    Copy the full SHA
    f0daf6b View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Analysis/Calculus/Deriv/Mul.lean 

    Co-authored-by: David Loeffler <[email protected]>
    @CBirkbeck @loefflerd
    CBirkbeck and loefflerd authored May 28, 2024
    Configuration menu
    Copy the full SHA
    c3829f5 View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Analysis/Calculus/Deriv/Mul.lean 

    Co-authored-by: David Loeffler <[email protected]>
    @CBirkbeck @loefflerd
    CBirkbeck and loefflerd authored May 28, 2024
    Configuration menu
    Copy the full SHA
    71d6720 View commit details
    Browse the repository at this point in the history

  9. remove bigops

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    e10fa19 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'differentiableAt_product' of https://github.com/leanpro… 

    …ver-community/mathlib4 into differentiableAt_product
    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    01c9fec View commit details
    Browse the repository at this point in the history

  11. fix

    @CBirkbeck
    CBirkbeck committed May 28, 2024
    Configuration menu
    Copy the full SHA
    2014a5e View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. forgotten within version

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    f597de9 View commit details
    Browse the repository at this point in the history

  2. remove bad lemma

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    9d37c03 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/differentiableAt_product' into l… 

    …ogarithmic_derivatives
    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    cbc9d98 View commit details
    Browse the repository at this point in the history

  4. re add the lost file!

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    7698169 View commit details
    Browse the repository at this point in the history

  5. fix

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    b52c9d9 View commit details
    Browse the repository at this point in the history

  6. lint fix

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    b63f294 View commit details
    Browse the repository at this point in the history

  7. some examples

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    a636c77 View commit details
    Browse the repository at this point in the history

  8. tiny

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    a00c3fb View commit details
    Browse the repository at this point in the history

  9. slight generalisation

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    ddf2c4e View commit details
    Browse the repository at this point in the history

  10. clog lemma

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    5fdd30d View commit details
    Browse the repository at this point in the history

  11. doc string

    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    ea5f80f View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/master' into logarithmic_derivat… 

    …ives
    @CBirkbeck
    CBirkbeck committed May 29, 2024
    Configuration menu
    Copy the full SHA
    c4e1cae View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2024

  1. rev fixes

    @CBirkbeck
    CBirkbeck committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    b8b965d View commit details
    Browse the repository at this point in the history

  2. save

    @CBirkbeck
    CBirkbeck committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    4dbd00a View commit details
    Browse the repository at this point in the history

  3. fix lintr

    @CBirkbeck
    CBirkbeck committed Jun 16, 2024
    Configuration menu
    Copy the full SHA
    e2eee81 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2024

  1. rev updates

    @CBirkbeck
    CBirkbeck committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    f7969a2 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into logarithmic_derivat… 

    …ives
    @CBirkbeck
    CBirkbeck committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    6f1c533 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/NormedSpace/LogarithmicDerivatives.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @CBirkbeck @github-actions
    CBirkbeck and github-actions[bot] authored Jul 16, 2024
    Configuration menu
    Copy the full SHA
    50db781 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. split files

    @CBirkbeck
    CBirkbeck committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    152faee View commit details
    Browse the repository at this point in the history

  2. fix name

    @CBirkbeck
    CBirkbeck committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    2e99a0f View commit details
    Browse the repository at this point in the history

  3. fix

    @CBirkbeck
    CBirkbeck committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    4be543b View commit details
    Browse the repository at this point in the history

  4. fix 2

    @CBirkbeck
    CBirkbeck committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    c7ad95a View commit details
    Browse the repository at this point in the history

  5. name update

    @CBirkbeck
    CBirkbeck committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    f8b9d8c View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2024

  1. Merge branch 'master' into logarithmic_derivatives

    @urkud
    urkud committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    0eea8f0 View commit details
    Browse the repository at this point in the history

  2. Golf, drop unneeded assumptions

    @urkud
    urkud committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    c08855a View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into logarithmic_derivatives

    @urkud
    urkud committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    8d0166b View commit details
    Browse the repository at this point in the history

  4. Fix

    @urkud
    urkud committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    1fd8ffc View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. rev updates

    @CBirkbeck
    CBirkbeck committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    9eb6182 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into logarithmic_derivatives

    @urkud
    urkud authored Jul 29, 2024
    Configuration menu
    Copy the full SHA
    993a85a View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

    @urkud
    urkud authored Jul 29, 2024
    Configuration menu
    Copy the full SHA
    3d67567 View commit details
    Browse the repository at this point in the history