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/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) #7918

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(measure_theory/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) #7918

wants to merge 17 commits into from

Commits on Jun 12, 2021

  1. simple func facts

    @RemyDegenne
    RemyDegenne committed Jun 12, 2021
    Configuration menu
    Copy the full SHA
    8f6c5e1 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2021

  1. simplify and organize

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    bbb31a0 View commit details
    Browse the repository at this point in the history

  2. remove lemma

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

  3. fix name

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    5696306 View commit details
    Browse the repository at this point in the history

  4. names

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    e371d4c View commit details
    Browse the repository at this point in the history

  5. move everything to bochner_integration

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    cc70820 View commit details
    Browse the repository at this point in the history

  6. move lemmas to lp_space

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    14f0d2b View commit details
    Browse the repository at this point in the history

  7. remove unused lemma

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    a0335cd View commit details
    Browse the repository at this point in the history

  8. docstring

    @RemyDegenne
    RemyDegenne committed Jun 13, 2021
    Configuration menu
    Copy the full SHA
    46cea43 View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2021

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

    @RemyDegenne
    RemyDegenne committed Jun 14, 2021
    Configuration menu
    Copy the full SHA
    851a580 View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2021

  1. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    3ab179f View commit details
    Browse the repository at this point in the history

  2. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    c9d3289 View commit details
    Browse the repository at this point in the history

  3. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    f540df7 View commit details
    Browse the repository at this point in the history

  4. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    98594ad View commit details
    Browse the repository at this point in the history

  5. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    ad1bd5f View commit details
    Browse the repository at this point in the history

  6. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    6657e55 View commit details
    Browse the repository at this point in the history

  7. Update src/measure_theory/bochner_integration.lean 

    Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
    @RemyDegenne @benjamindavidson
    RemyDegenne and benjamindavidson committed Jun 15, 2021
    Configuration menu
    Copy the full SHA
    bb7b475 View commit details
    Browse the repository at this point in the history