Ostrowski’s Theorem #

Ostrowski's Theorem for the field ℚ: every absolute value on ℚ is equivalent to either a p-adic absolute value or to the standard Archimedean (Euclidean) absolute value.

Main results #

Rat.AbsoluteValue.equiv_real_or_padic: given an absolute value on ℚ, it is equivalent to the standard Archimedean (Euclidean) absolute value Rat.AbsoluteValue.real or to a p-adic absolute value Rat.AbsoluteValue.padic p for a unique prime number p.

TODO #

Extend to arbitrary number fields.

References #

[K. Conrad, Ostrowski's Theorem for Q][conradQ]
[K. Conrad, Ostrowski for number fields][conradnumbfield]
[J. W. S. Cassels, Local fields][cassels1986local]

Tags #

absolute value, Ostrowski's theorem

Preliminary lemmas #

source

📐 coverage

theorem Rat.AbsoluteValue.eq_on_nat_iff_eq {f g : AbsoluteValue ℚ ℝ} :

(∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Values of an absolute value on the rationals are determined by the values on the natural numbers.

source

📐 coverage

theorem Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv {f g : AbsoluteValue ℚ ℝ} :

(∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.IsEquiv g

The equivalence class of an absolute value on the rationals is determined by its values on the natural numbers.

source

📐 coverage

@[deprecated Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv (since := "2025-09-12")]

theorem Rat.AbsoluteValue.equiv_on_nat_iff_equiv {f g : AbsoluteValue ℚ ℝ} :

(∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.IsEquiv g

Alias of Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv.

The equivalence class of an absolute value on the rationals is determined by its values on the natural numbers.

The non-archimedean case #

Every bounded absolute value on ℚ is equivalent to a p-adic absolute value.

source

🔸 coverage

def Rat.AbsoluteValue.padic (p : ℕ) [Fact (Nat.Prime p)] :

AbsoluteValue ℚ ℝ

The real-valued AbsoluteValue corresponding to the p-adic norm on ℚ.

Equations

Instances For

source

📐 coverage

@[simp]

theorem Rat.AbsoluteValue.padic_eq_padicNorm (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) :

(padic p) r = ↑(padicNorm p r)

source

📐 coverage

theorem Rat.AbsoluteValue.padic_le_one (p : ℕ) [Fact (Nat.Prime p)] (n : ℤ) :

(padic p) ↑n ≤ 1

source

📐 coverage

theorem Rat.AbsoluteValue.exists_minimal_nat_zero_lt_and_lt_one {f : AbsoluteValue ℚ ℝ} (hf_nontriv : f.IsNontrivial) (bdd : ∀ (n : ℕ), f ↑n ≤ 1) :

∃ (p : ℕ), (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

There exists a minimal positive integer with absolute value smaller than 1.

source

📐 coverage

theorem Rat.AbsoluteValue.is_prime_of_minimal_nat_zero_lt_and_lt_one {f : AbsoluteValue ℚ ℝ} {p : ℕ} (hp0 : 0 < f ↑p) (hp1 : f ↑p < 1) (hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) :

Nat.Prime p

The minimal positive integer with absolute value smaller than 1 is a prime number.

source

theorem Rat.AbsoluteValue.eq_one_of_not_dvd {f : AbsoluteValue ℚ ℝ} (bdd : ∀ (n : ℕ), f ↑n ≤ 1) {p : ℕ} (hp0 : 0 < f ↑p) (hp1 : f ↑p < 1) (hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) {m : ℕ} (hpm : ¬p ∣ m) :

f ↑m = 1

A natural number not divisible by p has absolute value 1.

source

📐 coverage

theorem Rat.AbsoluteValue.exists_pos_eq_pow_neg {f : AbsoluteValue ℚ ℝ} {p : ℕ} (hp0 : 0 < f ↑p) (hp1 : f ↑p < 1) (hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) :

∃ (t : ℝ), 0 < t ∧ f ↑p = ↑p ^ (-t)

The absolute value of p is p ^ (-t) for some positive real number t.

source

📐 coverage

theorem Rat.AbsoluteValue.equiv_padic_of_bounded {f : AbsoluteValue ℚ ℝ} (hf_nontriv : f.IsNontrivial) (bdd : ∀ (n : ℕ), f ↑n ≤ 1) :

∃! p : ℕ , ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)

If f is bounded and not trivial, then it is equivalent to a p-adic absolute value.

Archimedean case #

Every unbounded absolute value on ℚ is equivalent to the standard absolute value.

source

🔸 coverage

def Rat.AbsoluteValue.real :

AbsoluteValue ℚ ℝ

The standard absolute value on ℚ. We name it real because it corresponds to the unique real place of ℚ.

Equations

Instances For

source

📐 coverage

@[simp]

theorem Rat.AbsoluteValue.real_eq_abs (r : ℚ) :

real r = ↑|r|

source

📐 coverage

theorem Rat.AbsoluteValue.apply_le_sum_digits {f : AbsoluteValue ℚ ℝ} (n : ℕ) {m : ℕ} (hm : 1 < m) :

f ↑n ≤ (List.mapIdx (fun (i x : ℕ) => ↑m * f ↑m ^ i) (m.digits n)).sum

Given any two integers n, m with m > 1, the absolute value of n is bounded by m + m * f m + m * (f m) ^ 2 + ... + m * (f m) ^ d where d is the number of digits of the expansion of n in base m.

source

📐 coverage

theorem Rat.AbsoluteValue.one_lt_of_not_bounded {f : AbsoluteValue ℚ ℝ} (notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) :

1 < f ↑n₀

If f n > 1 for some n then f n > 1 for all n ≥ 2

source

📐 coverage

theorem Rat.AbsoluteValue.le_pow_log {f : AbsoluteValue ℚ ℝ} {m n : ℕ} (hm : 1 < m) (hn : 1 < n) (notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1) :

f ↑n ≤ f ↑m ^ Real.logb ↑m ↑n

Given two natural numbers n, m greater than 1 we have f n ≤ f m ^ logb m n.

source

📐 coverage

theorem Rat.AbsoluteValue.equiv_real_of_unbounded {f : AbsoluteValue ℚ ℝ} (notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1) :

f.IsEquiv real

If f is not bounded and not trivial, then it is equivalent to the standard absolute value on ℚ.

The main result #

source

📐 coverage

theorem Rat.AbsoluteValue.equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) :

f ≈ real ∨ ∃! p : ℕ , ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Ostrowski's Theorem: every absolute value (with values in ℝ) on ℚ is equivalent to either the standard absolute value or a p-adic absolute value for a prime p.

source

📐 coverage