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: add last implication of portmanteau characterizations of weak convergence #8097

Closed
wants to merge 50 commits into from
Closed

[Merged by Bors] - feat: add last implication of portmanteau characterizations of weak convergence #8097

wants to merge 50 commits into from

Commits on Jun 26, 2023

  1. A file with an outline of the proof of le_liminf_open_implies_converg… 

    …ence.
    kkytola committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    1149cc8 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. Thoughts.

    kkytola committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    a9ddc6d View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2023

  1. Switched to Metric.Bounded instead of Bornology.IsBounded.

    @kkytola
    kkytola committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    a10a674 View commit details
    Browse the repository at this point in the history

  2. Continuing to switch.

    @kkytola
    kkytola committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    c47250e View commit details
    Browse the repository at this point in the history

  3. Removing commented out bornology lemmas.

    @kkytola
    kkytola committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    310fc41 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    52e6a35 View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    68e779e View commit details
    Browse the repository at this point in the history

  2. Messing around trying to find the optimal hypotheses for liminf_add_c… 

    …onst and 7 friends.
    @kkytola
    kkytola committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    4949de9 View commit details
    Browse the repository at this point in the history

  3. limsup_const_add and 7 friends with essentially satisfactory assumpti… 

    …ons (except with subtraction counterparts have to assume AddCommGroup and one additional covariance property).
    @kkytola
    kkytola committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    8da382c View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    6dc6a70 View commit details
    Browse the repository at this point in the history

  2. Think about cleanup.

    @kkytola
    kkytola committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    6ccc892 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Aug 26, 2023
    Configuration menu
    Copy the full SHA
    3b88051 View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2023

  1. A more reasonable proof of a triviality (still not in the right gener… 

    …ality).
    @kkytola
    kkytola committed Aug 28, 2023
    Configuration menu
    Copy the full SHA
    d646758 View commit details
    Browse the repository at this point in the history

  2. Probably the right generality for the triviality.

    @kkytola
    kkytola committed Aug 28, 2023
    Configuration menu
    Copy the full SHA
    e1918ec View commit details
    Browse the repository at this point in the history

  3. Should maybe generalize the layercake file to use AEMeasurable (or AE… 

    …StronglyMeasurable?).
    @kkytola
    kkytola committed Aug 28, 2023
    Configuration menu
    Copy the full SHA
    7c2f5c9 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    kkytola committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    6d91bca View commit details
    Browse the repository at this point in the history

  2. Some fixes but VS Code is stuck...k...

    @kkytola
    kkytola committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    534bcde View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2023

  1. Clean up by moving lemmas about integrals of bounded continuous funct… 

    …ions to one file. Generalize to usual typeclasses.
    kkytola committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    26baf40 View commit details
    Browse the repository at this point in the history

  2. Small simplifications and cleaning up.

    kkytola committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    8e42e1f View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2023

  1. Small edits.

    kkytola committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    3b293b7 View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2023

  1. Merge?

    @kkytola
    kkytola committed Sep 30, 2023
    Configuration menu
    Copy the full SHA
    61c1ac2 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2023

  1. Towards an acceptable proof.

    @kkytola
    kkytola committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    597a41c View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2023

  1. Mostly reduced to a MonotoneOn version of map_liminf lemma.

    @kkytola
    kkytola committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    8d1aa9d View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Oct 21, 2023
    Configuration menu
    Copy the full SHA
    64fd2e2 View commit details
    Browse the repository at this point in the history

  2. Filling in stuff (coercion heavy). Oops with filter le.

    @kkytola
    kkytola committed Oct 21, 2023
    Configuration menu
    Copy the full SHA
    38a8c70 View commit details
    Browse the repository at this point in the history

  3. Fix the filter le and separate two lemmas that should exist.

    @kkytola
    kkytola committed Oct 21, 2023
    Configuration menu
    Copy the full SHA
    1d1c447 View commit details
    Browse the repository at this point in the history

  4. Delete a stupid direct proof attempt.

    @kkytola
    kkytola committed Oct 21, 2023
    Configuration menu
    Copy the full SHA
    af71e6b View commit details
    Browse the repository at this point in the history

  5. Hmmm... What is a reasonable way to prove the mapping of liminfs unde… 

    …r AntitoneOn functions?
    @kkytola
    kkytola committed Oct 21, 2023
    Configuration menu
    Copy the full SHA
    6eaf134 View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2023

  1. Let us take an ad hoc route and avoind map_liminf for MonotoneOn.

    kkytola committed Oct 30, 2023
    Configuration menu
    Copy the full SHA
    261221d View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2023

  1. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    26b57c0 View commit details
    Browse the repository at this point in the history

  2. Sorry-free avoiding MonotoneOn via ad hoc truncation.

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    f7def1b View commit details
    Browse the repository at this point in the history

  3. Some cleanup.

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    a58a27b View commit details
    Browse the repository at this point in the history

  4. Move some ENNReal lemmas to an appropriate file.

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    9b397ab View commit details
    Browse the repository at this point in the history

  5. Add Lipschitzness of Real.toNNReal.

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    cf94e14 View commit details
    Browse the repository at this point in the history

  6. Indent correctly.

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    fd6e7e6 View commit details
    Browse the repository at this point in the history

  7. Why did this material disappear when creating the PR?

    kkytola committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    cedbc62 View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2023

  1. Add a necessary import (Layercake) and fix broken things.

    @kkytola
    kkytola committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    552d0bc View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @kkytola @github-actions
    kkytola and github-actions[bot] committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    86e01b7 View commit details
    Browse the repository at this point in the history

  3. Moved a lemma and added docstrings and rearranged some.

    @kkytola
    kkytola committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    e4636d8 View commit details
    Browse the repository at this point in the history

  4. Lints.

    @kkytola
    kkytola committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    13070df View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2023

  1. Apply suggestions from code review 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @kkytola @sgouezel
    kkytola and sgouezel committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    40cc652 View commit details
    Browse the repository at this point in the history

  2. Clarify proof as requested.

    @kkytola
    kkytola committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    49178d3 View commit details
    Browse the repository at this point in the history

  3. Generalize two lemmas to assume the hypotheses only eventually along … 

    …the filter.
    @kkytola
    kkytola committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    0f4f62c View commit details
    Browse the repository at this point in the history

  4. Move two lemmas to their own file.

    @kkytola
    kkytola committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    049625c View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2023

  1. Fix a broken proof.

    @kkytola
    kkytola committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    e81404b View commit details
    Browse the repository at this point in the history

  2. Import the new file in Mathlib.lean.

    @kkytola
    kkytola committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    1731ccf View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/MeasureTheory/Measure/Portmanteau.lean 

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

  4. Correct one subscript in a docstring.

    @kkytola
    kkytola committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    31776b1 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into kkytola/portmanteau_open_implies_convergen… 

    …ce_overview
    @kkytola
    kkytola committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    45691a8 View commit details
    Browse the repository at this point in the history

  6. Replace ENNReal.some by ENNReal.ofNNReal.

    @kkytola
    kkytola committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    98debd0 View commit details
    Browse the repository at this point in the history