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(measure_theory/lp_space): add mem_Lp.mono_measure #7927

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(measure_theory/lp_space): add mem_Lp.mono_measure #7927

wants to merge 5 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

also add monotonicity lemmas wrt the measure for snorm', snorm_ess_sup and snorm.

Open in Gitpod

@RemyDegenne RemyDegenne added the awaiting-review The author would like community review of the PR label Jun 14, 2021
@RemyDegenne
Copy link
Collaborator Author

I don't know why the checks got cancelled. Is there a way to restart them?

@RemyDegenne
Copy link
Collaborator Author

I think that the checks got cancelled because I have another branch (continuous_set_integral) which builds upon this one and in which I have a newer commit.

@RemyDegenne RemyDegenne mentioned this pull request Jun 14, 2021
Closed
1 task
hrmacbeth
hrmacbeth reviewed Jun 14, 2021
View reviewed changes
Copy link
Member

@hrmacbeth hrmacbeth left a comment

Choose a reason for hiding this comment

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

You could tag these lemmas @[mono], if they happen to be compatible with the monotonicity tactic. Otherwise LGTM.

src/measure_theory/lp_space.lean Outdated
@@ -413,6 +413,38 @@ lemma mem_ℒp.of_bound [finite_measure μ] {f : α → E} (hf : ae_measurable f
mem_ℒp f p μ :=
(mem_ℒp_const C).of_le hf (hfC.mono (λ x hx, le_trans hx (le_abs_self _)))

lemma snorm'_mono_measure {μ ν : measure α} {f : α → F} (hμν : ν ≤ μ) (hq : 0 ≤ q) :
Copy link
Member

Choose a reason for hiding this comment

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

Should be f explicit here, and in the next two lemmas? (I am not sure ... in your use case here it is not needed.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks. I made it explicit, since it cannot be inferred from other arguments. It was not needed in the places where I use those lemmas, but I think it's better to have one more argument than to require @ when one want to write have h := snorm'_mono_measure ...

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 14, 2021
@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 15, 2021
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 15, 2021
bors bot pushed a commit that referenced this pull request Jun 15, 2021
@RemyDegenne
feat(measure_theory/lp_space): add mem_Lp.mono_measure (#7927)
2f1f34a 
also add monotonicity lemmas wrt the measure for `snorm'`, `snorm_ess_sup` and `snorm`.
@bors
Copy link

bors bot commented Jun 15, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/lp_space): add mem_Lp.mono_measure [Merged by Bors] - feat(measure_theory/lp_space): add mem_Lp.mono_measure Jun 15, 2021
@bors bors bot closed this Jun 15, 2021
@bors bors bot deleted the mem_Lp_mono_measure branch June 15, 2021 19:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hrmacbeth hrmacbeth hrmacbeth left review comments

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
3 participants
@RemyDegenne @sgouezel @hrmacbeth