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(probability/strong_law): Lp version of the strong law of large numbers #15392

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat(probability/strong_law): Lp version of the strong law of large numbers #15392

wants to merge 16 commits into from

Commits on Jul 15, 2022

  1. initial commit

    @JasonKYi
    JasonKYi committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    e6cb689 View commit details
    Browse the repository at this point in the history

  2. add uniform_integrable_of_ident_distrib

    @JasonKYi
    JasonKYi committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    676ff8f View commit details
    Browse the repository at this point in the history

  3. done

    @JasonKYi
    JasonKYi committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    7700cd8 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2022

  1. change to integrable

    @JasonKYi
    JasonKYi committed Jul 16, 2022
    Configuration menu
    Copy the full SHA
    4fb433f View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2022

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

     into JasonKYi/strong_law_L1
    @JasonKYi
    JasonKYi committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    729e273 View commit details
    Browse the repository at this point in the history

  2. make assumption only require ae_strongly_measurable

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

  3. move lemma

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

Commits on Jul 27, 2022

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

     into JasonKYi/strong_law_L1
    @JasonKYi
    JasonKYi committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    0f16a3c View commit details
    Browse the repository at this point in the history

  2. Update src/probability/ident_distrib.lean 

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

  3. remove ae_strongly_measurable condition

    @JasonKYi
    JasonKYi committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    59d6bdf View commit details
    Browse the repository at this point in the history

  4. Merge branch 'JasonKYi/strong_law_L1' of https://github.com/leanprove… 

    …r-community/mathlib into JasonKYi/strong_law_L1
    @JasonKYi
    JasonKYi committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    2560dc2 View commit details
    Browse the repository at this point in the history

  5. remove frome slln too

    @JasonKYi
    JasonKYi committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    4e30940 View commit details
    Browse the repository at this point in the history

  6. Lp verison

    @JasonKYi
    JasonKYi committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    e24a5e4 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2022

  1. rename

    @JasonKYi
    JasonKYi committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    d232065 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

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

  3. fix

    @JasonKYi
    JasonKYi committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    2343f6b View commit details
    Browse the repository at this point in the history