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

feat(analysis): seminorms and local convexity #1926

Closed
wants to merge 16 commits into from
Closed

feat(analysis): seminorms and local convexity #1926

wants to merge 16 commits into from

Commits on Jan 26, 2020

  1. feat(algebra/pointwise): more lemmas about scaling sets 

    - rename `smul_set` to `scale_set` for disambiguation
- define `scale_set_action`, which subsumes `one_smul_set`
- additional lemmas lemmas
    @jlpaca
    jlpaca committed Jan 26, 2020
    Configuration menu
    Copy the full SHA
    3534403 View commit details
    Browse the repository at this point in the history

  2. fix(analysis/convex): refactor proofs for scale_set

    @jlpaca
    jlpaca committed Jan 26, 2020
    Configuration menu
    Copy the full SHA
    d6bacd2 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2020

  1. feat(analysis/seminorm): create file on seminorms/local convexity

    @jlpaca
    jlpaca committed Jan 29, 2020
    Configuration menu
    Copy the full SHA
    93fea30 View commit details
    Browse the repository at this point in the history

  2. feat(analysis/seminorm): remove spurious nonnegativity hypothesis 

    - also add documentation
    @jlpaca
    jlpaca committed Jan 29, 2020
    Configuration menu
    Copy the full SHA
    7d707cb View commit details
    Browse the repository at this point in the history

  3. docs(analysis/seminorm): add reference entry

    @jlpaca
    jlpaca committed Jan 29, 2020
    Configuration menu
    Copy the full SHA
    2a6cec0 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into scale-set-lem
    @jlpaca
    jlpaca committed Jan 29, 2020
    Configuration menu
    Copy the full SHA
    cf6b2af View commit details
    Browse the repository at this point in the history

  5. Merge branch 'scale-set-lem' of https://github.com/leanprover-communi… 

    …ty/mathlib into seminorm-etc
    @jlpaca
    jlpaca committed Jan 29, 2020
    Configuration menu
    Copy the full SHA
    9104eb8 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2020

  1. feat(algebra/pointwise): re-organise file 

    - subsume `pointwise_mul_action`
    @jlpaca
    jlpaca committed Jan 31, 2020
    Configuration menu
    Copy the full SHA
    bd03b89 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2020

  1. fix(algebra/pointwise): resolve conflicts with analysis/convex 

    - also restore name of `smul_set`
    @jlpaca
    jlpaca committed Feb 1, 2020
    Configuration menu
    Copy the full SHA
    32dba01 View commit details
    Browse the repository at this point in the history

  2. feat(algebra/pointwise): remove pointwise_mul_action 

    - subsumed by `smul_set_action` with left-regular action.
    @jlpaca
    jlpaca committed Feb 1, 2020
    Configuration menu
    Copy the full SHA
    51c3355 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into scale-set-lem
    @jlpaca
    jlpaca committed Feb 1, 2020
    Configuration menu
    Copy the full SHA
    d342bc7 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2020

  1. Merge branch 'scale-set-lem' into seminorm-etc

    @jlpaca
    jlpaca committed Feb 2, 2020
    Configuration menu
    Copy the full SHA
    a79f72c View commit details
    Browse the repository at this point in the history

  2. fix(analysis/seminorm): resolve conflicts 

    * resolve updates in `analysis/convex` and `algebra/pointwise`.
    @jlpaca
    jlpaca committed Feb 2, 2020
    Configuration menu
    Copy the full SHA
    16a8098 View commit details
    Browse the repository at this point in the history

Commits on May 23, 2020

  1. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into seminorm-etc
    @jlpaca
    jlpaca committed May 23, 2020
    Configuration menu
    Copy the full SHA
    7465ab0 View commit details
    Browse the repository at this point in the history

  2. fix(analysis/seminorm): fixes for updated mathlib

    @jlpaca
    jlpaca committed May 23, 2020
    Configuration menu
    Copy the full SHA
    9650ec8 View commit details
    Browse the repository at this point in the history

Commits on May 24, 2020

  1. fix(analysis/seminorm): remove spurious simp lemma 

    - also remove some TODO comments
    @jlpaca
    jlpaca committed May 24, 2020
    Configuration menu
    Copy the full SHA
    394f443 View commit details
    Browse the repository at this point in the history