English
If deg p > 0 and f(p.leadingCoeff) ≠ 0, then for any l and z with abv ∘ z → atTop, the quantity abv(p.eval₂ f (z x)) also tends to atTop.
Русский
Пусть deg p > 0 и f(p.leadingCoeff) ≠ 0. Тогда при любом фильтре l и любой z с abv ∘ z → atTop, имеем abv(p.eval₂ f (z x)) → atTop.
LaTeX
$$$\\forall p\\, f,\, p.leadingCoeff \\neq 0,\, hd>0,\\; \\forall l \\; \\forall z:\\; Tendsto (abv \\circ z) l \\text{ atTop} \\Rightarrow\\; Tendsto (\\lambda x. abv(p.eval₂ f (z x))) l \\text{ atTop}$$$
Lean4
theorem tendsto_abv_eval₂_atTop {R S k α : Type*} [Semiring R] [Ring S] [Field k] [LinearOrder k]
[IsStrictOrderedRing k] (f : R →+* S) (abv : S → k) [IsAbsoluteValue abv] (p : R[X]) (hd : 0 < degree p)
(hf : f p.leadingCoeff ≠ 0) {l : Filter α} {z : α → S} (hz : Tendsto (abv ∘ z) l atTop) :
Tendsto (fun x => abv (p.eval₂ f (z x))) l atTop :=
by
revert hf; refine degree_pos_induction_on p hd ?_ ?_ ?_ <;> clear hd p
· rintro _ - hc
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)
· intro _ _ ihp hf
rw [leadingCoeff_mul_X] at hf
simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop₀ hz
· intro _ a hd ihp hf
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf
refine .atTop_of_add_const (abv (-f a)) ?_
refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_
simpa using ihp hf
