mathlib

mathlib copied to clipboard

I had a go at Minkowski's convex body theorem and it works thanks to @urkud 's pidgeonhole for measurable spaces. My interest is in the applications to number theory, hence the location of the file, but I'm happy to move it.

---

• [x] depends on: #8591
• [x] depends on: #8600
• [x] depends on: #8608
• [x] depends on: #8695
• [x] depends on: #16708

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.

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 .

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.

Should this depend on #8695 instead of #8642 ? Because it seems that the former supersedes the latter.

Should this depend on #8695 instead of #8642 ? Because it seems that the former supersedes the latter.

It should, thanks @jcommelin somehow I missed #8695 (thanks @PatrickMassot !!)

This PR/issue depends on:

• ~~leanprover-community/mathlib#8591~~
• ~~leanprover-community/mathlib#8600~~
• ~~leanprover-community/mathlib#8608~~
• ~~leanprover-community/mathlib#8695~~
• ~~leanprover-community/mathlib#16708~~
• leanprover-community/mathlib#17030 By Dependent Issues (🤖). Happy coding!

It seems that CI is happy with this. So after a little bit of cleaning up, this should be mergeable!

Please remove the commented code, move lemmas to appropriate files, and use to_additive to generate lemmas about is_add_fundamental_domain when possible. Also see #17293 for a version of exists_mul_inv_mem_lattice_of_volume_lt_volume.

@urkud indeed this still needs a lot of work, I'm slowly trying to make sure that the final theorem is actually usable for applications, and think more still needs doing. What results are you thinking of for to_additive? I think I'm already using that wherever possible.

I'd also still love to get a version of #17293 where having measure larger than n times the measure of the fundamental domain gives n + 1 distinct points that are equivalent under the action. Do you have a slick way of proving that too?

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

This PR/issue depends on:

• ~~leanprover-community/mathlib#8591~~
• ~~leanprover-community/mathlib#8600~~
• ~~leanprover-community/mathlib#8608~~
• ~~leanprover-community/mathlib#8695~~
• ~~leanprover-community/mathlib#16708~~
• ~~leanprover-community/mathlib#17030~~
• ~~leanprover-community/mathlib#17535~~
• ~~leanprover-community/mathlib#17536~~
• ~~leanprover-community/mathlib#17590~~
• ~~leanprover-community/mathlib#17766~~
• ~~leanprover-community/mathlib#17771~~
• ~~leanprover-community/mathlib#17773~~
• ~~leanprover-community/mathlib#17774~~
• ~~leanprover-community/mathlib#17775~~ By Dependent Issues (🤖). Happy coding!

~~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.

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests