English
Let p be a polynomial over a commutative semiring R, viewed in A via an R-algebra, and let abv be an absolute value on A. If deg p > 0 and the leading coefficient of p does not map to 0 in A, then for any index set α, any z: α → A, and any filter l on α such that abv ∘ z tends to +∞ along l, the quantity abv(aeval(z x) p) also tends to +∞ along l. In other words, the absolute value of p evaluated at z grows without bound when the input grows without bound under abv.
Русский
Пусть p — многочлен над коммутативным полем R, рассматриваемый через R-алгебру в A, и abv — абсолютная величина на A. Если deg p > 0 и коэффициент при старшей степени не отображается в 0 в A, то для любой множества индексов α, любой z: α → A и любого фильтра l на α, если abv ∘ z tends к +∞ по l, то и abv(aeval(z x) p) tend к +∞ по l. То есть мажорная последовательность по модулю растёт без ограничений, если вход растёт без границ под abv.
LaTeX
$$$\\deg p > 0 \\;\\land\\; p.\\ leadsCoeff \\mapsto 0 \\\\neq 0 \\Rightarrow \\forall \\{l: \\text{Filter } \\alpha\\}\\{z: \\alpha \\to A\\},\\; \\mathrm{Tendsto}(\\mathrm{abv} \\circ z)\\, l\\, \\mathrm{atTop} \\Rightarrow \\mathrm{Tendsto}(x \\mapsto \\mathrm{abv}(\\mathrm{aeval}(z x) p))\\, l\\, \\mathrm{atTop}$$$
Lean4
theorem tendsto_abv_aeval_atTop {R A k α : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Field k] [LinearOrder k]
[IsStrictOrderedRing k] (abv : A → k) [IsAbsoluteValue abv] (p : R[X]) (hd : 0 < degree p)
(h₀ : algebraMap R A p.leadingCoeff ≠ 0) {l : Filter α} {z : α → A} (hz : Tendsto (abv ∘ z) l atTop) :
Tendsto (fun x => abv (aeval (z x) p)) l atTop :=
tendsto_abv_eval₂_atTop _ abv p hd h₀ hz
