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/convex): Carathéodory's convexity theorem #2960

Closed
wants to merge 68 commits into from
Closed

[Merged by Bors] - feat(analysis/convex): Carathéodory's convexity theorem #2960

wants to merge 68 commits into from

Commits on Jun 4, 2020

  1. feat(analysis/convex): preparatory statement for caratheodory

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    91ead87 View commit details
    Browse the repository at this point in the history

  2. Simplify the proof

    @urkud
    urkud committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    5cd5864 View commit details
    Browse the repository at this point in the history

  3. all the boring bits

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    f957086 View commit details
    Browse the repository at this point in the history

  4. some more work

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    cdf130d View commit details
    Browse the repository at this point in the history

  5. more

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    dff708a View commit details
    Browse the repository at this point in the history

  6. naming

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    a7857e9 View commit details
    Browse the repository at this point in the history

  7. more

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    d568922 View commit details
    Browse the repository at this point in the history

  8. minor

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    884d4e2 View commit details
    Browse the repository at this point in the history

  9. fix naming

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    c2c3836 View commit details
    Browse the repository at this point in the history

  10. minor

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    4d27028 View commit details
    Browse the repository at this point in the history

  11. various progress

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    bfe26c6 View commit details
    Browse the repository at this point in the history

  12. mostly done with linear algebra API now

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    a377b12 View commit details
    Browse the repository at this point in the history

  13. comment

    @semorrison
    semorrison committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    9775a61 View commit details
    Browse the repository at this point in the history

  14. Fill in some easy sorrys

    @jcommelin
    jcommelin committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    e04ee78 View commit details
    Browse the repository at this point in the history

  15. Remove another sorry

    @jcommelin
    jcommelin committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    9b4758d View commit details
    Browse the repository at this point in the history

  16. unsorry convex_coefficients

    @jcommelin
    jcommelin committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    f1492e7 View commit details
    Browse the repository at this point in the history

  17. Remove more sorrys

    @jcommelin
    jcommelin committed Jun 4, 2020
    Configuration menu
    Copy the full SHA
    d81dec8 View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2020

  1. almost there

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    51cb60f View commit details
    Browse the repository at this point in the history

  2. some more

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    426108f View commit details
    Browse the repository at this point in the history

  3. Removing sorrys

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    7e3d70d View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into caratheodory2

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    8acfdaf View commit details
    Browse the repository at this point in the history

  5. copyright header

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    3382c56 View commit details
    Browse the repository at this point in the history

  6. minor

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    6cb0797 View commit details
    Browse the repository at this point in the history

  7. merge

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    7405412 View commit details
    Browse the repository at this point in the history

  8. minor

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    e8d86ae View commit details
    Browse the repository at this point in the history

  9. so close

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    b7f4288 View commit details
    Browse the repository at this point in the history

  10. Remove more sorrys

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    007251d View commit details
    Browse the repository at this point in the history

  11. Merge branch 'caratheodory2' of github.com:leanprover-community/mathl… 

    …ib into caratheodory2
    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    513fff7 View commit details
    Browse the repository at this point in the history

  12. Remove another sorry

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    4faf765 View commit details
    Browse the repository at this point in the history

  13. minor

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    11bdf99 View commit details
    Browse the repository at this point in the history

  14. Kill another sorry

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    079e0a6 View commit details
    Browse the repository at this point in the history

  15. merge

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    9b74ffd View commit details
    Browse the repository at this point in the history

  16. Merge branch 'caratheodory2' of github.com:leanprover-community/mathl… 

    …ib into caratheodory2
    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    edb6fef View commit details
    Browse the repository at this point in the history

  17. Sorry free

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    f94162f View commit details
    Browse the repository at this point in the history

  18. Merge branch 'caratheodory2' of github.com:leanprover-community/mathl… 

    …ib into caratheodory2
    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    6026985 View commit details
    Browse the repository at this point in the history

  19. explicit formulation

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    b5a9ace View commit details
    Browse the repository at this point in the history

  20. moving lemmas to their homes

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    38135f9 View commit details
    Browse the repository at this point in the history

  21. tidying up

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    ea782f1 View commit details
    Browse the repository at this point in the history

  22. cleaning up

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    609a7b0 View commit details
    Browse the repository at this point in the history

  23. nearly final cleanup

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    3f0584d View commit details
    Browse the repository at this point in the history

  24. cleaning up comments

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    86a0d1d View commit details
    Browse the repository at this point in the history

  25. Merge remote-tracking branch 'origin/master' into caratheodory2

    @semorrison
    semorrison committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    4ac14f4 View commit details
    Browse the repository at this point in the history

  26. Add module docstring, compress some proofs

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    e906b22 View commit details
    Browse the repository at this point in the history

  27. Merge branch 'caratheodory2' of github.com:leanprover-community/mathl… 

    …ib into caratheodory2
    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    0afd9b1 View commit details
    Browse the repository at this point in the history

  28. Linting

    @jcommelin
    jcommelin committed Jun 5, 2020
    Configuration menu
    Copy the full SHA
    983d253 View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2020

  1. Further cleanups

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    0025699 View commit details
    Browse the repository at this point in the history

  2. More cleanup

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    720e84d View commit details
    Browse the repository at this point in the history

  3. Move things

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    b29f55f View commit details
    Browse the repository at this point in the history

  4. Fix double namespace

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    f351d3f View commit details
    Browse the repository at this point in the history

  5. Linting

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    8e8fd23 View commit details
    Browse the repository at this point in the history

  6. Fix build, hopefully

    @jcommelin
    jcommelin committed Jun 6, 2020
    Configuration menu
    Copy the full SHA
    43399cd View commit details
    Browse the repository at this point in the history

Commits on Jun 7, 2020

  1. add some comments

    @semorrison
    semorrison committed Jun 7, 2020
    Configuration menu
    Copy the full SHA
    0965c01 View commit details
    Browse the repository at this point in the history

  2. move exists_pos_of_sum_zero_of_exists_nonzero

    @semorrison
    semorrison committed Jun 7, 2020
    Configuration menu
    Copy the full SHA
    7b390b7 View commit details
    Browse the repository at this point in the history

  3. remove unnecessary comment

    @semorrison
    semorrison committed Jun 7, 2020
    Configuration menu
    Copy the full SHA
    014aefe View commit details
    Browse the repository at this point in the history

  4. minor renaming

    @semorrison
    semorrison committed Jun 7, 2020
    Configuration menu
    Copy the full SHA
    89ac810 View commit details
    Browse the repository at this point in the history

  5. the variation patrick wants

    @semorrison
    semorrison committed Jun 7, 2020
    Configuration menu
    Copy the full SHA
    a0164e9 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2020

  1. remove a sorry

    @semorrison
    semorrison committed Jun 8, 2020
    Configuration menu
    Copy the full SHA
    e90ffe2 View commit details
    Browse the repository at this point in the history

  2. remove the other sorry

    @semorrison
    semorrison committed Jun 8, 2020
    Configuration menu
    Copy the full SHA
    6820b60 View commit details
    Browse the repository at this point in the history

  3. rename

    @semorrison
    semorrison committed Jun 8, 2020
    Configuration menu
    Copy the full SHA
    990a37c View commit details
    Browse the repository at this point in the history

Commits on Jun 9, 2020

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

    @semorrison
    semorrison committed Jun 9, 2020
    Configuration menu
    Copy the full SHA
    b72e86f View commit details
    Browse the repository at this point in the history

  2. fix typeclasses?

    @semorrison
    semorrison committed Jun 9, 2020
    Configuration menu
    Copy the full SHA
    f4be05c View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2020

  1. Merge branch 'community-master' into caratheodory2

    @bryangingechen
    bryangingechen committed Jun 10, 2020
    Configuration menu
    Copy the full SHA
    7e6b925 View commit details
    Browse the repository at this point in the history

  2. fix build

    @bryangingechen
    bryangingechen committed Jun 10, 2020
    Configuration menu
    Copy the full SHA
    7165813 View commit details
    Browse the repository at this point in the history

Commits on Jun 11, 2020

  1. merge

    @semorrison
    semorrison committed Jun 11, 2020
    Configuration menu
    Copy the full SHA
    4527b22 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2020

  1. Merge branch 'master' into caratheodory2

    @bryangingechen
    bryangingechen committed Jun 13, 2020
    Configuration menu
    Copy the full SHA
    d8a2975 View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2020

  1. Update src/analysis/convex/caratheodory.lean

    @semorrison
    semorrison committed Jun 15, 2020
    Configuration menu
    Copy the full SHA
    46033e3 View commit details
    Browse the repository at this point in the history

  2. Update src/analysis/convex/caratheodory.lean

    @bryangingechen
    bryangingechen committed Jun 15, 2020
    Configuration menu
    Copy the full SHA
    4335e3e View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2020

  1. Update src/analysis/convex/caratheodory.lean

    @bryangingechen
    bryangingechen committed Jun 16, 2020
    Configuration menu
    Copy the full SHA
    3f1f885 View commit details
    Browse the repository at this point in the history