A new proof of a `NormedDivisionRing` is nonarch iff Nat is

Stream: mathlib4

[Jiang Jiedong]

Hi everyone,
I have formalized a proof of the statement "If $R$ is a normed division ring, then the norm on $R$ is non-archimedean if the restriction of the norm to $\mathbb{N}$ is non-archimedean." Only after I formalized the whole proof, did I realize a very similar proof is already in mathlib using IsUltrametricDist language, see IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one.

The main difference between my proof and the mathlib proof is that my proof uses a direct calculation of limit $\lim_{n \to \infty} (n + 1)^{1/n} = 1$ and the mathlib proof avoided it but using another trick based on this limit idea. So I think my proof is a little bit easier to read than the mathlib's proof.

Since it is a repeated work, I'll just post my proof here. If you think any part of the proof is useful to mathlib, please feel free to use it on your own or tell me I could PR some part of the proof!

import Mathlib

open Polynomial Filter Topology
theorem IsNonarchimedean.map_le_map_one {α : Type*} [Semiring α] {f : α → ℝ} (h0 : f 0 ≤ f 1)
    (h : IsNonarchimedean f) (n : ℕ) : f n ≤ f 1 := by
  induction n with
  | zero => simpa using h0
  | succ n hn =>
    push_cast
    apply (h n 1).trans
    simp only [hn, max_eq_right, le_refl]

theorem IsNonarchimedean.of_algebraMap_nat {R} [NormedDivisionRing R]
  (is_na : IsNonarchimedean (‖algebraMap ℕ R ·‖ : ℕ → ℝ)) : IsNonarchimedean (‖·‖ : R → ℝ) := by
  -- It suffices to show that for all r : R, ‖r + 1‖ ≤ max ‖r‖ 1.
  suffices ∀ r : R, ‖r + 1‖ ≤ max ‖r‖ 1 by
    intro x y
    by_cases hy : y = 0
    · simp [hy]
    calc
      ‖x + y‖ = ‖x * y⁻¹ + 1‖ * ‖y‖ := by simp [← norm_mul, add_mul, hy]
      _ ≤ (max ‖x * y⁻¹‖ 1) * ‖y‖ := mul_le_mul_of_nonneg_right (this _) (norm_nonneg y)
      _ = max ‖x‖ ‖y‖ := by simp [max_mul_of_nonneg _ 1 (norm_nonneg y), hy]
  intro r
  suffices ∀ n : ℕ, ‖r + 1‖ ^ n ≤ (n + 1) * max (‖r‖ ^ n) 1 by
    -- Take ^ (1 / n : ℝ) for both side and take limit n → ∞ to prove the goal.
    apply le_of_tendsto_of_tendsto' (f := fun n : ℕ => (‖r + 1‖ ^ n : ℝ) ^ (1 / n : ℝ))
        (g := fun n => (n + 1 : ℝ) ^ (1 / n : ℝ) * max ‖r‖ 1) (b := atTop)
    -- The limit of (‖r + 1‖ ^ n) ^ (1 / ↑n) is ‖r + 1‖
    · refine tendsto_atTop_of_eventually_const (i₀ := 1) (fun i hi => ?_)
      simp [Real.pow_rpow_inv_natCast (norm_nonneg (r + 1)) (by linarith)]
    -- The limit of (n + 1) ^ (1 / ↑n) * max ‖r‖ 1 is max ‖r‖ 1.
    · nth_rw 2 [← one_mul (max ‖r‖ 1)]
      -- It suffices to show the limit of (n + 1) ^ (1 / ↑n) is 1.
      apply Filter.Tendsto.mul_const (max ‖r‖ 1)
      -- We use sandwich theorem, n ^ (1 / n) ≤ (n + 1) ^ (1 / ↑n) ≤ (n * n) ^ (1 / n) for n ≥ 1.
      apply tendsto_of_tendsto_of_tendsto_of_le_of_le'
          (f := (fun k : ℕ ↦ ((k : ℝ) + 1) ^ (1 / k : ℝ))) (g := fun n => n ^ (1 / n : ℝ))
          (h := fun n => (n * n) ^ (1 / n : ℝ)) (b := atTop) (a := 1)
      -- n ^ (1 / n) tends to 1.
      · exact tendsto_rpow_div.comp tendsto_natCast_atTop_atTop
      -- (n * n) ^ (1 / n) tends to 1.
      · have : (fun n : ℕ => (n * n : ℝ) ^ (1 / n : ℝ)) =
            (fun n : ℕ => (n : ℝ) ^ (1 / n : ℝ) * (n : ℝ) ^ (1 / n : ℝ)) := by
          funext x
          rw [Real.mul_rpow (by simp) (by simp)]
        rw [this]
        nth_rw 3 [← mul_one 1]
        apply Filter.Tendsto.mul <;>
        exact tendsto_rpow_div.comp tendsto_natCast_atTop_atTop
      -- n ^ (1 / n) ≤ (n + 1) ^ (1 / ↑n)
      · simp only [eventually_atTop]
        exact ⟨0, fun _ _ => Real.rpow_le_rpow (by linarith)
            (by linarith) (Nat.one_div_cast_nonneg _)⟩
      -- (n + 1) ^ (1 / ↑n) ≤ (n * n) ^ (1 / n).
      · simp only [eventually_atTop]
        refine ⟨2, fun n hn => Real.rpow_le_rpow (by linarith)
            ?_ (Nat.one_div_cast_nonneg _)⟩
        norm_cast
        calc
          n + 1 ≤ 2 * n := by linarith
          _ ≤ n * n := Nat.mul_le_mul_right n hn
    -- Given ∀ n : ℕ, ‖r + 1‖ ^ n ≤ (n + 1) * max (‖r‖ ^ n) 1, we show that
    -- (‖r + 1‖ ^ n) ^ (1 / ↑n) < (n + 1) ^ (1 / ↑n) * max ‖r‖ 1 holds for all n.
    · intro n
      by_cases hn : n = 0
      · simp [hn]
      calc
        (‖r + 1‖ ^ n) ^ (1 / n : ℝ) ≤  ((n + 1) * max (‖r‖ ^ n) 1) ^ (1 / n : ℝ) := by
          apply Real.rpow_le_rpow (pow_nonneg (norm_nonneg _) _)
              (this n) (Nat.one_div_cast_nonneg n)
        _ =  (n + 1) ^ (1 / n : ℝ) * max (‖r‖ ^ n) 1 ^ (1 / n : ℝ) := by
          rw [Real.mul_rpow (by linarith) (by simp)]
        _ = (n + 1) ^ (1 / n : ℝ) * max ‖r‖ 1 := by
          simp only [Set.mem_Ici, norm_nonneg, pow_nonneg, zero_le_one,
              (Real.monotoneOn_rpow_Ici_of_exponent_nonneg (Nat.one_div_cast_nonneg n)).map_max]
          simp [Real.pow_rpow_inv_natCast (norm_nonneg r) hn]
  -- Finally, we show that ‖r + 1‖ ^ n ≤ (n + 1) * max (‖r‖ ^ n) 1 for all n.
  intro n
  calc
    ‖r + 1‖ ^ n = ‖(r + 1) ^ n‖ := by simp
    _ = ‖∑ m ∈ Finset.range (n + 1), r ^ m * (n.choose m)‖ := by
      simp [(Commute.one_right r).add_pow]
    _ ≤ ∑ m ∈ Finset.range (n + 1), ‖r ^ m‖ := by
      refine norm_sum_le_of_le _ (fun m hm => (norm_mul_le (r ^ m) (n.choose m)).trans ?_)
      apply mul_le_of_le_one_right (norm_nonneg _)
      simpa using is_na.map_le_map_one (n := n.choose m)
    _ ≤ ∑ m ∈ Finset.range (n + 1), max ‖r ^ n‖ 1 := by
      refine Finset.sum_le_sum (fun i ha => ?_)
      by_cases hr : ‖r‖ ≤ 1 <;>
      simp only [norm_pow, le_max_iff]
      · exact Or.inr <| pow_le_one₀ (norm_nonneg r) hr
      · exact Or.inl <| (pow_le_pow_iff_right (by linarith)).mpr (Finset.mem_range_succ_iff.mp ha)
    _ = (n + 1) * max (‖r‖ ^ n) 1 := by simp

[Yakov Pechersky]

I specifically avoided importing rpow for my proof

[Yakov Pechersky]

And my preference is that if we're discussing the explicit norm, it should avoid utilizing the IsNonarchimedean predicate

[Yakov Pechersky]

Rather, help provide the proof that can be populated into the typeclass system -- phrase the goal with IsUltrametricDist

[Jiang Jiedong]

Yakov Pechersky said:

Rather, help provide the proof that can be populated into the typeclass system -- phrase the goal with IsUltrametricDist

Yes, I agree with your opinion. And I am now building a small conversion API between IsUltrametricDist and IsNonarchimedean.

[Yakov Pechersky]

I think the tendsto proof is conceptually "simpler" but in terms of the actual proof obligations, using the docs#le_of_forall_le_dense turns out to be similar

[Yakov Pechersky]

We have that conversion API in PRs that Maria Ines recently merged

[Jiang Jiedong]

Yakov Pechersky said:

We have that conversion API in PRs that Maria Ines recently merged

Ah, I only saw one direction, from IsNonarchimedean to IsUltrametricDist. Do we have both direction?

[Yakov Pechersky]

When do you need to have the proposition that the norm is IsNonarchimedean when IsUltrametricDist is available?

[Yakov Pechersky]

The benefit of IsUltrametricDist is that it is valid for (Semi)NormedGroups, while IsNonarchimedean is solely about addition.

[Jiang Jiedong]

Thanks for your advice. I was PRing my Krasner's lemma into mathlib. The original statements require the norm on K to be non-archimedean. Now I'll convert everything to the IsUltrametricDistside. Using type-class inference is definitely better than passing an explicit argument.

[David Loeffler]

Tagging @María Inés de Frutos Fernández in case she didn't see this