Skip to content

[Merged by Bors] - feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt#5650

Closed
xroblot wants to merge 67 commits intomasterfrom
xfr-canonical_embedding_minkowski
Closed

[Merged by Bors] - feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt#5650
xroblot wants to merge 67 commits intomasterfrom
xfr-canonical_embedding_minkowski

Conversation

@xroblot
Copy link
Copy Markdown
Collaborator

@xroblot xroblot commented Jul 1, 2023 •
edited by github-actions bot
Loading

This PR proves the following result:

theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w

where f : InfinitePlace K → ℝ≥0 and convex_body_lt K f is the set of points x such that ‖x w‖ < f w for all infinite places w. This is a key result in the proof of Dirichlet's unit theorem #5960

Open in Gitpod

@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 1, 2023
@xroblot xroblot added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 1, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 1, 2023
@xroblot xroblot added the WIP Work in progress label Jul 9, 2023
@xroblot xroblot mentioned this pull request Jul 17, 2023
Closed
3 tasks
@xroblot xroblot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Jul 18, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 16, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 16, 2023

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 16, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 16, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:25
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:16
jcommelin
jcommelin reviewed Sep 18, 2023
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Sep 18, 2023
@xroblot xroblot added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 19, 2023
jcommelin
jcommelin reviewed Sep 19, 2023
View reviewed changes
@jcommelin jcommelin changed the title feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ring_of_integers_lt feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt Sep 19, 2023
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 19, 2023

I think this is looking pretty good now. If you fix the two naming issues that I pointed out above, please kick this on the bors queue.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 19, 2023

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

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Sep 19, 2023
@xroblot
Copy link
Copy Markdown
Collaborator Author

xroblot commented Sep 20, 2023

bors r+

bors bot pushed a commit that referenced this pull request Sep 20, 2023
@xroblot
feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero…
14b1439 
…_mem_ringOfIntegers_lt (#5650)

This PR proves the following result: 
```lean
theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w 
```
where `f : InfinitePlace K → ℝ≥0` and `convex_body_lt K f` is the set of points `x` such that `‖x w‖ < f w` for all infinite places `w`. This is a key result in the proof of Dirichlet's unit theorem #5960
@bors
Copy link
Copy Markdown

bors bot commented Sep 20, 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(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt [Merged by Bors] - feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt Sep 20, 2023
@bors bors bot closed this Sep 20, 2023
@bors bors bot deleted the xfr-canonical_embedding_minkowski branch September 20, 2023 09:59
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@xroblot @kodyvajjha
feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero…
d9c5067 
…_mem_ringOfIntegers_lt (#5650)

This PR proves the following result: 
```lean
theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w 
```
where `f : InfinitePlace K → ℝ≥0` and `convex_body_lt K f` is the set of points `x` such that `‖x w‖ < f w` for all infinite places `w`. This is a key result in the proof of Dirichlet's unit theorem #5960
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@xroblot @jcommelin @kim-em