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(measure_theory/integral): Circle integral transform #13885

Closed
wants to merge 40 commits into from
Closed

[Merged by Bors] - feat(measure_theory/integral): Circle integral transform #13885

wants to merge 40 commits into from

Commits on May 2, 2022

  1. add file on circle_integral_transforms

    @CBirkbeck
    CBirkbeck committed May 2, 2022
    Configuration menu
    Copy the full SHA
    e13e103 View commit details
    Browse the repository at this point in the history

  2. some lint fix

    @CBirkbeck
    CBirkbeck committed May 2, 2022
    Configuration menu
    Copy the full SHA
    9e47b61 View commit details
    Browse the repository at this point in the history

  3. lint

    @CBirkbeck
    CBirkbeck committed May 2, 2022
    Configuration menu
    Copy the full SHA
    6099e86 View commit details
    Browse the repository at this point in the history

Commits on May 6, 2022

  1. style fixes

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    063ed36 View commit details
    Browse the repository at this point in the history

  2. typo

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    da2f9b7 View commit details
    Browse the repository at this point in the history

  3. lint fix

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    8d5d7ec View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into circle_integral_tra… 

    …nsform
    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    96a927b View commit details
    Browse the repository at this point in the history

  5. update

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    ec43a35 View commit details
    Browse the repository at this point in the history

  6. Update src/measure_theory/integral/circle_integral.lean 

    Co-authored-by: loefflerd <d.loeffler.01@cantab.net>
    @CBirkbeck @loefflerd
    CBirkbeck and loefflerd committed May 6, 2022
    Configuration menu
    Copy the full SHA
    051bf2e View commit details
    Browse the repository at this point in the history

  7. less spaces

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    c394807 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'circle_integral_transform' of https://github.com/leanpr… 

    …over-community/mathlib into circle_integral_transform
    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    14cf250 View commit details
    Browse the repository at this point in the history

  9. refine to exact

    @CBirkbeck
    CBirkbeck committed May 6, 2022
    Configuration menu
    Copy the full SHA
    1043015 View commit details
    Browse the repository at this point in the history

  10. golf

    @loefflerd
    loefflerd committed May 6, 2022
    Configuration menu
    Copy the full SHA
    c771fe4 View commit details
    Browse the repository at this point in the history

  11. one more tiny fix

    @loefflerd
    loefflerd committed May 6, 2022
    Configuration menu
    Copy the full SHA
    0af9042 View commit details
    Browse the repository at this point in the history

  12. final bit of golf

    @loefflerd
    loefflerd committed May 6, 2022
    Configuration menu
    Copy the full SHA
    97b1fdd View commit details
    Browse the repository at this point in the history

Commits on May 9, 2022

  1. remove some lemmas

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

  2. remove some lemmas

    @CBirkbeck
    CBirkbeck committed May 9, 2022
    Configuration menu
    Copy the full SHA
    860c3a2 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2022

  1. Some golf

    @loefflerd
    loefflerd committed May 10, 2022
    Configuration menu
    Copy the full SHA
    403f867 View commit details
    Browse the repository at this point in the history

  2. more inteval fixes

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

  3. merge my changes with rev changes

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

Commits on May 26, 2022

  1. some rev changes

    @CBirkbeck
    CBirkbeck committed May 26, 2022
    Configuration menu
    Copy the full SHA
    e82c7f9 View commit details
    Browse the repository at this point in the history

  2. circle_int updates

    @CBirkbeck
    CBirkbeck committed May 26, 2022
    Configuration menu
    Copy the full SHA
    b033f95 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2022

  1. lint

    @CBirkbeck
    CBirkbeck committed May 30, 2022
    Configuration menu
    Copy the full SHA
    a2d934d View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2022

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

    …nsform
    @CBirkbeck
    CBirkbeck committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    0aafc10 View commit details
    Browse the repository at this point in the history

  2. rev changes

    @CBirkbeck
    CBirkbeck committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    19d397a View commit details
    Browse the repository at this point in the history

  3. typo

    @CBirkbeck
    CBirkbeck committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    90598ba View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2022

  1. cit_deriv periodic

    @CBirkbeck
    CBirkbeck committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    db66d01 View commit details
    Browse the repository at this point in the history

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

    …nsform
    @CBirkbeck
    CBirkbeck committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    cbfc747 View commit details
    Browse the repository at this point in the history

  3. merge fix

    @CBirkbeck
    CBirkbeck committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    f0350e5 View commit details
    Browse the repository at this point in the history

  4. lint fix

    @CBirkbeck
    CBirkbeck committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    964e23a View commit details
    Browse the repository at this point in the history

  5. lint fix2

    @CBirkbeck
    CBirkbeck committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    579c985 View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2022

  1. rev fixes

    @CBirkbeck
    CBirkbeck committed Jun 24, 2022
    Configuration menu
    Copy the full SHA
    2187ae7 View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2022

  1. name change

    @CBirkbeck
    CBirkbeck committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    81b660a View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2022

  1. Update src/measure_theory/integral/circle_integral.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @CBirkbeck @sgouezel
    CBirkbeck and sgouezel committed Jul 5, 2022
    Configuration menu
    Copy the full SHA
    5841923 View commit details
    Browse the repository at this point in the history

  2. name fix

    @CBirkbeck
    CBirkbeck committed Jul 5, 2022
    Configuration menu
    Copy the full SHA
    70cd920 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2022

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

    …nsform
    @CBirkbeck
    CBirkbeck committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    e4356b6 View commit details
    Browse the repository at this point in the history

  2. orange hell

    @CBirkbeck
    CBirkbeck committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    86c4e6f View commit details
    Browse the repository at this point in the history

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

    …nsform
    @CBirkbeck
    CBirkbeck committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    eb104c5 View commit details
    Browse the repository at this point in the history

  4. orange hell2

    @CBirkbeck
    CBirkbeck committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    0ab5068 View commit details
    Browse the repository at this point in the history

  5. fix merge issue

    @CBirkbeck
    CBirkbeck committed Jul 6, 2022
    Configuration menu
    Copy the full SHA
    a15550b View commit details
    Browse the repository at this point in the history