English
If p is a ring seminorm with p(1) ≤ 1 and s: N → N is bounded by n (i.e., s(n) ≤ n), then for any x ∈ R and any ψ: N → N the sequence n ↦ p(x^{s(ψ(n))})^{1/ψ(n)} is bounded above.
Русский
Если p — кольцевой семинорм с p(1) ≤ 1 и s: ℕ → ℕ ограничена сверху числом n (то есть s(n) ≤ n), тогда для любого x ∈ R и любого ψ: ℕ → ℕ последовательность n ↦ p(x^{s(ψ(n))})^{1/ψ(n)} ограничена сверху.
LaTeX
$$$\text{If } p(1) \le 1\text{ and } s: \mathbb{N} \to \mathbb{N}\text{ with } s(n) \le n,\ \forall x:\,R,\ \forall \psi:\mathbb{N}\to\mathbb{N},\ IsBoundedUnder LE.le atTop\, \lambda n.\ p(x^{s(\psi(n))})^{1/\psi(n)}$$$
Lean4
/-- If `f` is a ring seminorm on `R` with `f 1 ≤ 1` and `s : ℕ → ℕ` is bounded by `n`, then
`f (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))` is eventually bounded. -/
theorem isBoundedUnder (hp : p 1 ≤ 1) {s : ℕ → ℕ} (hs_le : ∀ n : ℕ, s n ≤ n) {x : R} (ψ : ℕ → ℕ) :
IsBoundedUnder LE.le atTop fun n : ℕ => p (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) :=
by
have h_le : ∀ m : ℕ, p (x ^ s (ψ m)) ^ (1 / (ψ m : ℝ)) ≤ p x ^ ((s (ψ m) : ℝ) / (ψ m : ℝ)) :=
by
intro m
rw [← mul_one_div (s (ψ m) : ℝ), rpow_mul (apply_nonneg p x), rpow_natCast]
exact rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hp x _) (one_div_nonneg.mpr (cast_nonneg _))
apply isBoundedUnder_of
by_cases hfx : p x ≤ 1
· use 1, fun m => le_trans (h_le m) (rpow_le_one (apply_nonneg _ _) hfx (div_nonneg (cast_nonneg _) (cast_nonneg _)))
· use p x
intro m
apply le_trans (h_le m)
conv_rhs => rw [← rpow_one (p x)]
exact
rpow_le_rpow_of_exponent_le (le_of_lt (not_le.mp hfx)) (div_le_one_of_le₀ (cast_le.mpr (hs_le _)) (cast_nonneg _))
