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/function/uniform_integrable): Egorov's theorem #11328

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(measure_theory/function/uniform_integrable): Egorov's theorem #11328

wants to merge 12 commits into from

Commits on Jan 9, 2022

  1. initial commit

    @JasonKYi
    JasonKYi committed Jan 9, 2022
    Configuration menu
    Copy the full SHA
    ae73434 View commit details
    Browse the repository at this point in the history

  2. some typos

    @JasonKYi
    JasonKYi committed Jan 9, 2022
    Configuration menu
    Copy the full SHA
    917e315 View commit details
    Browse the repository at this point in the history

  3. its 2022

    @JasonKYi
    JasonKYi committed Jan 9, 2022
    Configuration menu
    Copy the full SHA
    3f48562 View commit details
    Browse the repository at this point in the history

  4. consistency

    @JasonKYi
    JasonKYi committed Jan 9, 2022
    Configuration menu
    Copy the full SHA
    25971b6 View commit details
    Browse the repository at this point in the history

Commits on Jan 10, 2022

  1. change lt top to ne top

    @JasonKYi
    JasonKYi committed Jan 10, 2022
    Configuration menu
    Copy the full SHA
    20cc5b1 View commit details
    Browse the repository at this point in the history

  2. add a version for finite measures

    @JasonKYi
    JasonKYi committed Jan 10, 2022
    Configuration menu
    Copy the full SHA
    415c919 View commit details
    Browse the repository at this point in the history

  3. add measurability of t

    @JasonKYi
    JasonKYi committed Jan 10, 2022
    Configuration menu
    Copy the full SHA
    1dbf1f3 View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2022

  1. add variables

    @JasonKYi
    JasonKYi committed Jan 13, 2022
    Configuration menu
    Copy the full SHA
    e916c2a View commit details
    Browse the repository at this point in the history

  2. remove [m]

    @JasonKYi
    JasonKYi committed Jan 13, 2022
    Configuration menu
    Copy the full SHA
    93fc601 View commit details
    Browse the repository at this point in the history

  3. Apply suggestions from code review 

    Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
    @JasonKYi @RemyDegenne
    JasonKYi and RemyDegenne committed Jan 13, 2022
    Configuration menu
    Copy the full SHA
    ddf92b9 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'JasonKYi/egorov' of https://github.com/leanprover-commu… 

    …nity/mathlib into JasonKYi/egorov
    @JasonKYi
    JasonKYi committed Jan 13, 2022
    Configuration menu
    Copy the full SHA
    da5c405 View commit details
    Browse the repository at this point in the history

  5. extract lemma

    @JasonKYi
    JasonKYi committed Jan 13, 2022
    Configuration menu
    Copy the full SHA
    35d58ee View commit details
    Browse the repository at this point in the history