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

• mulRingNorm_equiv_standard_or_padic: given an absolute value on ℚ, it is equivalent to the standard Archimedean (Euclidean) absolute value or to a p-adic absolute value for some 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

ring norm, ostrowski

theorem Rat.MulRingNorm.eq_on_nat_iff_eq_on_Int {f g : MulRingNorm ℚ} : (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n

Values of a multiplicative norm of the rationals coincide on ℕ if and only if they coincide on ℤ.

theorem Rat.MulRingNorm.eq_on_nat_iff_eq {f g : MulRingNorm ℚ} : (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Values of a multiplicative norm of the rationals are determined by the values on the natural numbers.

theorem Rat.MulRingNorm.equiv_on_nat_iff_equiv {f g : MulRingNorm ℚ} : (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.equiv g

The equivalence class of a multiplicative norm on the rationals is determined by its values on the natural numbers.

Non-archimedean case

Every bounded absolute value is equivalent to a p-adic absolute value

def Rat.MulRingNorm.mulRingNorm_padic (p : ℕ) [Fact (Nat.Prime p)] : MulRingNorm ℚ

The mulRingNorm corresponding to the p-adic norm on ℚ.

Equations

• Rat.MulRingNorm.mulRingNorm_padic p = { toFun := fun (x : ℚ) => ↑(padicNorm p x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }

@[simp]

theorem Rat.MulRingNorm.mulRingNorm_eq_padic_norm (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) : (Rat.MulRingNorm.mulRingNorm_padic p) r = ↑(padicNorm p r)

theorem Rat.MulRingNorm.exists_minimal_nat_zero_lt_mulRingNorm_lt_one {f : MulRingNorm ℚ} (hf_nontriv : f ≠ 1) (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.

theorem Rat.MulRingNorm.is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one {f : MulRingNorm ℚ} {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.

theorem Rat.MulRingNorm.mulRingNorm_eq_one_of_not_dvd {f : MulRingNorm ℚ} (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 divible by p has absolute value 1.

theorem Rat.MulRingNorm.exists_pos_mulRingNorm_eq_pow_neg {f : MulRingNorm ℚ} {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.

theorem Rat.MulRingNorm.mulRingNorm_equiv_padic_of_bounded {f : MulRingNorm ℚ} (hf_nontriv : f ≠ 1) (bdd : ∀ (n : ℕ), f ↑n ≤ 1) : ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.equiv (Rat.MulRingNorm.mulRingNorm_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 is equivalent to the standard absolute value

def Rat.MulRingNorm.mulRingNorm_real : MulRingNorm ℚ

The usual absolute value on ℚ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rat.MulRingNorm.mul_ring_norm_eq_abs (r : ℚ) : Rat.MulRingNorm.mulRingNorm_real r = ↑|r|

theorem Rat.MulRingNorm.mulRingNorm_apply_le_sum_digits {f : MulRingNorm ℚ} (n : ℕ) {m : ℕ} (hm : 1 < m) : f ↑n ≤ (List.mapIdx (fun (i x : ℕ) => ↑m * f ↑m ^ i) (m.digits n)).sum

Given an two integers n, m with m > 1 the mulRingNorm 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.

theorem Rat.MulRingNorm.one_lt_of_not_bounded {f : MulRingNorm ℚ} (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

theorem Rat.MulRingNorm.mulRingNorm_le_mulRingNorm_pow_log {f : MulRingNorm ℚ} {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.

theorem Rat.MulRingNorm.le_of_mulRingNorm_eq {f : MulRingNorm ℚ} {m n : ℕ} (hm : 1 < m) (hn : 1 < n) (notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1) {s t : ℝ} (hfm : f ↑m = ↑m ^ s) (hfn : f ↑n = ↑n ^ t) : t ≤ s

Given m,n ≥ 2 and f m = m ^ s, f n = n ^ t for s, t > 0, we have t ≤ s.

theorem Rat.MulRingNorm.mulRingNorm_equiv_standard_of_unbounded {f : MulRingNorm ℚ} (notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1) : f.equiv Rat.MulRingNorm.mulRingNorm_real

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

theorem Rat.MulRingNorm.mulRingNorm_equiv_standard_or_padic (f : MulRingNorm ℚ) (hf_nontriv : f ≠ 1) : f.equiv Rat.MulRingNorm.mulRingNorm_real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.equiv (Rat.MulRingNorm.mulRingNorm_padic p)

Ostrowski's Theorem