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: locally Lipschitz maps #7314

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat: locally Lipschitz maps #7314

wants to merge 16 commits into from

Commits on Sep 21, 2023

  1. Define locally Lipschitz maps and show basic properties. 

    Two sorries related to coercions remain.
    @grunweg
    grunweg committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    e6cd7f9 View commit details
    Browse the repository at this point in the history

  2. Golf more using dot notation.

    @grunweg
    grunweg committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    22c17bd View commit details
    Browse the repository at this point in the history

  3. C¹ functions are locally Lipschitz.

    @grunweg
    grunweg committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    9bbc0f1 View commit details
    Browse the repository at this point in the history

  4. Also show that min, max of locally Lipschitz functions is locally Lip… 

    …schitz.

And some small golfs using dot notation.
    @grunweg
    grunweg committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    5eff2f7 View commit details
    Browse the repository at this point in the history

  5. Fix the build, while generalising to arbitrary fields.

    @grunweg
    grunweg committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    6fbf15f View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2023

  1. Golf a proof in term mode; address doc comment.

    @grunweg
    grunweg committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    af6f9eb View commit details
    Browse the repository at this point in the history

  2. Move LocallyLipschitz.ofLipschitz to LipschitzWith: 

    enables dot notation and golfing some proofs quite a bit more.
    @grunweg
    grunweg committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    0f2012b View commit details
    Browse the repository at this point in the history

  3. Fix line length.

    @grunweg
    grunweg committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    2e47448 View commit details
    Browse the repository at this point in the history

  4. Small simplification. 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @grunweg @eric-wieser
    grunweg and eric-wieser committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    153fd09 View commit details
    Browse the repository at this point in the history

  5. Fix the last sorry with a hammer. And use dot notation more.

    @grunweg
    grunweg committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    3d81e2f View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2023

  1. Review comments (automatic part). 

    Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
    @grunweg @ADedecker
    grunweg and ADedecker committed Sep 24, 2023
    Configuration menu
    Copy the full SHA
    83ab480 View commit details
    Browse the repository at this point in the history

  2. Review comments (manual). 

    And slight tweaks to the doc comments, and a minigolf using dot notation.
    @grunweg
    grunweg committed Sep 24, 2023
    Configuration menu
    Copy the full SHA
    0ce2603 View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2023

  1. Suggested golf of LocallyLipschitz.comp. 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @grunweg @sgouezel
    grunweg and sgouezel committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    f9d2032 View commit details
    Browse the repository at this point in the history

  2. Golf LocallyLipschitz.prod in the same way.

    @grunweg
    grunweg committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    055ddbd View commit details
    Browse the repository at this point in the history

  3. Rename LocallyLipschitz.{mul,pow} to {mul,pow}_end.

    @grunweg
    grunweg committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    66c7ee0 View commit details
    Browse the repository at this point in the history

  4. Same for LipschitzWith.{mul,pow}.

    @grunweg
    grunweg committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    0ab2536 View commit details
    Browse the repository at this point in the history