[Merged by Bors] - feat(MeasureTheory): Fatou's lemma for countably generated filters by CoolRmal · Pull Request #37313 · leanprover-community/mathlib4

CoolRmal · 2026-03-28T12:17:58Z

depends on: [Merged by Bors] - feat(Topology/Order): existence of a sequence that converges to limsup #37296

github-actions · 2026-03-28T12:19:06Z

PR summary 8f1377de1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Tendsto.liminf_le_liminf_comp
+ Tendsto.limsup_comp_le_limsup
+ lintegral_liminf_nat_le'

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Co-authored-by: Snir Broshi <[email protected]>

Co-authored-by: Anatole Dedecker <[email protected]>

…nto liminfsubseq

Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

mathlib-dependent-issues · 2026-04-03T18:22:03Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Topology/Order): existence of a sequence that converges to limsup #37296~~
By Dependent Issues (🤖). Happy coding!

Co-authored-by: Anatole Dedecker <[email protected]>

CoolRmal · 2026-04-03T21:19:09Z

-awaiting-author

ADedecker

Thanks!

bors merge

…37313)

mathlib-bors · 2026-04-05T01:34:22Z

Pull request successfully merged into master.

Build succeeded:

CoolRmal added 6 commits March 27, 2026 20:59

Update LiminfLimsup.lean

804442e

Update LiminfLimsup.lean

4e4f181

Update Bounded.lean

c52a230

Update Regular.lean

6b86e76

delete

46474a0

Update Add.lean

20562d4

CoolRmal changed the title ~~feat(MeasureTheory): Fatou's lemma for countably generated nontrivial filter~~ feat(MeasureTheory): Fatou's lemma for countably generated nontrivial filters Mar 28, 2026

github-actions bot added the t-measure-probability Measure theory / Probability theory label Mar 28, 2026

CoolRmal and others added 4 commits March 28, 2026 08:20

Update Mathlib/Topology/Order/LiminfLimsup.lean

c8ed5af

Co-authored-by: Snir Broshi <[email protected]>

Update Mathlib/Topology/Order/LiminfLimsup.lean

0b06a92

Co-authored-by: Snir Broshi <[email protected]>

Merge branch 'liminfsubseq' into fatou

a9c3445

Merge branch 'liminfsubseq' into fatou

082e84e

CoolRmal mentioned this pull request Mar 28, 2026

feat(MeasureTheory): uniformly distributed outer regular measures in a second countable pseudometric space are unique up to a finite constant #37310

Open

3 tasks

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 28, 2026

CoolRmal and others added 15 commits March 28, 2026 08:32

Update Add.lean

1466945

Update Add.lean

a167a65

update

71177e8

update

6446519

fixdocstring

d484892

deprecation

a1d9ed7

Update CountablyCompact.lean

e728bdf

Update CountablyCompact.lean

fae2367

Update Mathlib/Topology/Order/LiminfLimsup.lean

afd38b0

Co-authored-by: Anatole Dedecker <[email protected]>

Update Bases.lean

1a0d269

Merge branch 'liminfsubseq' of https://github.com/CoolRmal/mathlib4 i…

e1e3a3c

…nto liminfsubseq

Merge branch 'master' into liminfsubseq

31e690f

address comments

bb68313

Update LiminfLimsup.lean

17f5072

Update Sequences.lean

3aef770

CoolRmal added 2 commits April 2, 2026 21:40

Update Sequences.lean

29ef4b2

Update LiminfLimsup.lean

88f4129

ADedecker reviewed Apr 3, 2026

View reviewed changes

Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean Outdated Show resolved Hide resolved

ADedecker reviewed Apr 3, 2026

View reviewed changes

Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean Outdated Show resolved Hide resolved

ADedecker reviewed Apr 3, 2026

View reviewed changes

Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean Outdated Show resolved Hide resolved

ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

Merge branch 'master' into fatou

1561d11

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 3, 2026

CoolRmal and others added 2 commits April 3, 2026 14:24

Merge branch 'liminfsubseq' into fatou

eeebe47

Update Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

b938413

Co-authored-by: Anatole Dedecker <[email protected]>

CoolRmal changed the title ~~feat(MeasureTheory): Fatou's lemma for countably generated nontrivial filters~~ feat(MeasureTheory): Fatou's lemma for countably generated filters Apr 3, 2026

address comments

9b6538b

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

mathlib-triage bot assigned kex-y Apr 4, 2026

ADedecker reviewed Apr 5, 2026

View reviewed changes

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 5, 2026

mathlib-bors bot pushed a commit that referenced this pull request Apr 5, 2026

feat(MeasureTheory): Fatou's lemma for countably generated filters (#…

f47b612

…37313)

mathlib-bors bot changed the title ~~feat(MeasureTheory): Fatou's lemma for countably generated filters~~ [Merged by Bors] - feat(MeasureTheory): Fatou's lemma for countably generated filters Apr 5, 2026

mathlib-bors bot closed this Apr 5, 2026

CoolRmal deleted the fatou branch April 5, 2026 02:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(MeasureTheory): Fatou's lemma for countably generated filters#37313

[Merged by Bors] - feat(MeasureTheory): Fatou's lemma for countably generated filters#37313
CoolRmal wants to merge 31 commits intoleanprover-community:masterfrom
CoolRmal:fatou

CoolRmal commented Mar 28, 2026

Uh oh!

github-actions bot commented Mar 28, 2026 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues bot commented Apr 3, 2026

Uh oh!

CoolRmal commented Apr 3, 2026

Uh oh!

ADedecker left a comment

Uh oh!

mathlib-bors bot commented Apr 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

CoolRmal commented Mar 28, 2026

Uh oh!

github-actions bot commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8f1377de1f

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues bot commented Apr 3, 2026

Uh oh!

CoolRmal commented Apr 3, 2026

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented Mar 28, 2026 •

edited

Loading