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/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems #2819

Closed
wants to merge 189 commits into from
Closed

[Merged by Bors] - feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems #2819

wants to merge 189 commits into from

Conversation

alexjbest
Copy link
Member

@alexjbest alexjbest commented May 25, 2020 •
edited by xroblot

I had a go at Minkowski's convex body theorem and it works thanks to @urkud 's pidgeonhole for measurable spaces.

Open in Gitpod

@alexjbest alexjbest added help-wanted The author needs attention to resolve issues incomplete not-ready-to-merge WIP Work in progress labels May 25, 2020
@urkud
Copy link
Member

urkud commented May 26, 2020

Please split this into smaller PRs. E.g., I see that you have a prod.measure_space instance. This definitely can (and should) be a separate PR.

This way (a) some chunks will be merged before the whole diff is cleared; (b) people will be able to review parts of the PR that touch files they feel responsible for/comfortable with while not taking responsibility for other parts of your PR.

@alexjbest
Copy link
Member Author

Sorry I should have been more clear, the two large files in measure theory are from https://github.com/jtristan/stump-learnable if the authors are ok with it I will PR the relevant parts (separately), not all of it is needed for this application. But first I would like to know if defining the product measure via the monadic machinery they develop is the best way, or wether it is recommended to use a different approach to get the lebesgue measure on R^n .

@urkud
Copy link
Member

urkud commented May 26, 2020 •
edited

stump-learnable is under the same Apache 2.0 license, so you may PR code from that repo without asking the authors as long as you preserve their copyrights. It's pretty clear to me that they're not going to submit PRs themselves.

@bryangingechen bryangingechen changed the title [WIP] feat(number_theory/geometry_of_numbers) Minkowski's theorem [WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem Jun 25, 2020
@alexjbest alexjbest added the please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. label Nov 1, 2020
@alexjbest alexjbest removed the help-wanted The author needs attention to resolve issues label Aug 8, 2021
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 13, 2023
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 1, 2023
@xroblot xroblot mentioned this pull request Feb 21, 2023
Closed
4 tasks
@xroblot
Copy link
Collaborator

xroblot commented Mar 30, 2023 •
edited

I have committed a new proof of Minkowski's theorem (and Blichfeldt's theorem) that doesn't require a basis and thus doesn't rely anymore on #18343

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 30, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@xroblot
Copy link
Collaborator

xroblot commented Mar 30, 2023 •
edited

The new version requires the hypothesis measurable_set T. As suggested by @YaelDillies, it would be nice to remove this hypothesis using the fact that T is convex using convex.null_measurable_set.

But, then it is necessary to prove that ((2⁻¹ : ℝ) • T) is also null_measurable_set for μ and there is no version of measurable_set.const_smul₀ for null_measurable_set.

I tried to prove the result but I did not succeed. In fact, there is measure_theory.null_measurable_set.smul that could be easily adapted to the case of group_with_zero but is requires that the measure is smul_invariant_measure and we certainly do not want that so I suspect this is not so easy to prove...

This is now fixed thanks to the help of Yaël.

eric-wieser
eric-wieser reviewed Mar 31, 2023
View reviewed changes
src/measure_theory/group/geometry_of_numbers.lean
open ennreal finite_dimensional measure_theory measure_theory.measure set
open_locale pointwise

variables {E L : Type*} [measurable_space E] {μ : measure E} {F s : set E}
Copy link
Member

Choose a reason for hiding this comment

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

It feels weird to me to have F and s appear before all the typeclass arguments. Can you put these in the lemma statements instead?

Copy link
Collaborator

Choose a reason for hiding this comment

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

"typeclass arguments first" is a bit of a meaningless rule when you get to measure theory where there are many typeclasses some of which depend on non-typeclasses. I certainly won't enforce it here if it leads to duplicating variable declarations.

jcommelin
jcommelin approved these changes Mar 31, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Mar 31, 2023
bors bot pushed a commit that referenced this pull request Mar 31, 2023
@alexjbest @YaelDillies
@xroblot @RemyDegenne
feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkow…
02e095b 
…ski's theorems (#2819)

I had a go at Minkowski's convex body theorem and it works thanks to @urkud 's pidgeonhole for measurable spaces.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
@bors
Copy link

bors bot commented Mar 31, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems [Merged by Bors] - feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems Mar 31, 2023
@bors bors bot closed this Mar 31, 2023
@bors bors bot deleted the minkowski branch March 31, 2023 22:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

@ocfnash ocfnash ocfnash left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@jcommelin jcommelin jcommelin 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+`.) t-algebra Algebra (groups, rings, fields etc) t-measure-probability Measure theory / Probability theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet