English
Let R be a normed division ring. If for all x and m ∈ ℕ, ∥x+1∥^m ≤ (m+1) max(1, ∥x∥^m), then IsUltrametricDist R.
Русский
Пусть R — нормированное делимое кольцо. Если для всех x и натуральных m выполняется неравенство ∥x+1∥^m ≤ (m+1) max(1, ∥x∥^m), то IsUltrametricDist R.
LaTeX
$$$\\forall x\\in R, \\forall m\\in \\mathbb{N}, \\|x+1\\|^m \\le (m+1) \\max\\left(1, \\|x\\|^m\\right) \\Rightarrow \\mathrm{IsUltrametricDist}(R)$$$
Lean4
/-- This technical lemma is used in the proof of
`isUltrametricDist_of_forall_norm_natCast_le_one`. -/
theorem isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
(h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)) : IsUltrametricDist R := by
-- it will suffice to prove that `‖x + 1‖ ≤ max 1 ‖x‖`
refine
isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦
?_
-- Morally, we want to deduce this from the hypothesis `h` by taking an `m`-th root and showing
-- that `(m + 1) ^ (1 / m)` gets arbitrarily close to 1, although we will formalise this in a way
-- that avoids explicitly mentioning `m`-th roots.
-- First note it suffices to show that `‖x + 1‖ ≤ a` for all `a : ℝ` with `max ‖x‖ 1 < a`.
rw [max_comm]
refine le_of_forall_gt_imp_ge_of_dense fun a ha ↦ ?_
have ha' : 1 < a := (max_lt_iff.mp ha).left
obtain ⟨m, hm⟩ : ∃ m : ℕ, ((m + 1) : ℕ) < (a / (max 1 ‖x‖)) ^ m :=
by
apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt
rwa [one_lt_div (by positivity)]
-- and we rearrange again to get `(m + 1) • max 1 ‖x‖ ^ m < a ^ m`
rw [div_pow, lt_div_iff₀ (by positivity), ← nsmul_eq_mul] at hm
have hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m) := by
rw [pow_left_monotoneOn.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]
rw [hp] at hm
refine le_of_pow_le_pow_left₀ (fun h ↦ ?_) (zero_lt_one.trans ha').le ((h _ _).trans hm.le)
simp only [h, zero_add, pow_zero, max_self, one_smul, lt_self_iff_false] at hm
