isUltrametricDist_of_forall_norm_natCast_le_one

English

Let R be a normed division ring. If for all natural numbers n we have ∥n∈R∥ ≤ 1, then IsUltrametricDist R.

Русский

Пусть R — нормированное делимое кольцо. Если для каждого натурального числа n выполняется ∥n∥ ≤ 1, то IsUltrametricDist R.

LaTeX

$$$\\forall n\\in \\mathbb{N}, \\|n\\cdot 1_R\\| \\le 1 \\Rightarrow \\mathrm{IsUltrametricDist}(R)$$$

Lean4

/-- To prove that a normed division ring is nonarchimedean, it suffices to prove that the norm
of the image of any natural is less than or equal to one. -/
theorem isUltrametricDist_of_forall_norm_natCast_le_one (h : ∀ n : ℕ, ‖(n : R)‖ ≤ 1) : IsUltrametricDist R := by
  -- from a previous lemma, suffices to prove that for all `m`, we have
    -- `‖x + 1‖ ^ m ≤ (m + 1) • max 1 ‖x‖ ^ m`

  refine
    isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
      (fun x m ↦ ?_)
        -- we first use our hypothesis about the norm of naturals to have that multiplication by
          -- naturals keeps the norm small

  replace h (x : R) (n : ℕ) : ‖n • x‖ ≤ ‖x‖ := by
    rw [nsmul_eq_mul, norm_mul]
    rcases (norm_nonneg x).eq_or_lt with hx | hx
    · simp only [← hx, mul_zero, le_refl]
    ·
      simpa only [mul_le_iff_le_one_left hx] using
        h
          _
            -- we expand the LHS using the binomial theorem, and apply the hypothesis to bound each term by
              -- a power of ‖x‖

  transitivity ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k
  ·
    simpa only [← norm_pow, (Commute.one_right x).add_pow, one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm] using
      (norm_sum_le _ _).trans
        (Finset.sum_le_sum fun _ _ ↦ h _ _)
          -- the nature of the norm means that one of `1` and `‖x‖ ^ m` is the largest of the two, so the
            -- other terms in the binomial expansion are bounded by the max of these, and the number of terms
            -- in the sum is precisely `m + 1`

  rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]
  rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩ | ⟨hm, hx⟩) <;> rw [hm] <;>
    -- which we show by comparing the terms in the sum one by one
    refine Finset.sum_le_sum fun i hi ↦ ?_
  · rcases eq_or_ne m 0 with rfl | hm
    ·
      simp only [pow_zero, le_refl,
        show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]
    · rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
      exact pow_le_one₀ (norm_nonneg _) hx
  · refine pow_le_pow_right₀ ?_ (by simpa only [Finset.mem_range, Nat.lt_succ] using hi)
    contrapose! hx
    exact pow_le_one₀ (norm_nonneg _) hx.le

Похожие утверждения