English
Liouville-Weierstrass framework: for a polynomial f with integer coefficients, there exists a real constant c and, for each prime p > |f(0)|, an integer n_p and a polynomial g_p ∈ ℤ[X] with degree constraints so that for every root r of f, a quantitative bound holds between |n_p e^{r} − p g_p(r)| and c^p/(p−1)!.
Русский
В рамках теоремы Лиувиля–Вейерштрасса для целых коэффициентов f существует константа c и для каждого простого p > |f(0)| существует n_p ∈ ℤ и g_p ∈ ℤ[X] с ограничениями по степеням так, что для каждого корня r ∈ f(aroots) выполняется неравенство: |n_p e^{r} − p g_p(r)| ≤ c^p/(p−1)!.
LaTeX
$$$\\exists c\\in\\mathbb R,\\; \\forall p>(eval\\,0\\,f).natAbs,\\; p\\text{ prime}→\\exists n∈\\mathbb Z,\\; n\\not\\equiv 0\\ (p),\\; ∃ g_p∈ℤ[X],\\; \\deg(g_p)≤p\\deg(f)−1,\\; ∀{r∈f.aroots\\mathbb C},\\; \\|n e^{r} − p g_p(r)\\|≤\\frac{c^{p}}{(p-1)!}.$$
Lean4
theorem integral_exp_mul_eval (p : ℂ[X]) (s : ℂ) :
s * ∫ x in 0..1, exp (-(x • s)) * p.eval (x • s) = -(exp (-s) * p.sumIDeriv.eval s) + p.sumIDeriv.eval 0 :=
by
rw [← intervalIntegral.integral_const_mul,
intervalIntegral.integral_eq_sub_of_hasDerivAt (fun x hx => hasDerivAt_cexp_mul_sumIDeriv p s x)
(ContinuousOn.intervalIntegrable (by fun_prop))]
simp
