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: port MeasureTheory.Function.L1Space #4383

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port MeasureTheory.Function.L1Space #4383

wants to merge 12 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented May 26, 2023 •
edited
Loading

@Komyyy Komyyy added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) awaiting-review mathlib-port This is a port of a theory file from mathlib. awaiting-CI labels May 26, 2023
@Komyyy Komyyy added WIP Work in progress and removed awaiting-review labels May 27, 2023
@Komyyy Komyyy closed this May 28, 2023
@Komyyy Komyyy reopened this May 28, 2023
@Komyyy Komyyy added awaiting-review awaiting-CI and removed WIP Work in progress labels May 28, 2023
@Komyyy Komyyy added WIP Work in progress and removed awaiting-review labels May 28, 2023
eric-wieser
eric-wieser requested changes May 28, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Please rebase this on the latest starT_port.sh output for l1_space (once the dependencies are merged), as the current version was ported from a file that said "please wait for ..." and did not wait.

@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels May 28, 2023
@kim-em
Copy link
Contributor

kim-em commented May 29, 2023

This PR/issue depends on:

Komyyy added 3 commits May 29, 2023 21:44
@Komyyy
feat: port MeasureTheory.Function.L1Space
f81f0ea
@Komyyy
Initial file copy from mathport
90c15a4
@Komyyy
automated fixes
7da5c4b 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy Komyyy force-pushed the port/MeasureTheory.Function.L1Space branch from cc74c95 to 53d553e Compare May 29, 2023 12:45
@Komyyy Komyyy added awaiting-review awaiting-CI and removed WIP Work in progress merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 29, 2023
@Komyyy Komyyy force-pushed the port/MeasureTheory.Function.L1Space branch from 53d553e to 27846e0 Compare May 29, 2023 12:55
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 29, 2023
@Komyyy Komyyy added WIP Work in progress and removed awaiting-review labels May 30, 2023
@Komyyy Komyyy added awaiting-review awaiting-CI and removed WIP Work in progress labels May 30, 2023
@kim-em
Copy link
Contributor

kim-em commented May 31, 2023

bors d+

@bors
Copy link

bors bot commented May 31, 2023

✌️ Komyyy can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@Komyyy
Copy link
Collaborator Author

Komyyy commented May 31, 2023

bors r+

bors bot pushed a commit that referenced this pull request May 31, 2023
@Komyyy
feat: port MeasureTheory.Function.L1Space (#4383)
27ebbd6
@bors
Copy link

bors bot commented May 31, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port MeasureTheory.Function.L1Space [Merged by Bors] - feat: port MeasureTheory.Function.L1Space May 31, 2023
@bors bors bot closed this May 31, 2023
@bors bors bot deleted the port/MeasureTheory.Function.L1Space branch May 31, 2023 05:40
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@Komyyy @qawbecrdtey
feat: port MeasureTheory.Function.L1Space (leanprover-community#4383)
3ffd7ef
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Komyyy @kim-em @eric-wieser @urkud