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): Equivalent condition for uniformly integrable in the probability sense #12955

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense #12955

wants to merge 17 commits into from

Commits on Mar 24, 2022

  1. initial commit, one sorry left

    @JasonKYi
    JasonKYi committed Mar 24, 2022
    Configuration menu
    Copy the full SHA
    4cfc0ae View commit details
    Browse the repository at this point in the history

Commits on Mar 25, 2022

  1. extract lemma

    @JasonKYi
    JasonKYi committed Mar 25, 2022
    Configuration menu
    Copy the full SHA
    b552c8d View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2022

  1. move lemmas

    @JasonKYi
    JasonKYi committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    c88617e View commit details
    Browse the repository at this point in the history

  2. fix error

    @JasonKYi
    JasonKYi committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    fc01a0b View commit details
    Browse the repository at this point in the history

  3. fix error

    @JasonKYi
    JasonKYi committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    17c63e4 View commit details
    Browse the repository at this point in the history

  4. fix error

    @JasonKYi
    JasonKYi committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    245cfb7 View commit details
    Browse the repository at this point in the history

  5. fix lint

    @JasonKYi
    JasonKYi committed Mar 26, 2022
    Configuration menu
    Copy the full SHA
    8f7c360 View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2022

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

     into JasonKYi/unif_integrable_equiv
    @JasonKYi
    JasonKYi committed Mar 30, 2022
    Configuration menu
    Copy the full SHA
    a2895be View commit details
    Browse the repository at this point in the history

  2. fix using new refactor

    @JasonKYi
    JasonKYi committed Mar 30, 2022
    Configuration menu
    Copy the full SHA
    502b30e View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2022

  1. remove old doc-string

    @JasonKYi
    JasonKYi committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    7c534a6 View commit details
    Browse the repository at this point in the history

  2. use max M 1 instead

    @JasonKYi
    JasonKYi committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    a46019c View commit details
    Browse the repository at this point in the history

  3. add indicator_ae_eq_of_ae_eq

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

Commits on Apr 7, 2022

  1. small golf

    @JasonKYi
    JasonKYi committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    09d1103 View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2022

  1. make lemma for general filters

    @JasonKYi
    JasonKYi committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    498f617 View commit details
    Browse the repository at this point in the history

  2. add lt_two_mul_self lemma for general semirings

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

  3. delete nnreal version and use semiring version

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

Commits on Apr 11, 2022

  1. Update src/order/filter/indicator_function.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @JasonKYi @sgouezel
    JasonKYi and sgouezel committed Apr 11, 2022
    Configuration menu
    Copy the full SHA
    c1dca6b View commit details
    Browse the repository at this point in the history