English
Let p be a nonarchimedean ring seminorm on a commutative ring R. For elements x, y in R and n in N, there exists m with m < n+1 such that p((x+y)^n)^{1/n} ≤ (p(x^m) p(y^{n−m}))^{1/n}. (In words, a form of the nonarchimedean inequality for powers.)
Русский
Пусть p — неархимедово кольцевое семинорм на кольце R. Для элементов x, y ∈ R и n ∈ ℕ существует m < n+1 такое, что p((x+y)^n)^{1/n} ≤ (p(x^m) p(y^{n−m}))^{1/n}.
LaTeX
$$$\exists m \in \mathbb{N},\ m < n+1 \ \land\ p((x+y)^n)^{1/n} \le (p(x^m)\, p(y^{n-m}))^{1/n}$$$
Lean4
theorem exists_index_pow_le (hna : IsNonarchimedean p) (x y : R) (n : ℕ) :
∃ (m : ℕ), m < n + 1 ∧ p ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤ (p (x ^ m) * p (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ)) :=
by
obtain ⟨m, hm_lt, hm⟩ := IsNonarchimedean.add_pow_le hna n x y
exact ⟨m, hm_lt, Real.rpow_le_rpow (apply_nonneg p _) hm (one_div_nonneg.mpr n.cast_nonneg')⟩
