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 (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem #14026

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem #14026

wants to merge 23 commits into from

Conversation

fbarroero
Copy link
Collaborator

@fbarroero fbarroero commented Jun 22, 2024 •
edited
Loading

In this PR we prove that a non-archimedean non-trivial absolute value on the rational is equivalent to a padic one.

Main result

theorem mulRingNorm_equiv_padic_of_bounded :
    ∃! p, ∃ (hp : Fact (Nat.Prime p)), MulRingNorm.equiv f (mulRingNorm_padic p)

Co-authored-by:

David Kurniadi Angdinata [email protected]
Laura Capuano [email protected]
Nirvana Coppola [email protected]
María Inés de Frutos Fernández [email protected]
Sam van Gool [email protected]
Silvain Rideau-Kikuchi [email protected]
Amos Turchet [email protected]
Francesco Veneziano [email protected]

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 22, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 22, 2024 •
edited
Loading

PR summary 9564ea302a

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.NumberTheory.Ostrowski 1288 1291 +3 (+0.23%)

Declarations diff

+ eq_on_nat_iff_eq
+ eq_on_nat_iff_eq_on_Int
+ equiv_on_nat_iff_equiv
+ exists_minimal_nat_zero_lt_mulRingNorm_lt_one
+ exists_pos_mulRingNorm_eq_pow_neg
+ is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one
+ mulRingNorm_eq_one_of_not_dvd
+ mulRingNorm_eq_padic_norm
+ mulRingNorm_equiv_padic_of_bounded
+ mulRingNorm_padic
- eq_on_Nat_iff_eq
- eq_on_Nat_iff_eq_on_Int
- equiv_on_Nat_iff_equiv

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@fbarroero fbarroero added awaiting-review t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jun 22, 2024
@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 22, 2024
@MichaelStollBayreuth
Copy link
Collaborator

@fbarroero Can you change "Nat" to "nat" in eq_on_Nat_iff_eq_on_Int and the following two lemmas in a follow-up PR? Also, there should be spaces around ^ in

lemma equiv_on_Nat_iff_equiv : (∃ c : ℝ, 0 < c ∧ (∀ n : ℕ , (f n)^c = g n)) ↔ f.equiv g

But this is, I think, out of scope for this PR.

MichaelStollBayreuth
MichaelStollBayreuth approved these changes Jun 24, 2024
View reviewed changes
Copy link
Collaborator

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

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

LGTM!

@fbarroero
Copy link
Collaborator Author

fbarroero commented Jun 24, 2024 •
edited
Loading

@fbarroero Can you change "Nat" to "nat" in eq_on_Nat_iff_eq_on_Int and the following two lemmas in a follow-up PR? Also, there should be spaces around ^ in

lemma equiv_on_Nat_iff_equiv : (∃ c : ℝ, 0 < c ∧ (∀ n : ℕ , (f n)^c = g n)) ↔ f.equiv g

But this is, I think, out of scope for this PR.

Why should I not do it in this PR?

@riccardobrasca riccardobrasca self-assigned this Jun 24, 2024
riccardobrasca
riccardobrasca reviewed Jun 24, 2024
View reviewed changes
@MichaelStollBayreuth
Copy link
Collaborator

Why should I not do it in this PR?

You can of course do that here, too, if you like. I just didn't want to make that a requirement, as it is somewhat orthogonal to the original purpose.

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 25, 2024
@riccardobrasca
Copy link
Member

Oh sorry, CI is still running

bors r-

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

Canceled.

@riccardobrasca
Copy link
Member

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

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

@riccardobrasca
Copy link
Member

bors merge

@fbarroero
Copy link
Collaborator Author

bors r+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

Already running a review

mathlib-bors bot pushed a commit that referenced this pull request Jun 25, 2024
@fbarroero
Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of O…
bf26137 
…strowski's Theorem (#14026)

In this PR we prove that a non-archimedean non-trivial absolute value on the rational is equivalent to a padic one.

Main result
```lean
theorem mulRingNorm_equiv_padic_of_bounded :
    ∃! p, ∃ (hp : Fact (Nat.Prime p)), MulRingNorm.equiv f (mulRingNorm_padic p)
```

Co-authored-by:

David Kurniadi Angdinata [[email protected]](mailto:[email protected])
Laura Capuano [[email protected]](mailto:[email protected])
Nirvana Coppola [[email protected]](mailto:[email protected])
María Inés de Frutos Fernández [[email protected]](mailto:[email protected])
Sam van Gool [[email protected]](mailto:[email protected])
Silvain Rideau-Kikuchi [[email protected]](mailto:[email protected])
Amos Turchet [[email protected]](mailto:[email protected])
Francesco Veneziano [[email protected]](mailto:[email protected])
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem [Merged by Bors] - Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem Jun 25, 2024
@mathlib-bors mathlib-bors bot closed this Jun 25, 2024
@mathlib-bors mathlib-bors bot deleted the fbarroero_ostrowski_nonarch branch June 25, 2024 10:35
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@fbarroero @kbuzzard
Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of O…
6d39203 
…strowski's Theorem (#14026)

In this PR we prove that a non-archimedean non-trivial absolute value on the rational is equivalent to a padic one.

Main result
```lean
theorem mulRingNorm_equiv_padic_of_bounded :
    ∃! p, ∃ (hp : Fact (Nat.Prime p)), MulRingNorm.equiv f (mulRingNorm_padic p)
```

Co-authored-by:

David Kurniadi Angdinata [[email protected]](mailto:[email protected])
Laura Capuano [[email protected]](mailto:[email protected])
Nirvana Coppola [[email protected]](mailto:[email protected])
María Inés de Frutos Fernández [[email protected]](mailto:[email protected])
Sam van Gool [[email protected]](mailto:[email protected])
Silvain Rideau-Kikuchi [[email protected]](mailto:[email protected])
Amos Turchet [[email protected]](mailto:[email protected])
Francesco Veneziano [[email protected]](mailto:[email protected])
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@fbarroero @dagurtomas
Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of O…
f4e7373 
…strowski's Theorem (#14026)

In this PR we prove that a non-archimedean non-trivial absolute value on the rational is equivalent to a padic one.

Main result
```lean
theorem mulRingNorm_equiv_padic_of_bounded :
    ∃! p, ∃ (hp : Fact (Nat.Prime p)), MulRingNorm.equiv f (mulRingNorm_padic p)
```

Co-authored-by:

David Kurniadi Angdinata [[email protected]](mailto:[email protected])
Laura Capuano [[email protected]](mailto:[email protected])
Nirvana Coppola [[email protected]](mailto:[email protected])
María Inés de Frutos Fernández [[email protected]](mailto:[email protected])
Sam van Gool [[email protected]](mailto:[email protected])
Silvain Rideau-Kikuchi [[email protected]](mailto:[email protected])
Amos Turchet [[email protected]](mailto:[email protected])
Francesco Veneziano [[email protected]](mailto:[email protected])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth approved these changes

Assignees

@riccardobrasca riccardobrasca

Labels
delegated new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. 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.
4 participants
@fbarroero @MichaelStollBayreuth @riccardobrasca @erdOne