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

feat(measure_theory/integration): dominated convergence theorem #1123

Merged
merged 10 commits into from
Jun 14, 2019
Merged

feat(measure_theory/integration): dominated convergence theorem #1123

merged 10 commits into from
Jun 14, 2019

Conversation

aceg00
Copy link
Collaborator

@aceg00 aceg00 commented Jun 9, 2019

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@aceg00 aceg00 requested a review from a team as a code owner June 9, 2019 05:19
minchaowu
minchaowu reviewed Jun 9, 2019
View reviewed changes
src/measure_theory/borel_space.lean Outdated Show resolved Hide resolved
src/measure_theory/borel_space.lean Outdated Show resolved Hide resolved
src/measure_theory/borel_space.lean Outdated Show resolved Hide resolved
avigad
avigad requested changes Jun 12, 2019
View reviewed changes
Copy link
Collaborator

@avigad avigad left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR looks very good to me. I'll meet with Zhouhang (Joe) tomorrow, and approve once these changes are made, if there are no objections.

src/measure_theory/integration.lean Outdated Show resolved Hide resolved
src/measure_theory/integration.lean Outdated Show resolved Hide resolved
src/measure_theory/measure_space.lean Outdated Show resolved Hide resolved
src/measure_theory/integration.lean Outdated Show resolved Hide resolved
src/topology/instances/nnreal.lean Outdated Show resolved Hide resolved
@avigad avigad added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jun 14, 2019
@mergify mergify bot merged commit 5040c81 into leanprover-community:master Jun 14, 2019
@aceg00 aceg00 deleted the bochner branch June 22, 2019 07:51
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@anrddh
feat(measure_theory/integration): dominated convergence theorem (lean…
104298c 
…prover-community#1123)

* Create .DS_Store

* Revert "Create .DS_Store"

This reverts commit 5612886.

* feat(measure_theory/integration): dominated convergence theorem

* Changes to styles

* Update ordered.lean

* Changes to styles

* Update integration.lean

* Changes to styles
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kckennylau kckennylau kckennylau left review comments

@minchaowu minchaowu minchaowu left review comments

@avigad avigad avigad approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@aceg00 @avigad @kckennylau @minchaowu