English
The growth of the top order under powering is at least linear in n.
Русский
Рост верхнего порядка под возведением в степень линейно зависит от n.
LaTeX
$$$ n \cdot orderTop(x) \le orderTop(x^n) $$$
Lean4
theorem orderTop_nsmul_le_orderTop_pow {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R]
{x : HahnSeries Γ R} {n : ℕ} : n • x.orderTop ≤ (x ^ n).orderTop := by
induction n with
| zero =>
simp only [zero_smul, pow_zero]
by_cases h : (0 : R) = 1
· simp [subsingleton_iff_zero_eq_one.mp h]
· simp [nontrivial_of_ne 0 1 h]
| succ n ih =>
rw [add_nsmul, pow_add]
calc
n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := add_le_add_right ih (1 • x.orderTop)
(x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
(x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
(x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
