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/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

Closed
wants to merge 41 commits into from
Closed

[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

wants to merge 41 commits into from

Commits on Jul 6, 2021

  1. extend integral comp lemmas

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    be00f14 View commit details
    Browse the repository at this point in the history

  2. add space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    5495f8e View commit details
    Browse the repository at this point in the history

  3. undo accidental deletion of integral_apply

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    c354445 View commit details
    Browse the repository at this point in the history

  4. fix

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    81dd754 View commit details
    Browse the repository at this point in the history

  5. Update docstring 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @RemyDegenne @eric-wieser
    RemyDegenne and eric-wieser committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    fd532ea View commit details
    Browse the repository at this point in the history

  6. use nondiscrete_normed_field

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    603a922 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'integral_comp' of github.com:leanprover-community/mathl… 

    …ib into integral_comp
    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    9aca324 View commit details
    Browse the repository at this point in the history

  8. use semi_normed_space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    30dddea View commit details
    Browse the repository at this point in the history

  9. use semi_normed_space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    e8f80d2 View commit details
    Browse the repository at this point in the history

  10. Revert "use semi_normed_space" 

    This reverts commit e8f80d2.
    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    897f5b7 View commit details
    Browse the repository at this point in the history

  11. add one semi_

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    67e010f View commit details
    Browse the repository at this point in the history

  12. use more semi_normed_space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    c6f7218 View commit details
    Browse the repository at this point in the history

  13. use semi_normed_group

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    3abe826 View commit details
    Browse the repository at this point in the history

  14. distinguish normed and semi_normed in lp_space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    5cefb13 View commit details
    Browse the repository at this point in the history

  15. prove completeness of Lp with only semi_

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    af62add View commit details
    Browse the repository at this point in the history

  16. prove completeness of Lp with only semi_

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    4756a3a View commit details
    Browse the repository at this point in the history

  17. add many semi_ and pseudo_ in bounded.lean

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    5bce86a View commit details
    Browse the repository at this point in the history

  18. add semi_ to lp_space lemmas about bounded

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    da9fc10 View commit details
    Browse the repository at this point in the history

  19. add some semi_ in compact.lean

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    4d16fed View commit details
    Browse the repository at this point in the history

  20. more semi_ in lp_space

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    e6a45f5 View commit details
    Browse the repository at this point in the history

  21. fix

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    b66ca78 View commit details
    Browse the repository at this point in the history

  22. fix lint

    @RemyDegenne
    RemyDegenne committed Jul 6, 2021
    Configuration menu
    Copy the full SHA
    5300fa3 View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2021

  1. Merge branch 'integral_comp' of https://github.com/leanprover-communi… 

    …ty/mathlib into integral_comp
    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    0ef8151 View commit details
    Browse the repository at this point in the history

  2. undo indicator_function

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    9acee35 View commit details
    Browse the repository at this point in the history

  3. undo bochner_integration

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    1920f24 View commit details
    Browse the repository at this point in the history

  4. undo borel_space

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    619507e View commit details
    Browse the repository at this point in the history

  5. undo l1_space

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    7dd7bf6 View commit details
    Browse the repository at this point in the history

  6. undo set_integral

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    073c244 View commit details
    Browse the repository at this point in the history

  7. undo simple_func_dense

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    46f2a02 View commit details
    Browse the repository at this point in the history

  8. undo bounded and compact

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    9e40657 View commit details
    Browse the repository at this point in the history

  9. undo gromov_hausdorff

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    6722134 View commit details
    Browse the repository at this point in the history

  10. fake commit

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    762c3cd View commit details
    Browse the repository at this point in the history

  11. fake commit

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    a01130f View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/master' into integral_comp

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    f31481c View commit details
    Browse the repository at this point in the history

  13. remove semi_ in lp_space

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    d76e2c3 View commit details
    Browse the repository at this point in the history

  14. remove primes in lp_space

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    533290e View commit details
    Browse the repository at this point in the history

  15. more undo in lp_space

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    2185b53 View commit details
    Browse the repository at this point in the history

  16. undo

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    5103d1b View commit details
    Browse the repository at this point in the history

  17. undo bounded

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    bb533c9 View commit details
    Browse the repository at this point in the history

  18. add references in docstring

    @RemyDegenne
    RemyDegenne committed Jul 7, 2021
    Configuration menu
    Copy the full SHA
    56372a4 View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2021

  1. Update src/measure_theory/lp_space.lean 

    Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
    @RemyDegenne @hrmacbeth
    RemyDegenne and hrmacbeth committed Jul 11, 2021
    Configuration menu
    Copy the full SHA
    d418652 View commit details
    Browse the repository at this point in the history