Commit 2024-10-15 22:29 1fdea42e

feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem (#14442) 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
• 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) #17138 completes the proof of the theorem