feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem

[amosturchet]

This proves the first step of the proof of the Archimedean case of Ostrowski's Theorem, namely that a rational absolute value f : MulRingNorm ℚ that is not bounded, i.e. such that, evaluated at an integer n, it attains a value greater than one, then f n is always greater than one, whenever 1<n.

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

Include also

• preliminary lemmas on limits of functions with natural inputs
• lemma on Nat.log less or equal than Real.log
• technical lemma on an inequality between an integer and an expression involving MulRingNorm and the number of digits of its expansion in an integer base
• triangle inequality for lists (added in the file RingSeminorm.lean)

Co-authored-by:

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

---

[github-actions[bot]]

PR summary d4d83120db

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Ostrowski	1414	1417	+3 (+0.21%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.Ostrowski	3

---

Declarations diff

+ mulRingNorm_apply_le_sum_digits + mulRingNorm_sum_le_sum_mulRingNorm + one_lt_of_not_bounded

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

The doc-module for script/declarations_diff.sh contains some details about this script.

[erdOne]

What is the status of this PR? It seems to me that you might have forgot to push your commit.

[amosturchet]

What is the status of this PR? It seems to me that you might have forgot to push your commit.

sorry forgot to push, you're right

[amosturchet]

As for @erdOne suggestion to move the "preliminary lemmas": there are some natural folders in Mathlib where they might go but it's unclear to me whether we want to clog the limits section with these.

One solution would be to write a meta-lemma like this one (thanks to @fbarroero): theorem aux {l: Filter ℝ} {f : ℝ → ℝ} {g: ℕ → ℝ} (hg: ∀ᶠ n in atTop, g n = f n) (hl : Filter.Tendsto f Filter.atTop l) : Filter.Tendsto g Filter.atTop l := by sorry

would that make sense?

[erdOne]

I think that is exactly Filter.Tendsto.congr'

[amosturchet]

I think that is exactly Filter.Tendsto.congr'

Thanks! it seems to me that Filter.Tendsto.cong' requires the two functions to have the same domain though

[fbarroero]

I have a more general version of the above theorem aux like this

theorem aux' {α : Type*} [Nonempty α] [LinearOrder α] {l : Filter ℝ} {f : ℝ → ℝ} {g : α → ℝ}
    {c : α → ℝ} (hc₀ : Monotone c) (hc : ∀ x : ℝ, ∃ a : α, x ≤ c a)
    (hg : ∀ᶠ n in atTop, g n = f (c n)) (hl : Filter.Tendsto f Filter.atTop l) :
    Filter.Tendsto g Filter.atTop l

Would this make it more interesting? This would give limits at infinity for functions with domain $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$...

[amosturchet]

As for the late commit a couple of remarks:

• the lemma about natLog vs realLog is now in Mathlib as Real.natLog_le_logb so it has been removed here
• the lemmas about the limits are now private (and use the Zulip suggestion that the coercion from Nat to Real tends to atTop along atTop)

[kbuzzard]

This PR still makes some erroneous changes (e.g. incorrectly changing -/ to --/) which need to be fixed before we can consider merging it.

Usually it's nice to have smaller PRs to review, but how far are we away from the proof of the main theorem which you want here? The lemmas introduced here currently look weird and unmotivated -- I know they're not, but they look like it because the ultimate goal is missing. If you added the full proof how long would the PR be?

[fbarroero]

This PR still makes some erroneous changes (e.g. incorrectly changing -/ to --/) which need to be fixed before we can consider merging it.

Usually it's nice to have smaller PRs to review, but how far are we away from the proof of the main theorem which you want here? The lemmas introduced here currently look weird and unmotivated -- I know they're not, but they look like it because the ultimate goal is missing. If you added the full proof how long would the PR be?

The full proof can now be found in #17138. There are 167 lines in addition to what is in this PR.

[YaelDillies]

Do you need help with merging master?

[fbarroero]

Do you need help with merging master?

Maybe, I am trying to solve it myself.. I hope I didn't make a mess. I let you know if I need help, thanks

[fbarroero]

Do you need help with merging master?

Everything should be fine now. Thanks for having offered to help!

[YaelDillies]

Are you sure? There are still 162 commits and 52 participants in this PR.

[fbarroero]

Are you sure? There are still 162 commits and 52 participants in this PR.

I am sorry. I don't know what happened earlier. I just wanted to merge master and that's what I thought I was doing in the same way I always do (pull in the master and then git merge master in the branch). I merged master again and the second time it seems it worked just fine. I guess all these 52 people are going to get automatically subscribed to this PR and I apologise for the spam. Is there a way to fix this? I would appreciate anyone's help.

[YaelDillies]

I'm going to try something. Please don't touch the branch for a few minutes

[YaelDillies]

Looks like that solved it. Please make sure you have no local changes on branch amos_ostrowski_arch, then run git reset origin/amos_ostrowski_arch --hard. ⚠️ This will lose all your local changes on this branch ⚠️

[fbarroero]

Looks like that solved it. Please make sure you have no local changes on branch amos_ostrowski_arch, then run git reset origin/amos_ostrowski_arch --hard. ⚠️ This will lose all your local changes on this branch ⚠️

I have done that. Thank you very much! And I apologise again for the mess...

[fbarroero]

@YaelDillies Thanks for the golfing! It's much cleaner now.

[YaelDillies]

Great, thanks!

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[kbuzzard]

Thanks a lot! Looking forward to the next instalment of the proof of this important and long-awaited result!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build