Ostrowski's Theorem Project

Stream: LFTCM 2024

[María Inés de Frutos Fernández]

The partial Lean 3 version is at https://github.com/mariainesdff/ostrowski.

[Fabrizio Barroero]

I'm in!

[Amos Turchet]

Me (and Laura Capuano which is arriving soon) are interested

[Francesco Veneziano]

Me too!

[Silvain Rideau-Kikuchi]

And me too!

[Pietro Monticone]

Me too

[Nirvana Coppola]

Unless anyone shows up in the Schur Functions project, in which case I feel like I should contribute, I'm in :)

[Laura Capuano]

I'm in! (just arrived)

[María Inés de Frutos Fernández]

Great! We will meet at the library after the coffee break to get started :smile:

[Pietro Monticone]

I'll arrive later after having contributed to the FLT3 project.

[Amos Turchet]

We wrote three steps for the proof of each of the two lemmas we wrote before (archimedean and not archimedean) following conrad's note as a reference (in the README.md file)

[Sam van G]

I formalized the statements of step 1 and 2 of the Archimedean case, leaving the proofs sorry. I also added some documentation to the file. Feel free to do the same for your outline of the non-Archimedean case.

[Amos Turchet]

some of the steps can probably be split into smaller steps

[María Inés de Frutos Fernández]

We are at the library.

[Amos Turchet]

For the Archimedean part we need the following lemma: is it already in Mathlib?
lemma MulRingNorm_le (n : ℕ) (f : MulRingNorm ℚ) : f n ≤ n :=
The proof is easy by induction on n
If it is not in Mathlib maybe we should consider adding it to the Basic file

[Johan Commelin]

I can't find it, but it should be a 3-line induction proof

[Sam van G]

Good exercise! :)

[Amos Turchet]

Got almost a proof, but it got stuck in the easiest step (using that f(1) = 1) and no idea why

lemma MulRingNorm_nat_le_nat (n : ℕ) (f : MulRingNorm ℚ) : f n ≤ n := by
  induction' n with n hn
  · push_cast
    rw [le_iff_lt_or_eq]
    right
    exact f.map_zero'
  · push_cast
    calc
      f (↑n + 1) ≤ f (↑n) + f 1 := by exact f.add_le' ↑n 1
      _ = f (↑n) + 1 := by sorry -- rw[f.map_one']
      _ ≤ ↑n + 1 := by exact add_le_add_right hn 1

[María Inés de Frutos Fernández]

What error do you get when you try that rw[f.map_one']?

[Amos Turchet]

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
f.toFun 1

[Sam van G]

I think rw[map_one] should work

[Amos Turchet]

it does......but why?

[María Inés de Frutos Fernández]

Because f is a MulRingNorm, so Lean is able to infer that f 1 = 1 (it finds a OneHomClass instance).

[Sam van G]

I think it's because map_one' gives f.toFun 1 = 1, whereas map_one gives directly f 1 = 1. This is a subtle thing that's also been bugging me though.

[María Inés de Frutos Fernández]

Yes, that is why map_one' is failing.

[Sam van G]

One way to avoid this kind of problem is to write simp?. It suggests simp only [map_one] in this case. This doesn't always work but it's nice when it does.

[Anatole Dedecker]

The ' version is supposed to tell you not to use it :wink:

[Amos Turchet]

The file README.md contains now a short list of info that we are planning to use in the presentation

[Amos Turchet]

if you have any comments or suggestions feel free to tell us!

[Nirvana Coppola]

How did the presentation go? :octopus:

[Amos Turchet]

I think it went well, we kept it kind of short but hopefully informative enough for the audience

[Kevin Buzzard]

How's the PRing to mathlib going? :-)

[Nirvana Coppola]

Kevin Buzzard said:

How's the PRing to mathlib going? :-)

Good question.

[Nirvana Coppola]

Anyway, I'll have a few talks to prepare in the next days, but after that I'm happy to resume this work! :)

[Amos Turchet]

Maybe we should start pushing some lemmas soon? Not sure how this is done usually

[Riccardo Brasca]

In general it is better to open small PRs. Don't worry if there are only preliminary lemmas, that is totally fine.

[Riccardo Brasca]

In practice as soon you have a lemma that you think is ready you can open the PR

[Amos Turchet]

Would it be better to create a different file which contains some of the lemmas and push that one?

[Riccardo Brasca]

Well, it depends on the lemmas. If they're very basic you can probably find a file to put them in mathlib. But the best is to open a PR and discuss it on github

[Riccardo Brasca]

note that if you modify, say "Mathlib.VeryBasic.Basic", you can push, CI will do its work, after some time lake exe cache get will get the oleans

[Johan Commelin]

#find_home! lemmaName will tell you a good place to put the lemma

[Damiano Testa]

Johan Commelin said:

#find_home! lemmaName will tell you a good place to put the lemma

and if the results do not convince you, try it with import Mathlib or you may have found a bug in #find_home!

[Amos Turchet]

I made some small changes to the file. I realized that step 1 Arch is what makes the files very slow (at least in my Mac) so i started pulling out some of the haves that have long proofs into separate lemmas (as @Nirvana Coppola started doing) and already with two lemmas the speed increase is noticeable.

[María Inés de Frutos Fernández]

I think that everything in Basic.lean could be PR'd in the file Mathlib.Analysis.Normed.Ring.Seminorm. This would require adding an import to that file (Mathlib.Analysis.SpecialFunctions.Pow.Real), but since Mathlib.Analysis.Normed.Ring.Seminorm is not imported by anything yet, that is probably ok.

[María Inés de Frutos Fernández]

Who wants to PR it? :smile:

[Kevin Buzzard]

If someone who's never made a PR before makes the PR then they get special treatment from reviewers :-)

[Damiano Testa]

... and if they start it from the current master, their PR should be automatically labeled as new-contributor!

(This would be a great test of the bot.)

[Amos Turchet]

I can do it

[Amos Turchet]

@María Inés de Frutos Fernández does it make sense to move any of the lemmas in the first part of Rationals into basic?

[María Inés de Frutos Fernández]

I would PR what is in Basic.lean first (short PRs are preferred, especially for first contributions).
What lemmas would you like to move?

[Amos Turchet]

Ok let's try to PR these and we can discuss what to move later (there are lemmas about the triangle inequality of MulRingNorms with lists like flits_triang but it has probably to be written in a better way (and possibly generalized)

[María Inés de Frutos Fernández]

Yes, I think that this lemma could be generalized using any ring instead of ℚ and any function satisfying SubadditiveHomClass. There are probably other lemmas in Rationals.lean and MulRingNormRat.lean that are currently stated for ℚ but actually hold in greater generality.

[Amos Turchet]

If I did everything correctly we have our first PR:
https://github.com/leanprover-community/mathlib4/pull/11852

[Anatole Dedecker]

Please choose a more descriptive name than my_new_branch in the future :wink: (but no need to change it now that the PR is open)

[Amos Turchet]

Sorry about that, I was too focused on following every step of the tutorial for the new PR that forgot to change the name

[Anatole Dedecker]

No worries!

[Damiano Testa]

Sadly, the new-contributor's bot reports

continuous integration / New Contributor Check (push) — Found 30 PRs by this author.

:face_palm:

[Amos Turchet]

30? :flushed:

[Damiano Testa]

In fact, this is just a lower bound: apparently it stops counting at 30. No one seems to know what it is that it is counting, though, since according to GitHub you have 1 PR...

[Filippo A. E. Nuccio]

From the Italian academic perspective, 30 is a nice number... :top_hat:

[Fabrizio Barroero]

In the meanwhile I removed the last sorry in step 2 of the Archimedean case. There is one sorry left in fn_le_from_expansion, but that should follow from the lemma right before that.

[Francesco Veneziano]

I simplified the proof of the last lemma in MulRingNormRat.lean

[Fabrizio Barroero]

We have a first sorry-free proof of Ostrowski's Theorem for the rationals!
There is a lot of cleaning up to do and comments to add

[Sam van G]

Great!! I can have a look at it today and see if there's anything I can do to help with cleaning up.

[Sam van G]

We should then also start discussing how to PR it into Mathlib. If I've understood correctly the maintainers prefer to review small pieces (it is currently about 1200 lines.
Maybe @María Inés de Frutos Fernández and/or @Riccardo Brasca have more suggestions about that?

[Sam van G]

I just noticed this file Prova.lean, I guess it was not intended to be committed?

[Riccardo Brasca]

I won't be at the computer until next Monday, but smaller PR are surely a good idea.

[Fabrizio Barroero]

Sam van G said:

I just noticed this file Prova.lean, I guess it was not intended to be committed?

Sorry, that one is some file I pushed by mistake... I erase it...

[Amos Turchet]

There are some lemmas in the file MulRingNormRat that sounds the easiest to clean up/generalize/PR as a smaller PR

[Amos Turchet]

There’s also stuff about lists that looks simpler to move into a separate smaller PR

[Amos Turchet]

But I agree that someone with more experience can give better suggestions

[Fabrizio Barroero]

I agree that facts about lists can make a reasonable small PR

[Sam van G]

If you want I think you can already go ahead and put those facts about lists into one PR, mentioning that it is part of Ostrowski for rationals. If I remember right Johan helped you with those facts, so he can probably tell you where in Mathlib they should go.

[Johan Commelin]

Probably in the folder on digits... :smiley:

[Fabrizio Barroero]

For future use, what is the command that tries to find a folder where some lemma could fit? Someone told me last week but I forgot

[Kevin Buzzard]

I think find_home!? Or possibly #find_home!?

[Michael Stoll]

#find_home <name> or #find_home! <name>.

[Fabrizio Barroero]

Thanks!!!

[Amos Turchet]

First PR is now officially merged to mathlib!

[Nirvana Coppola]

What up next? :) I'll be back in Strasbourg soon, and I'm ready to start working again!

[Kevin Buzzard]

Well getting this stuff into mathlib is important. If you're looking for more maths to do then there's the extension to number fields. This doesn't involve redoing everything: you have a valuation on a number field and you want to show that it's either P-adic or an embedding into \C, and you can do this by restricting to \Q and then using techniques that Maria Ines has developed

[Amos Turchet]

I think one first step would be to start polishing the lemmas in the file MulRingNormRat, see what can be written in a more general setting, and probably start a PR for those

[Amos Turchet]

I'm planning to do the same for some of the Lemmas with the lists and Nat.digits that can also be PR separately

[Amos Turchet]

then at one point there would probably be a "bigger" PR with the whole Ostrowski for Q

[María Inés de Frutos Fernández]

There were also some lemmas about limits that could be PR'd separately, right?

[María Inés de Frutos Fernández]

After the general lemmas are PR'd, the proof of Ostrowski could be split in two PRs (one for each case).

[Nirvana Coppola]

Ok then since this NormRat lemma I wrote looks hideous I'll try to polish that. Also, I just noticed that I called it Norm_Rat_bla as opposed to NormRat_bla like the others so I'll fix that too. Sahll we also get rid of the comments that refer to the old lean3 version?

[Nirvana Coppola]

Ok, thinking about how to write things more generally I added this lemma (NormRat_equiv_iff_equiv_on_Nat1) even though then we need a slight specialization of it. Please let me know if it's worth PRing it (or the other one, or both, or neither)

[Fabrizio Barroero]

Hi all, the main file now only calls one version of NormRat_equiv_iff_equiv_on_Nat , the one added by Nirvana. I commented the other ones. I have also commented the imports of Basic.lean, since now everything there is in Mathlib. I think the four uncommented lemmas in MulRingNormRat.lean can all be PRd to Mathlib. @Nirvana Coppola , do you want to do it?

[Nirvana Coppola]

Great thanks! Sure, but it's my first PR so it will take a while, don't get alarmed if you don't see it immediately.

[Filippo A. E. Nuccio]

Please keep in mind that we have the new contributor label that you can add to PR's.

[Kevin Buzzard]

I think a machine now adds this label!

[Fabrizio Barroero]

can the label be used for the first contribution only? or for the first few ones?

[Michael Stoll]

I think the label is added as long as fewer than 5 (or so) PRs have been merged (or perhaps closed).

[Nirvana Coppola]

The new version of mathlib messed up some imports and name of theorems we were using and I just fixed it for our repo, I think. If any of you has time, can you check it compiles?

[Fabrizio Barroero]

It doesn't compile for me...
Before doing the last changes the other day, I had to manually update Mathlib. Maybe you have to do it too.
I see you changed Real.rpow_natCast to Real.rpow_nat_cast. If you look in the documentation the second does not exist. I think someone changed these names recently because I actually changed the second to the first after the update.
But it is possible I messed up, I don't know...

[Nirvana Coppola]

I'm confused. It compiled till the other day, today I updated mathlib and it didn't anymore, because it wanted these other names :|

[Riccardo Brasca]

The names changed in mathlib, it's not at all strange

[Riccardo Brasca]

Mathlib changes like 20 times a day, with additions but also with modifications

[Fabrizio Barroero]

but does one have to update it manually?

[Riccardo Brasca]

Yes

[Nirvana Coppola]

That's fair enough, what I'm surprised about is that now that I made the changes that should be consistent it broke for Fabrizio. Maybe you just have to reupdate mathlib and that's all though

[Riccardo Brasca]

Feel free to write a tool to do it automatically :sweat_smile:

[Riccardo Brasca]

There are partial tools, but atm the authors are busy on other stuff

[Nirvana Coppola]

Where "you" means "Fabrizio" :sweat_smile:

[Riccardo Brasca]

If someone (Nirvana) update mathlib, with lake update and push, the others (Fabrizio) must, after git pull do lake exe cache get and restart vs code

[Riccardo Brasca]

Note that of course the modifications to mathlib are most of the time harmless, so it's not really complicated

[Fabrizio Barroero]

I updated Mathlib. It still doesn't work for me...

[Fabrizio Barroero]

Thanks for the explanation, Riccardo

[Riccardo Brasca]

How did you update it?

[Fabrizio Barroero]

Lake update

[Riccardo Brasca]

Well, then both of you updated it, probably to different versions

[Nirvana Coppola]

D:

[Riccardo Brasca]

I guess that git pull complains about conflicts or stuff like that

[Fabrizio Barroero]

@Nirvana Coppola , if you had to uncomment import Ostrowski2024.Basic it means your Mathlib does not see what Amos PRd some weeks ago

[Riccardo Brasca]

I strongly suggest you synchronize your repositories

[Nirvana Coppola]

That's interesting.

[Riccardo Brasca]

Is the online version ok?

[Nirvana Coppola]

But it's also strange because I made the lake exe cache get before doing anything else.

[Riccardo Brasca]

I have the impression you are misunderstanding something about lake and git

[Nirvana Coppola]

This is very possible.

[Fabrizio Barroero]

This is clear... I still have so much to learn about that

[Nirvana Coppola]

But we don't even know who of us is... or maybe we both are! :sweat:

[Riccardo Brasca]

The mathlib version is written in a normal file, tracked by git

[Riccardo Brasca]

lake update changes it, and it downloads the new cache, that is a precompiled version of mathlib, and it is ignored by git

[Riccardo Brasca]

I am not at the computer right now so I cannot check it, but is the online version ok?

[Fabrizio Barroero]

I am about to get off my train right now, so I cannot check either

[Nirvana Coppola]

Riccardo Brasca said:

but is the online version ok?

At this point I would not know how to check and answer this question.

[Nirvana Coppola]

Luckily, the stuff I was supposed to PR aren't touched by this, and I'm finally done.

[Riccardo Brasca]

Ok, let me phrase the question differently: does anyone have a version you all would like to have?

[Riccardo Brasca]

Forget about mathlib errors, the point is local work done by people on their own computer and not pushed

[Nirvana Coppola]

I don't know, let's hear if the others complain. Otherwise tomorrow I'll try to figure out what's wrong with my computer.

[Riccardo Brasca]

Anyway git reset --hard makes everything like the online version. BEWARE THAT THIS DESTROYS LOCAL CHANGES

[María Inés de Frutos Fernández]

I will have a look.

[Fabrizio Barroero]

Quick recap: the version I pushed a few hours ago was working on my computer and not on Nirvana’s. She fixed it for hers and now it doesn’t work for me

[María Inés de Frutos Fernández]

Nirvana Coppola said:

The new version of mathlib messed up some imports and name of theorems we were using and I just fixed it for our repo, I think. If any of you has time, can you check it compiles?

@Nirvana Coppola , it seems that you are using an old version of Mathlib (in the latest changes you pushed, you reverted to old lemma names).
More importantly, the online repo had outdated versions of the lean-toolchain and lake-manifest.json files.
I have just pushed. Could either of you do git pull followed by lake exe cache get to confirm if it now works for you?

[Fabrizio Barroero]

I won’t be able to do it until tomorrow, but thanks

[Amos Turchet]

I tried doing that just now and got this strange GIT error

`/Users/amos/Documents/LEAN4/ostrowski2024/Ostrowski2024/Rationals.lean Init Ostrowski2024.MulRingNormRat Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Real --no-build` failed:

stderr:
error: > git rev-parse --verify HEAD    # in directory ./.lake/packages/mathlib
error: stderr:
fatal: Needed a single revision
error: external command `git` exited with code 128
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

[Amos Turchet]

Seems to be related to something other than our project:

https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/435877290

[Amos Turchet]

Also

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20error.20codes.20.28e.2Eg.2E.20code.20139.29

[Fabrizio Barroero]

I pulled what María Inés pushed, typed git reset --hard and lake exe cache get.
It works now, Thanks @María Inés de Frutos Fernández !

[Kevin Buzzard]

Just a warning that git reset --hard can make you lose local work. Would it have worked if you didn't type that?

[Amos Turchet]

Without the git reset --hard I got the error above (ie I only didgit pull followed by lake exe cache get)

[Fabrizio Barroero]

Sorry, I typed git reset —hard because vs code wasn’t letting me pull María Inés’ version.

[Fabrizio Barroero]

So, I did that before pulling, not after as I wrote above

[Fabrizio Barroero]

Amos Turchet said:

Without the git reset --hard I got the error above (ie I only didgit pull followed by lake exe cache get)

Does it work for you now?

[Kevin Buzzard]

Ok just as long as everyone is aware that git reset --hard means something like "delete all commits I made which I didn't push" and in particular it means "possibly delete some of my stuff"

[Fabrizio Barroero]

Yes yes, I learnt it the hard way some time ago… :sweat_smile:thanks!

[Nirvana Coppola]

María Inés de Frutos Fernández said:

Nirvana Coppola said:

The new version of mathlib messed up some imports and name of theorems we were using and I just fixed it for our repo, I think. If any of you has time, can you check it compiles?

Nirvana Coppola , it seems that you are using an old version of Mathlib (in the latest changes you pushed, you reverted to old lemma names).
More importantly, the online repo had outdated versions of the lean-toolchain and lake-manifest.json files.
I have just pushed. Could either of you do git pull followed by lake exe cache get to confirm if it now works for you?

This worked for me, thanks!

[Nirvana Coppola]

Question about the PR: the lint check failed (because I didn't think about it). Do I have to do something or just wait?

[Riccardo Brasca]

Which PR?

[Nirvana Coppola]

#87937 (I d'on't know how to make the short link, sorry)

[Riccardo Brasca]

The number does not exist... it is enough to write # 12345, without the space

[Riccardo Brasca]

Is it #12517?

[Nirvana Coppola]

Ah sorry, don't know where I found that, yes, it's correct

[Riccardo Brasca]

The linter is complaining that there lines with more than 100 characters, for example line 402. It is enough to go to a newline just before the last word. Note that in VSCode you have a vertical bar at the 100th character, nothing should be longer than that line.

[Riccardo Brasca]

Also, don't forget to mark the PR "awaiting review", otherwise nobody will have a look at it.

[Riccardo Brasca]

In the PR description you can use #backticks as in Zulip.

[Amos Turchet]

No i still get the message

error: > git rev-parse --verify HEAD    # in directory ./.lake/packages/mathlib
error: stderr:
fatal: Needed a single revision
error: external command `git` exited with code 128
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

[Riccardo Brasca]

If you only want the exact version online you can just reclone the whole repo.

[Jiale Miao]

Hello everyone, I just formalized Ostrowski's theorem in Lean4 as a part of my project in the formalizing course following my old lean3 code lead by Maria, you can check it here: https://github.com/Biiiilly/ostrowski_project. Is there anything I can help with it here?

[Fabrizio Barroero]

Jiale Miao said:

Hello everyone, I just formalized Ostrowski's theorem in Lean4 as a part of my project in the formalizing course following my old lean3 code lead by Maria, you can check it here: https://github.com/Biiiilly/ostrowski_project. Is there anything I can help with it here?

Hi! You could help by reviewing our PRs. We have been waiting for a while for #12517 to be merged (anybody knows what's going on with that?) and we are ready to open more.
After that we could start with Ostrowski for number fields. If you are interested and the rest of the team agrees, you can join the project.

[Antoine Chambert-Loir]

I believe you should open a full string of PRs that leads to the final statement, that would help evaluate the individual steps. The content of the present one doesn't look so useful once one will have Ostrowski.

[María Inés de Frutos Fernández]

I added some review comments to #12517. As Antoine said, you could start opening PRs for the rest of the proof without waiting for this one to be merged.

[Nirvana Coppola]

Hi, thanks Maria and Antoine. I just implemented Maria's suggestions, hoping I didn't mess anything up!

[Nirvana Coppola]

Hi everyone, hope you are doing well! I pushed a header to the new file (thanks @Fabrizio Barroero ), but since I've never written one I'd appreciate feedback, just so I know we didn't write anything inappropriate. Secondly, there is now a new error about the imports: what's to be done to fix it? :)

[María Inés de Frutos Fernández]

Hi Nirvana! The error is that you added a new file (Mathlib/NumberTheory/Ostrowski.lean), but you have not added it as an import to the file Mathlib.lean.

[Riccardo Brasca]

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

does it automatically

[Nirvana Coppola]

Thanks!!

[María Inés de Frutos Fernández]

Congrats on getting #12517 merged! What's next? :smile:

[Fabrizio Barroero]

I think we could start with the non-Archimedean part. If it’s ok with everyone I’m gonna do it, hopefully I can do it by the end of the week. Should I just make a PR with the whole non-arch case? It’s about 200 lines

[María Inés de Frutos Fernández]

200 lines should be fine.

[Fabrizio Barroero]

We have a PR with the non-archimedean case of Ostrowski's Theorem.
It can be found here #14026.

[Nirvana Coppola]

Wow, that was fast! :D

[Kevin Buzzard]

It helps if you have a maintainer who (a) was not involved with writing the code and (b) is definitely interested in the material :-)

[Fabrizio Barroero]

Many thanks to @Michael Stoll for the review and to @Riccardo Brasca for the suggestion to add the uniqueness of the prime p in the statement and for the final approval!

[Yakov Pechersky]

Will the infinity/Archimedean case be added as well?

[Fabrizio Barroero]

Yes, we have a proof, but there’s still some work to do on it

[Amos Turchet]

Dear all, maybe it's time to push the first step of the Archimedean part. If you want I can do it (with the help of @Fabrizio Barroero ) and start the PR

[María Inés de Frutos Fernández]

Sounds good!

[Amos Turchet]

PR with the first step of the Archimedean is here ##14442

[Amos Turchet]

for some reason i got the "new-contributor" tag at the second PR :grinning:

[Fabrizio Barroero]

Amos Turchet said:

for some reason i got the "new-contributor" tag at the second PR :grinning:

You get it for the first 5 PRs

[Amos Turchet]

Fabrizio Barroero said:
You get it for the first 5 PRs

Ah it makes sense

[Nirvana Coppola]

I think you have to add the "awaiting review" label :)

[Riccardo Brasca]

Not important, but in github if you write ```lean ...``` you get the right colors.

[Riccardo Brasca]

I mean this difference

lemma one_lt_of_not_bounded (notbdd : ¬ ∀ (n : ℕ), f n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) : 1 < f n₀

lemma one_lt_of_not_bounded (notbdd : ¬ ∀ (n : ℕ), f n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) : 1 < f n₀

[Fabrizio Barroero]

Hi everyone, I thought we could start looking at the number field case so I started with some small stuff.
I just pushed a file in the project with a definition mulRingNorm_arch of an Archimedean absolute value attached to a complex embedding.
I included the definition of the restriction of a 'mulRingNorm' to a subfield, since we need to use Ostrowski for the rationals to prove the general case.
There are also a couple of trivial lemmas which might be useful.

Now, for the Archimedean case, I believe one needs to speak about completions. Should we use CauSeq.Completion.Cauchy? Or are there complete fields in Mathlib?

I have also tried to define P-adic MulRingNormsfor a non-zero prime ideal P but I failed. I tried with IsDedekindDomain.HeightOneSpectrum.valuation but this gives a WithZero (Multiplicative ℤ). How does one get a real number out of it? Is this the right def to use?

I guess we need your help @María Inés de Frutos Fernández ... :pray:

[Yakov Pechersky]

There are also docs#UniformSpace.Completion and docs#AbstractCompletion. AFAIU CauSeq is an "implementation detail" in how the reals and Q_p are set up.

[Yakov Pechersky]

Regarding the WithZero (Multiplicative Z), there is docs#Valued.norm which is used in docs#Valued.toNormedField, which takes care of creating the function into reals. Looks like it uses a docs#Valuation.RankOne directly

[Fabrizio Barroero]

Thanks!

[Kevin Buzzard]

@Dawid Lipinski has the monoid hom from Z_{m0} to R_{>=0} sending 1 to r for any positive real r.

[Kevin Buzzard]

Borrowing from his repo:

import Mathlib.RingTheory.Valuation.Basic
import Mathlib.RingTheory.DedekindDomain.AdicValuation
import Mathlib.Analysis.SpecialFunctions.Pow.NNReal

open scoped DiscreteValuation

open Multiplicative DiscreteValuation

@[elab_as_elim]
protected lemma Zm0.induction_on {motive : ℤₘ₀ → Prop} (zero : motive 0)
  (of_int : ∀ z : ℤ, motive (ofAdd z : Multiplicative ℤ)) (x : ℤₘ₀) : motive x :=
WithZero.recZeroCoe zero of_int x

noncomputable def Zm0.toFun (r : ℝ) (x : ℤₘ₀) : ℝ := WithZero.recZeroCoe 0 (fun z : Multiplicative ℤ ↦ r ^ (toAdd z)) x

variable (r : ℝ)

lemma Zm0.toFun_zero :Zm0.toFun r 0 = 0 := rfl

lemma Zm0.toFun_coe_int (z : ℤ) :Zm0.toFun r (ofAdd z : Multiplicative ℤ) = r ^ z := rfl

lemma Zm0.toFun_coe_mult_int (z : Multiplicative ℤ) :Zm0.toFun r z = r ^ (toAdd z) := rfl

noncomputable def Zm0.toReal (r : ℝ) (h1: 0 < r) : ℤₘ₀ →* ℝ where
  toFun := Zm0.toFun r
  map_one' := by
    suffices toFun r 1 = r ^ 0 by
      convert this
    exact Zm0.toFun_coe_int r 0
  map_mul' := by
    intro x y
    simp only
    induction' x using Zm0.induction_on with x
    · simp only [Zm0.toFun_zero, zero_mul]
    · induction' y using Zm0.induction_on with y
      · simp only [Zm0.toFun_zero, mul_zero]
      · norm_cast
        simp only [toFun_coe_mult_int, toAdd_mul, toAdd_ofAdd]
        have h2: r ^ ((x : ℝ) + (y : ℝ)) = r ^ x * r ^ y := by
          rw [Real.rpow_add h1 x y]
          simp only [Real.rpow_intCast]
        rw [← h2]
        norm_cast

[Fabrizio Barroero]

Kevin Buzzard said:

Dawid Lipinski has the monoid hom from Z_{m0} to R_{>=0} sending 1 to r for any positive real r.

That's what I was looking for! Many many thanks!

[María Inés de Frutos Fernández]

Kevin Buzzard said:

Dawid Lipinski has the monoid hom from Z_{m0} to R_{>=0} sending 1 to r for any positive real r.

@Filippo A. E. Nuccio and I also have this function (although we put NNReal as the codomain; see withZeroMultIntToNNReal). We also prove in that file that this is a StrictMono when 1 < e, which you will probably need at some point.

[María Inés de Frutos Fernández]

Fabrizio Barroero said:

Hi everyone, I thought we could start looking at the number field case so I started with some small stuff.

That's great! If you haven't seen it, I suggest that you also have a look at the file Mathlib.NumberTheory.NumberField.Embeddings.

[Fabrizio Barroero]

María Inés de Frutos Fernández said:

Kevin Buzzard said:

Dawid Lipinski has the monoid hom from Z_{m0} to R_{>=0} sending 1 to r for any positive real r.

Filippo A. E. Nuccio and I also have this function (although we put NNReal as the codomain; see withZeroMultIntToNNReal). We also prove in that file that this is a StrictMono when 1 < e, which you will probably need at some point.

Very nice! Is this going to Mathlib soon?

[Fabrizio Barroero]

María Inés de Frutos Fernández said:

Fabrizio Barroero said:

Hi everyone, I thought we could start looking at the number field case so I started with some small stuff.

That's great! If you haven't seen it, I suggest that you also have a look at the file Mathlib.NumberTheory.NumberField.Embeddings.

Yes, that's probably going to be useful. Thanks!

[Fabrizio Barroero]

Hi everyone, I made some progress on the nonArchimedean case but there is quite a bit of work still to do. I left a couple of simple and hopefully simple sorries to get rid of.

[Yakov Pechersky]

nonarch_iff_bdd is proven in my #15077

[Yakov Pechersky]

isUltrametricDist_of_forall_norm_natCast_le_one

[Fabrizio Barroero]

I continued working on the nonArchimedean case. There are quite a few sorries left, but most of them should not be too hard. I think the only serious one is the following

exists_num_denom_MulRingNorm_one {K : Type u_2} [Field K] [nf : NumberField K]
  (P : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) (α : K) (h_nezero : α ≠ 0) (h_abs : (mulRingNorm_Padic P) α ≤ 1) :
 ∃ x y : 𝓞 K, α = x / y ∧ mulRingNorm_Padic P y = 1

Conrad uses class groups but maybe one can avoid that using norms...

[Fabrizio Barroero]

Concerning the archimedean case I just stumbled upon #16483... This looks pretty useful...

[Fabrizio Barroero]

Ostrowski's Theorem for the rationals is now on Mathlib!
:tada:

Back to work on the number field case!

[Johan Commelin]

Congratulations!

[María Inés de Frutos Fernández]

Congrats! :tada: