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

refactor(analysis/convex): simplify proofs, use implicit args and dot notation #1804

Merged
merged 5 commits into from Dec 16, 2019
Merged

refactor(analysis/convex): simplify proofs, use implicit args and dot notation #1804

merged 5 commits into from Dec 16, 2019

Commits on Dec 15, 2019

  1. feat(data/set/intervals): add nonempty_Icc etc, `image_(add/mul)_(l… 

    …eft/right)_Icc`
    @urkud
    urkud committed Dec 15, 2019
    Configuration menu
    Copy the full SHA
    4275707 View commit details
    Browse the repository at this point in the history

  2. refactor(analysis/convex): simplify proofs, use implicit args and dot… 

    … notation

* Use dot notation.
* Swap LHS and RHS of `image_Icc_zero_one_eq_segment`.
* Introduce `finset.center_mass`, prove basic properties.
* Deduce Jensen's inequality from the corresponding property of convex
  sets; rename corresponding lemmas.
    @urkud
    urkud committed Dec 15, 2019
    Configuration menu
    Copy the full SHA
    b342e25 View commit details
    Browse the repository at this point in the history

  3. Fix a typo 

    Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @urkud @sgouezel
    urkud and sgouezel committed Dec 15, 2019
    Configuration menu
    Copy the full SHA
    cecb689 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2019

  1. Update src/analysis/convex.lean

    @urkud
    urkud committed Dec 16, 2019
    Configuration menu
    Copy the full SHA
    8fc631a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into convex-review

    @urkud
    urkud committed Dec 16, 2019
    Configuration menu
    Copy the full SHA
    9a75181 View commit details
    Browse the repository at this point in the history