[Merged by Bors] - Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem

Mathlib/NumberTheory/Ostrowski.lean

@@ -7,8 +7,10 @@ Francesco Veneziano
 -/
 
 import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.Analysis.SpecialFunctions.Log.Base
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.Normed.Ring.Seminorm
+import Mathlib.NumberTheory.Padics.PadicNorm
 
 /-!
 # Ostrowski’s Theorem
@@ -55,4 +57,163 @@ lemma equiv_on_Nat_iff_equiv : (∃ c : ℝ, 0 < c ∧ (∀ n : ℕ , (f n)^c =
       (apply_nonneg f _), h x.den, ← MulRingNorm.apply_natAbs_eq,← MulRingNorm.apply_natAbs_eq,
       h (natAbs x.num)]
 
+/-!
+Throughout this file, `f` is an arbitrary absolute value.
+-/
+variable {f : MulRingNorm ℚ}
+
+open Rat.MulRingNorm
+
+section Non_archimedean
+
+-- ## Non-archimedean case
+
+/-- The mulRingNorm corresponding to the p-adic norm on ℚ. -/
+def mulRingNorm_padic (p : ℕ) [Fact p.Prime] : MulRingNorm ℚ :=
+{ toFun     := fun x : ℚ ↦ (padicNorm p x : ℝ),
+  map_zero' := by simp only [padicNorm.zero, Rat.cast_zero]
+  add_le'   := by simp only; norm_cast; exact fun r s ↦ padicNorm.triangle_ineq r s
+  neg'      := by simp only [forall_const, padicNorm.neg];
+  eq_zero_of_map_eq_zero' := by
+    simp only [Rat.cast_eq_zero]
+    apply padicNorm.zero_of_padicNorm_eq_zero
+  map_one' := by simp only [ne_eq, one_ne_zero, not_false_eq_true, padicNorm.eq_zpow_of_nonzero,
+    padicValRat.one, neg_zero, zpow_zero, Rat.cast_one]
+  map_mul' := by simp only [padicNorm.mul, Rat.cast_mul, forall_const]
+}
+
+@[simp] lemma mulRingNorm_eq_padic_norm (p : ℕ) [Fact (Nat.Prime p)] (r : ℚ) :
+  mulRingNorm_padic p r = padicNorm p r := rfl
+
+-- ## Step 1: define `p = smallest n s. t. 0 < |n| < 1`
+
+variable (hf_nontriv : f ≠ 1) (bdd : ∀ n : ℕ, f n ≤ 1)
+
+/-- There exists a minimal positive integer with absolute value smaller than 1. -/
+lemma exists_minimal_nat_zero_lt_mulRingNorm_lt_one : ∃ p : ℕ, (0 < f p ∧ f p < 1) ∧
+    ∀ m : ℕ, 0 < f m ∧ f m < 1 → p ≤ m := by
+  -- There is a positive integer with absolute value different from one.
+  obtain ⟨n, hn1, hn2⟩ : ∃ n : ℕ, n ≠ 0 ∧ f n ≠ 1 := by
+    contrapose! hf_nontriv
+    rw [← eq_on_Nat_iff_eq]
+    intro n
+    rcases eq_or_ne n 0 with rfl | hn0
+    · simp only [Nat.cast_zero, map_zero]
+    · simp only [MulRingNorm.apply_one, Nat.cast_eq_zero, hn0, ↓reduceIte, hf_nontriv n hn0]
+  set P := {m : ℕ | 0 < f ↑m ∧ f ↑m < 1} -- p is going to be the minimum of this set.
+  have hP : P.Nonempty :=
+    ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩
+  exact ⟨sInf P, Nat.sInf_mem hP, fun m hm ↦ Nat.sInf_le hm⟩
+
+-- ## Step 2: p is prime
+
+variable (p : ℕ) (hp0 : 0 < f p) (hp1 : f p < 1) (hmin : ∀ m : ℕ, 0 < f m ∧ f m < 1 → p ≤ m)
+
+ /-- The minimal positive integer with absolute value smaller than 1 is a prime number.-/
+lemma is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one : p.Prime := by
+  rw [← Nat.irreducible_iff_nat_prime]
+  constructor -- Two goals: p is not a unit and any product giving p must contain a unit.
+  · rw [Nat.isUnit_iff]
+    rintro rfl
+    simp only [Nat.cast_one, map_one, lt_self_iff_false] at hp1
+  · rintro a b rfl
+    rw [Nat.isUnit_iff, Nat.isUnit_iff]
+    by_contra! con
+    obtain ⟨ha₁, hb₁⟩ := con
+    obtain ⟨ha₀, hb₀⟩ : a ≠ 0 ∧ b ≠ 0 := by
+      refine mul_ne_zero_iff.1 fun h ↦ ?_
+      rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
+    have hap : a < a * b := lt_mul_of_one_lt_right (by omega) (by omega)
+    have hbp : b < a * b := lt_mul_of_one_lt_left (by omega) (by omega)
+    have ha :=
+      le_of_not_lt <| not_and.1 ((hmin a).mt hap.not_le) (map_pos_of_ne_zero f (mod_cast ha₀))
+    have hb :=
+      le_of_not_lt <| not_and.1 ((hmin b).mt hbp.not_le) (map_pos_of_ne_zero f (mod_cast hb₀))
+    rw [Nat.cast_mul, map_mul] at hp1
+    exact ((one_le_mul_of_one_le_of_one_le ha hb).trans_lt hp1).false
+
+-- ## Step 3: if p does not divide m, then |m|=1
+
+open Real
+
+/-- A natural number not divible by `p` has absolute value 1. -/
+lemma mulRingNorm_eq_one_of_not_dvd {m : ℕ} (hpm : ¬ p ∣ m) : f m = 1 := by
+  apply le_antisymm (bdd m)
+  by_contra! hm
+  set M := f p ⊔ f m with hM
+  set k := Nat.ceil (M.logb (1 / 2)) + 1 with hk
+  obtain ⟨a, b, bezout⟩ : IsCoprime (p ^ k : ℤ) (m ^ k) := by
+    apply IsCoprime.pow (Nat.Coprime.isCoprime _)
+    exact (Nat.Prime.coprime_iff_not_dvd
+      (is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one p hp0 hp1 hmin)).2 hpm
+  have le_half {x} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M) : x ^ k < 1 / 2 := by
+    calc
+    x ^ k = x ^ (k : ℝ) := (rpow_natCast x k).symm
+    _ < x ^ M.logb (1 / 2) := by
+      apply rpow_lt_rpow_of_exponent_gt hx0 hx1
+      rw [hk]
+      push_cast
+      exact lt_add_of_le_of_pos (Nat.le_ceil (M.logb (1 / 2))) zero_lt_one
+    _ ≤ x ^ x.logb (1 / 2) := by
+      apply rpow_le_rpow_of_exponent_ge hx0 (le_of_lt hx1)
+      simp only [one_div, ← log_div_log, Real.log_inv, neg_div, ← div_neg, hM]
+      gcongr
+      simp only [Left.neg_pos_iff]
+      exact log_neg (lt_sup_iff.2 <| Or.inl hp0) (sup_lt_iff.2 ⟨hp1, hm⟩)
+    _ = 1 / 2 := rpow_logb hx0 (ne_of_lt hx1) one_half_pos
+  apply lt_irrefl (1 : ℝ)
+  calc
+  1 = f 1 := (map_one f).symm
+  _ = f (a * p ^ k + b * m ^ k) := by rw_mod_cast [bezout]; norm_cast
+  _ ≤ f (a * p ^ k) + f (b * m ^ k) := f.add_le' (a * p ^ k) (b * m ^ k)
+  _ ≤ 1 * (f p) ^ k + 1 * (f m) ^ k := by
+    simp only [map_mul, map_pow, le_refl]
+    gcongr
+    all_goals rw [← MulRingNorm.apply_natAbs_eq]; apply bdd
+  _ = (f p) ^ k + (f m) ^ k := by simp only [one_mul]
+  _ < 1 := by
+    have hm₀ : 0 < f m :=
+      map_pos_of_ne_zero _ <| Nat.cast_ne_zero.2 fun H ↦ hpm <| H ▸ dvd_zero p
+    linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
+
+-- ## Step 4: |p| = p ^ (- t) for some positive real t
+
+/-- The absolute value of `p` is `p ^ (-t)` for some positive real number `t`. -/
+lemma exists_pos_mulRingNorm_eq_pow_neg : ∃ t : ℝ, 0 < t ∧ f p = p ^ (-t) := by
+  have pprime := is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one p hp0 hp1 hmin
+  refine ⟨- logb p (f p), Left.neg_pos_iff.2 <| logb_neg (mod_cast pprime.one_lt) hp0 hp1, ?_⟩
+  rw [neg_neg]
+  refine (rpow_logb (mod_cast pprime.pos) ?_ hp0).symm
+  simp only [ne_eq, Nat.cast_eq_one,Nat.Prime.ne_one pprime, not_false_eq_true]
+
+-- ## Non-archimedean case: end goal
+/--
+  If `f` is bounded and not trivial, then it is equivalent to a p-adic absolute value.
+-/
+theorem mulRingNorm_equiv_padic_of_bounded :
+    ∃ p, ∃ (hp : Fact (p.Prime)), MulRingNorm.equiv f (mulRingNorm_padic p) := by
+  obtain ⟨p, hfp, hmin⟩ := exists_minimal_nat_zero_lt_mulRingNorm_lt_one hf_nontriv bdd
+  have hprime := is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one p hfp.1 hfp.2 hmin
+  have hprime_fact : Fact (p.Prime) := ⟨hprime⟩
+  use p, hprime_fact
+  obtain ⟨t, h⟩ := exists_pos_mulRingNorm_eq_pow_neg p hfp.1 hfp.2 hmin
+  rw [← equiv_on_Nat_iff_equiv]
+  refine ⟨t⁻¹, by simp only [inv_pos, h.1], fun n ↦ ?_⟩
+  have ht : t⁻¹ ≠ 0 := inv_ne_zero h.1.ne'
+  rcases eq_or_ne n 0 with rfl | hn -- Separate cases n=0 and n ≠ 0
+  · simp only [Nat.cast_zero, map_zero, ne_eq, ht, not_false_eq_true, zero_rpow]
+  · /- Any natural number can be written as a power of p times a natural number not divisible
+    by p  -/
+    rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hprime.ne_one with ⟨e, m, hpm, rfl⟩
+    simp only [Nat.cast_mul, Nat.cast_pow, map_mul, map_pow, mulRingNorm_eq_padic_norm,
+      padicNorm.padicNorm_p_of_prime, Rat.cast_inv, Rat.cast_natCast, inv_pow,
+      mulRingNorm_eq_one_of_not_dvd bdd p hfp.1 hfp.2 hmin hpm, h.2]
+    rw [← padicNorm.nat_eq_one_iff] at hpm
+    simp only [← rpow_natCast, p.cast_nonneg, ← rpow_mul, mul_one, ← rpow_neg, hpm, cast_one]
+    congr
+    field_simp [h.1.ne']
+    ring
+
+end Non_archimedean
+
 end Rat.MulRingNorm