Documentation

Mathlib.NumberTheory.Ostrowski

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 #

TODO #

Extend to arbitrary number fields.

References #

Tags #

absolute value, Ostrowski's theorem

Preliminary lemmas #

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

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.

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

Equations
Instances For
    @[simp]
    theorem Rat.AbsoluteValue.padic_eq_padicNorm (p : ) [Fact (Nat.Prime p)] (r : ) :
    (padic p) r = (padicNorm p r)
    theorem Rat.AbsoluteValue.padic_le_one (p : ) [Fact (Nat.Prime p)] (n : ) :
    (padic p) n 1
    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 < 1p m

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

    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 < 1p m) :

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

    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 < 1p m) {m : } (hpm : ¬p m) :

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

    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 < 1p m) :
    ∃ (t : ), 0 < t f p = p ^ (-t)

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

    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 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.

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      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.

      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

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

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

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

      The main result #

      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.

      The standard absolute value on is not equivalent to any p-adic absolute value.