Theory E_Transcendental
section ‹Proof of the Transcendence of $e$›
theory E_Transcendental
imports
"HOL-Complex_Analysis.Complex_Analysis"
"HOL-Number_Theory.Number_Theory"
"HOL-Computational_Algebra.Polynomial"
begin
hide_const (open) UnivPoly.coeff UnivPoly.up_ring.monom
hide_const (open) Module.smult Coset.order
subsection ‹Various auxiliary facts›
lemma fact_dvd_pochhammer:
assumes "m ≤ n + 1"
shows "fact m dvd pochhammer (int n - int m + 1) m"
proof -
have "(real n gchoose m) * fact m = of_int (pochhammer (int n - int m + 1) m)"
by (simp add: gbinomial_pochhammer' pochhammer_of_int [symmetric])
also have "(real n gchoose m) * fact m = of_int (int (n choose m) * fact m)"
by (simp add: binomial_gbinomial)
finally have "int (n choose m) * fact m = pochhammer (int n - int m + 1) m"
by (subst (asm) of_int_eq_iff)
from this [symmetric] show ?thesis by simp
qed
lemma prime_elem_int_not_dvd_neg1_power:
"prime_elem (p :: int) ⟹ ¬p dvd (-1) ^ n"
by (metis dvdI minus_one_mult_self unit_imp_no_prime_divisors)
lemma nat_fact [simp]: "nat (fact n) = fact n"
by (metis nat_int of_nat_fact of_nat_fact)
lemma prime_dvd_fact_iff_int:
"p dvd fact n ⟷ p ≤ int n" if "prime p"
using that prime_dvd_fact_iff [of "nat ¦p¦" n]
by auto (simp add: prime_ge_0_int)
lemma power_over_fact_tendsto_0:
"(λn. (x :: real) ^ n / fact n) ⇢ 0"
using summable_exp[of x] by (intro summable_LIMSEQ_zero) (simp add: sums_iff field_simps)
lemma power_over_fact_tendsto_0':
"(λn. c * (x :: real) ^ n / fact n) ⇢ 0"
using tendsto_mult[OF tendsto_const[of c] power_over_fact_tendsto_0[of x]] by simp
subsection ‹Lifting integer polynomials›
lift_definition of_int_poly :: "int poly ⇒ 'a :: comm_ring_1 poly" is "λg x. of_int (g x)"
by (auto elim: eventually_mono)
lemma coeff_of_int_poly [simp]: "coeff (of_int_poly p) n = of_int (coeff p n)"
by (simp add: of_int_poly.rep_eq)
lemma of_int_poly_0 [simp]: "of_int_poly 0 = 0"
by transfer (simp add: fun_eq_iff)
lemma of_int_poly_pCons [simp]: "of_int_poly (pCons c p) = pCons (of_int c) (of_int_poly p)"
by transfer' (simp add: fun_eq_iff split: nat.splits)
lemma of_int_poly_smult [simp]: "of_int_poly (smult c p) = smult (of_int c) (of_int_poly p)"
by transfer simp
lemma of_int_poly_1 [simp]: "of_int_poly 1 = 1"
by (simp add: one_pCons)
lemma of_int_poly_add [simp]: "of_int_poly (p + q) = of_int_poly p + of_int_poly q"
by transfer' (simp add: fun_eq_iff)
lemma of_int_poly_mult [simp]: "of_int_poly (p * q) = (of_int_poly p * of_int_poly q)"
by (induction p) simp_all
lemma of_int_poly_sum [simp]: "of_int_poly (sum f A) = sum (λx. of_int_poly (f x)) A"
by (induction A rule: infinite_finite_induct) simp_all
lemma of_int_poly_prod [simp]: "of_int_poly (prod f A) = prod (λx. of_int_poly (f x)) A"
by (induction A rule: infinite_finite_induct) simp_all
lemma of_int_poly_power [simp]: "of_int_poly (p ^ n) = of_int_poly p ^ n"
by (induction n) simp_all
lemma of_int_poly_monom [simp]: "of_int_poly (monom c n) = monom (of_int c) n"
by transfer (simp add: fun_eq_iff)
lemma poly_of_int_poly [simp]: "poly (of_int_poly p) (of_int x) = of_int (poly p x)"
by (induction p) simp_all
lemma poly_of_int_poly_of_nat [simp]: "poly (of_int_poly p) (of_nat x) = of_int (poly p (int x))"
by (induction p) simp_all
lemma poly_of_int_poly_0 [simp]: "poly (of_int_poly p) 0 = of_int (poly p 0)"
by (induction p) simp_all
lemma poly_of_int_poly_1 [simp]: "poly (of_int_poly p) 1 = of_int (poly p 1)"
by (induction p) simp_all
lemma poly_of_int_poly_of_real [simp]:
"poly (of_int_poly p) (of_real x) = of_real (poly (of_int_poly p) x)"
by (induction p) simp_all
lemma of_int_poly_eq_iff [simp]:
"of_int_poly p = (of_int_poly q :: 'a :: {comm_ring_1, ring_char_0} poly) ⟷ p = q"
by (simp add: poly_eq_iff)
lemma of_int_poly_eq_0_iff [simp]:
"of_int_poly p = (0 :: 'a :: {comm_ring_1, ring_char_0} poly) ⟷ p = 0"
using of_int_poly_eq_iff[of p 0] by (simp del: of_int_poly_eq_iff)
lemma degree_of_int_poly [simp]:
"degree (of_int_poly p :: 'a :: {comm_ring_1, ring_char_0} poly) = degree p"
by (simp add: degree_def)
lemma pderiv_of_int_poly [simp]: "pderiv (of_int_poly p) = of_int_poly (pderiv p)"
by (induction p) (simp_all add: pderiv_pCons)
lemma higher_pderiv_of_int_poly [simp]:
"(pderiv ^^ n) (of_int_poly p) = of_int_poly ((pderiv ^^ n) p)"
by (induction n) simp_all
lemma int_polyE:
assumes "⋀n. coeff (p :: 'a :: {comm_ring_1, ring_char_0} poly) n ∈ ℤ"
obtains p' where "p = of_int_poly p'"
proof -
from assms have "∀n. ∃c. coeff p n = of_int c" by (auto simp: Ints_def)
hence "∃c. ∀n. of_int (c n) = coeff p n" by (simp add: choice_iff eq_commute)
then obtain c where c: "of_int (c n) = coeff p n" for n by blast
have [simp]: "coeff (Abs_poly c) = c"
proof (rule poly.Abs_poly_inverse, clarify)
have "eventually (λn. n > degree p) at_top" by (rule eventually_gt_at_top)
hence "eventually (λn. coeff p n = 0) at_top"
by eventually_elim (simp add: coeff_eq_0)
thus "eventually (λn. c n = 0) cofinite"
by (simp add: c [symmetric] cofinite_eq_sequentially)
qed
have "p = of_int_poly (Abs_poly c)"
by (rule poly_eqI) (simp add: c)
thus ?thesis by (rule that)
qed
subsection ‹General facts about polynomials›
lemma pderiv_power:
"pderiv (p ^ n) = smult (of_nat n) (p ^ (n - 1) * pderiv p)"
by (cases n) (simp_all add: pderiv_power_Suc del: power_Suc)
lemma degree_prod_sum_eq:
"(⋀x. x ∈ A ⟹ f x ≠ 0) ⟹
degree (prod f A :: 'a :: idom poly) = (∑x∈A. degree (f x))"
by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)
lemma pderiv_monom:
"pderiv (monom c n) = monom (of_nat n * c) (n - 1)"
by (cases n)
(simp_all add: monom_altdef pderiv_power_Suc pderiv_smult pderiv_pCons mult_ac del: power_Suc)
lemma power_poly_const [simp]: "[:c:] ^ n = [:c ^ n:]"
by (induction n) (simp_all add: power_commutes)
lemma monom_power: "monom c n ^ k = monom (c ^ k) (n * k)"
by (induction k) (simp_all add: mult_monom)
lemma coeff_higher_pderiv:
"coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)
lemma higher_pderiv_add: "(pderiv ^^ n) (p + q) = (pderiv ^^ n) p + (pderiv ^^ n) q"
by (induction n arbitrary: p q) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_add)
lemma higher_pderiv_smult: "(pderiv ^^ n) (smult c p) = smult c ((pderiv ^^ n) p)"
by (induction n arbitrary: p) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_smult)
lemma higher_pderiv_0 [simp]: "(pderiv ^^ n) 0 = 0"
by (induction n) simp_all
lemma higher_pderiv_monom:
"m ≤ n + 1 ⟹ (pderiv ^^ m) (monom c n) = monom (pochhammer (int n - int m + 1) m * c) (n - m)"
proof (induction m arbitrary: c n)
case (Suc m)
thus ?case
by (cases n)
(simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
qed simp_all
lemma higher_pderiv_monom_eq_zero:
"m > n + 1 ⟹ (pderiv ^^ m) (monom c n) = 0"
proof (induction m arbitrary: c n)
case (Suc m)
thus ?case
by (cases n)
(simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
qed simp_all
lemma higher_pderiv_sum: "(pderiv ^^ n) (sum f A) = (∑x∈A. (pderiv ^^ n) (f x))"
by (induction A rule: infinite_finite_induct) (simp_all add: higher_pderiv_add)
lemma fact_dvd_higher_pderiv:
"[:fact n :: int:] dvd (pderiv ^^ n) p"
proof -
have "[:fact n:] dvd (pderiv ^^ n) (monom c k)" for c :: int and k :: nat
by (cases "n ≤ k + 1")
(simp_all add: higher_pderiv_monom higher_pderiv_monom_eq_zero
fact_dvd_pochhammer const_poly_dvd_iff)
hence "[:fact n:] dvd (pderiv ^^ n) (∑k≤degree p. monom (coeff p k) k)"
by (simp_all add: higher_pderiv_sum dvd_sum)
thus ?thesis by (simp add: poly_as_sum_of_monoms)
qed
lemma fact_dvd_poly_higher_pderiv_aux:
"(fact n :: int) dvd poly ((pderiv ^^ n) p) x"
proof -
have "[:fact n:] dvd (pderiv ^^ n) p" by (rule fact_dvd_higher_pderiv)
then obtain q where "(pderiv ^^ n) p = [:fact n:] * q" by (erule dvdE)
thus ?thesis by simp
qed
lemma fact_dvd_poly_higher_pderiv_aux':
"m ≤ n ⟹ (fact m :: int) dvd poly ((pderiv ^^ n) p) x"
by (meson dvd_trans fact_dvd fact_dvd_poly_higher_pderiv_aux)
lemma algebraicE':
assumes "algebraic (x :: 'a :: field_char_0)"
obtains p where "p ≠ 0" "poly (of_int_poly p) x = 0"
proof -
from assms obtain q where "⋀i. coeff q i ∈ ℤ" "q ≠ 0" "poly q x = 0"
by (erule algebraicE)
moreover from this(1) obtain q' where "q = of_int_poly q'" by (erule int_polyE)
ultimately show ?thesis by (intro that[of q']) simp_all
qed
lemma algebraicE'_nonzero:
assumes "algebraic (x :: 'a :: field_char_0)" "x ≠ 0"
obtains p where "p ≠ 0" "coeff p 0 ≠ 0" "poly (of_int_poly p) x = 0"
proof -
from assms(1) obtain p where p: "p ≠ 0" "poly (of_int_poly p) x = 0"
by (erule algebraicE')
define n :: nat where "n = order 0 p"
have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff p n_def)
then obtain q where q: "p = monom 1 n * q" by (erule dvdE)
from p have "q ≠ 0" "poly (of_int_poly q) x = 0" by (auto simp: q poly_monom assms(2))
moreover from this have "order 0 p = n + order 0 q" by (simp add: q order_mult)
hence "order 0 q = 0" by (simp add: n_def)
with ‹q ≠ 0› have "poly q 0 ≠ 0" by (simp add: order_root)
ultimately show ?thesis using that[of q] by (auto simp: poly_0_coeff_0)
qed
lemma algebraic_of_real_iff [simp]:
"algebraic (of_real x :: 'a :: {real_algebra_1,field_char_0}) ⟷ algebraic x"
proof
assume "algebraic (of_real x :: 'a)"
then obtain p where "p ≠ 0" "poly (of_int_poly p) (of_real x :: 'a) = 0"
by (erule algebraicE')
hence "(of_int_poly p :: real poly) ≠ 0"
"poly (of_int_poly p :: real poly) x = 0" by simp_all
thus "algebraic x" by (intro algebraicI[of "of_int_poly p"]) simp_all
next
assume "algebraic x"
then obtain p where "p ≠ 0" "poly (of_int_poly p) x = 0" by (erule algebraicE')
hence "of_int_poly p ≠ (0 :: 'a poly)" "poly (of_int_poly p) (of_real x :: 'a) = 0"
by simp_all
thus "algebraic (of_real x)" by (intro algebraicI[of "of_int_poly p"]) simp_all
qed
subsection ‹Main proof›
lemma lindemann_weierstrass_integral:
fixes u :: complex and f :: "complex poly"
defines "df ≡ λn. (pderiv ^^ n) f"
defines "m ≡ degree f"
defines "I ≡ λf u. exp u * (∑j≤degree f. poly ((pderiv ^^ j) f) 0) -
(∑j≤degree f. poly ((pderiv ^^ j) f) u)"
shows "((λt. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)"
proof -
note [derivative_intros] =
exp_scaleR_has_vector_derivative_right vector_diff_chain_within
let ?g = "λt. 1 - t" and ?f = "λt. -exp (t *⇩R u)"
have "((λt. exp ((1 - t) *⇩R u) * u) has_integral
(?f ∘ ?g) 1 - (?f ∘ ?g) 0) {0..1}"
by (rule fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros simp del: o_apply)
hence aux_integral: "((λt. exp (u - t *⇩R u) * u) has_integral exp u - 1) {0..1}"
by (simp add: algebra_simps)
have "((λt. exp (u - t *⇩R u) * u * poly f (t *⇩R u)) has_integral I f u) {0..1}"
unfolding df_def m_def
proof (induction "degree f" arbitrary: f)
case 0
then obtain c where c: "f = [:c:]" by (auto elim: degree_eq_zeroE)
have "((λt. c * (exp (u - t *⇩R u) * u)) has_integral c * (exp u - 1)) {0..1}"
using aux_integral by (rule has_integral_mult_right)
with c show ?case by (simp add: algebra_simps I_def)
next
case (Suc m)
define df where "df = (λj. (pderiv ^^ j) f)"
show ?case
proof (rule integration_by_parts[OF bounded_bilinear_mult])
fix t :: real assume "t ∈ {0..1}"
have "((?f ∘ ?g) has_vector_derivative exp (u - t *⇩R u) * u) (at t)"
by (auto intro!: derivative_eq_intros simp: algebra_simps simp del: o_apply)
thus "((λt. -exp (u - t *⇩R u)) has_vector_derivative exp (u - t *⇩R u) * u) (at t)"
by (simp add: algebra_simps o_def)
next
fix t :: real assume "t ∈ {0..1}"
have "(poly f ∘ (λt. t *⇩R u) has_vector_derivative u * poly (pderiv f) (t *⇩R u)) (at t)"
by (rule field_vector_diff_chain_at) (auto intro!: derivative_eq_intros)
thus "((λt. poly f (t *⇩R u)) has_vector_derivative u * poly (pderiv f) (t *⇩R u)) (at t)"
by (simp add: o_def)
next
from Suc(2) have m: "m = degree (pderiv f)" by (simp add: degree_pderiv)
from Suc(1)[OF this] this
have "((λt. exp (u - t *⇩R u) * u * poly (pderiv f) (t *⇩R u)) has_integral
exp u * (∑j=0..m. poly (df (Suc j)) 0) - (∑j=0..m. poly (df (Suc j)) u)) {0..1}"
by (simp add: df_def funpow_swap1 atMost_atLeast0 I_def)
also have "(∑j=0..m. poly (df (Suc j)) 0) = (∑j=Suc 0..Suc m. poly (df j) 0)"
by (rule sum.shift_bounds_cl_Suc_ivl [symmetric])
also have "… = (∑j=0..Suc m. poly (df j) 0) - poly f 0"
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
also have "(∑j=0..m. poly (df (Suc j)) u) = (∑j=Suc 0..Suc m. poly (df j) u)"
by (rule sum.shift_bounds_cl_Suc_ivl [symmetric])
also have "… = (∑j=0..Suc m. poly (df j) u) - poly f u"
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
finally have "((λt. - (exp (u - t *⇩R u) * u * poly (pderiv f) (t *⇩R u))) has_integral
-(exp u * ((∑j = 0..Suc m. poly (df j) 0) - poly f 0) -
((∑j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}"
(is "(_ has_integral ?I) _") by (rule has_integral_neg)
also have "?I = - exp (u - 1 *⇩R u) * poly f (1 *⇩R u) -
- exp (u - 0 *⇩R u) * poly f (0 *⇩R u) - I f u"
by (simp add: df_def algebra_simps Suc(2) atMost_atLeast0 I_def)
finally show "((λt. - exp (u - t *⇩R u) * (u * poly (pderiv f) (t *⇩R u)))
has_integral …) {0..1}" by (simp add: algebra_simps)
qed (auto intro!: continuous_intros)
qed
thus ?thesis by (simp add: has_contour_integral_linepath algebra_simps)
qed
locale lindemann_weierstrass_aux =
fixes f :: "complex poly"
begin
definition I :: "complex ⇒ complex" where
"I u = exp u * (∑j≤degree f. poly ((pderiv ^^ j) f) 0) -
(∑j≤degree f. poly ((pderiv ^^ j) f) u)"
lemma lindemann_weierstrass_integral_bound:
fixes u :: complex
assumes "C ≥ 0" "⋀t. t ∈ closed_segment 0 u ⟹ norm (poly f t) ≤ C"
shows "norm (I u) ≤ norm u * exp (norm u) * C"
proof -
have "I u = contour_integral (linepath 0 u) (λt. exp (u - t) * poly f t)"
using contour_integral_unique[OF lindemann_weierstrass_integral[of u f]] unfolding I_def ..
also have "norm … ≤ exp (norm u) * C * norm (u - 0)"
proof (intro contour_integral_bound_linepath)
fix t assume t: "t ∈ closed_segment 0 u"
then obtain s where s: "s ∈ {0..1}" "t = s *⇩R u" by (auto simp: closed_segment_def)
hence "s * norm u ≤ 1 * norm u" by (intro mult_right_mono) simp_all
with s have norm_t: "norm t ≤ norm u" by auto
from s have "Re u - Re t = (1 - s) * Re u" by (simp add: algebra_simps)
also have "… ≤ norm u"
proof (cases "Re u ≥ 0")
case True
with ‹s ∈ {0..1}› have "(1 - s) * Re u ≤ 1 * Re u" by (intro mult_right_mono) simp_all
also have "Re u ≤ norm u" by (rule complex_Re_le_cmod)
finally show ?thesis by simp
next
case False
with ‹s ∈ {0..1}› have "(1 - s) * Re u ≤ 0" by (intro mult_nonneg_nonpos) simp_all
also have "… ≤ norm u" by simp
finally show ?thesis .
qed
finally have "exp (Re u - Re t) ≤ exp (norm u)" by simp
hence "exp (Re u - Re t) * norm (poly f t) ≤ exp (norm u) * C"
using assms t norm_t by (intro mult_mono) simp_all
thus "norm (exp (u - t) * poly f t) ≤ exp (norm u) * C"
by (simp add: norm_mult exp_diff norm_divide field_simps)
qed (auto simp: intro!: mult_nonneg_nonneg contour_integrable_continuous_linepath
continuous_intros assms)
finally show ?thesis by (simp add: mult_ac)
qed
end
lemma poly_higher_pderiv_aux1:
fixes c :: "'a :: idom"
assumes "k < n"
shows "poly ((pderiv ^^ k) ([:-c, 1:] ^ n * p)) c = 0"
using assms
proof (induction k arbitrary: n p)
case (Suc k n p)
from Suc.prems obtain n' where n: "n = Suc n'" by (cases n) auto
from Suc.prems n have "k < n'" by simp
have "(pderiv ^^ Suc k) ([:- c, 1:] ^ n * p) =
(pderiv ^^ k) ([:- c, 1:] ^ n * pderiv p + [:- c, 1:] ^ n' * smult (of_nat n) p)"
by (simp only: funpow_Suc_right o_def pderiv_mult n pderiv_power_Suc,
simp only: n [symmetric]) (simp add: pderiv_pCons mult_ac)
also from Suc.prems ‹k < n'› have "poly … c = 0"
by (simp add: higher_pderiv_add Suc.IH del: mult_smult_right)
finally show ?case .
qed simp_all
lemma poly_higher_pderiv_aux1':
fixes c :: "'a :: idom"
assumes "k < n" "[:-c, 1:] ^ n dvd p"
shows "poly ((pderiv ^^ k) p) c = 0"
proof -
from assms(2) obtain q where "p = [:-c, 1:] ^ n * q" by (elim dvdE)
also from assms(1) have "poly ((pderiv ^^ k) …) c = 0"
by (rule poly_higher_pderiv_aux1)
finally show ?thesis .
qed
lemma poly_higher_pderiv_aux2:
fixes c :: "'a :: {idom, semiring_char_0}"
shows "poly ((pderiv ^^ n) ([:-c, 1:] ^ n * p)) c = fact n * poly p c"
proof (induction n arbitrary: p)
case (Suc n p)
have "(pderiv ^^ Suc n) ([:- c, 1:] ^ Suc n * p) =
(pderiv ^^ n) ([:- c, 1:] ^ Suc n * pderiv p) +
(pderiv ^^ n) ([:- c, 1:] ^ n * smult (1 + of_nat n) p)"
by (simp del: funpow.simps power_Suc add: funpow_Suc_right pderiv_mult
pderiv_power_Suc higher_pderiv_add pderiv_pCons mult_ac)
also have "[:- c, 1:] ^ Suc n * pderiv p = [:- c, 1:] ^ n * ([:-c, 1:] * pderiv p)"
by (simp add: algebra_simps)
finally show ?case by (simp add: Suc.IH del: mult_smult_right power_Suc)
qed simp_all
lemma poly_higher_pderiv_aux3:
fixes c :: "'a :: {idom,semiring_char_0}"
assumes "k ≥ n"
shows "∃q. poly ((pderiv ^^ k) ([:-c, 1:] ^ n * p)) c = fact n * poly q c"
using assms
proof (induction k arbitrary: n p)
case (Suc k n p)
show ?case
proof (cases n)
fix n' assume n: "n = Suc n'"
have "poly ((pderiv ^^ Suc k) ([:-c, 1:] ^ n * p)) c =
poly ((pderiv ^^ k) ([:- c, 1:] ^ n * pderiv p)) c +
of_nat n * poly ((pderiv ^^ k) ([:-c, 1:] ^ n' * p)) c"
by (simp del: funpow.simps power_Suc add: funpow_Suc_right pderiv_power_Suc
pderiv_mult n pderiv_pCons higher_pderiv_add mult_ac higher_pderiv_smult)
also have "∃q1. poly ((pderiv ^^ k) ([:-c, 1:] ^ n * pderiv p)) c = fact n * poly q1 c"
using Suc.prems Suc.IH[of n "pderiv p"]
by (cases "n' = k") (auto simp: n poly_higher_pderiv_aux1 simp del: power_Suc of_nat_Suc
intro: exI[of _ "0::'a poly"])
then obtain q1
where "poly ((pderiv ^^ k) ([:-c, 1:] ^ n * pderiv p)) c = fact n * poly q1 c" ..
also from Suc.IH[of n' p] Suc.prems obtain q2
where "poly ((pderiv ^^ k) ([:-c, 1:] ^ n' * p)) c = fact n' * poly q2 c"
by (auto simp: n)
finally show ?case by (auto intro!: exI[of _ "q1 + q2"] simp: n algebra_simps)
qed auto
qed auto
lemma poly_higher_pderiv_aux3':
fixes c :: "'a :: {idom, semiring_char_0}"
assumes "k ≥ n" "[:-c, 1:] ^ n dvd p"
shows "fact n dvd poly ((pderiv ^^ k) p) c"
proof -
from assms(2) obtain q where "p = [:-c, 1:] ^ n * q" by (elim dvdE)
with poly_higher_pderiv_aux3[OF assms(1), of c q] show ?thesis by auto
qed
lemma e_transcendental_aux_bound:
obtains C where "C ≥ 0"
"⋀x. x ∈ closed_segment 0 (of_nat n) ⟹
norm (∏k∈{1..n}. (x - of_nat k :: complex)) ≤ C"
proof -
let ?f = "λx. (∏k∈{1..n}. (x - of_nat k))"
define C where "C = max 0 (Sup (cmod ` ?f ` closed_segment 0 (of_nat n)))"
have "C ≥ 0" by (simp add: C_def)
moreover {
fix x :: complex assume "x ∈ closed_segment 0 (of_nat n)"
hence "cmod (?f x) ≤ Sup ((cmod ∘ ?f) ` closed_segment 0 (of_nat n))"
by (intro cSup_upper bounded_imp_bdd_above compact_imp_bounded compact_continuous_image)
(auto intro!: continuous_intros)
also have "… ≤ C" by (simp add: C_def image_comp)
finally have "cmod (?f x) ≤ C" .
}
ultimately show ?thesis by (rule that)
qed
theorem e_transcendental_complex: "¬ algebraic (exp 1 :: complex)"
proof
assume "algebraic (exp 1 :: complex)"
then obtain q :: "int poly"
where q: "q ≠ 0" "coeff q 0 ≠ 0" "poly (of_int_poly q) (exp 1 :: complex) = 0"
by (elim algebraicE'_nonzero) simp_all
define n :: nat where "n = degree q"
from q have [simp]: "n ≠ 0" by (intro notI) (auto simp: n_def elim!: degree_eq_zeroE)
define qmax where "qmax = Max (insert 0 (abs ` set (coeffs q)))"
have qmax_nonneg [simp]: "qmax ≥ 0" by (simp add: qmax_def)
have qmax: "¦coeff q k¦ ≤ qmax" for k
by (cases "k ≤ degree q")
(auto simp: qmax_def coeff_eq_0 coeffs_def simp del: upt_Suc intro: Max.coboundedI)
obtain C where C: "C ≥ 0"
"⋀x. x ∈ closed_segment 0 (of_nat n) ⟹ norm (∏k∈{1..n}. (x - of_nat k :: complex)) ≤ C"
by (erule e_transcendental_aux_bound)
define E where "E = (1 + real n) * real_of_int qmax * real n * exp (real n) / real n"
define F where "F = real n * C"
have ineq: "fact (p - 1) ≤ E * F ^ p" if p: "prime p" "p > n" "p > abs (coeff q 0)" for p
proof -
from p(1) have p_pos: "p > 0" by (simp add: prime_gt_0_nat)
define f :: "int poly"
where "f = monom 1 (p - 1) * (∏k∈{1..n}. [:-of_nat k, 1:] ^ p)"
have poly_f: "poly (of_int_poly f) x = x ^ (p - 1) * (∏k∈{1..n}. (x - of_nat k)) ^ p"
for x :: complex by (simp add: f_def poly_prod poly_monom prod_power_distrib)
define m :: nat where "m = degree f"
from p_pos have m: "m = (n + 1) * p - 1"
by (simp add: m_def f_def degree_mult_eq degree_monom_eq degree_prod_sum_eq degree_linear_power)
define M :: int where "M = (- 1) ^ (n * p) * fact n ^ p"
with p have p_not_dvd_M: "¬int p dvd M"
by (auto simp: M_def prime_elem_int_not_dvd_neg1_power prime_dvd_power_iff
prime_gt_0_nat prime_dvd_fact_iff_int prime_dvd_mult_iff)
interpret lindemann_weierstrass_aux "of_int_poly f" .
define J :: complex where "J = (∑k≤n. of_int (coeff q k) * I (of_nat k))"
define idxs where "idxs = ({..n}×{..m}) - {(0, p - 1)}"
hence "J = (∑k≤n. of_int (coeff q k) * exp 1 ^ k) * (∑n≤m. of_int (poly ((pderiv ^^ n) f) 0)) -
of_int (∑k≤n. ∑n≤m. coeff q k * poly ((pderiv ^^ n) f) (int k))"
by (simp add: J_def I_def algebra_simps sum_subtractf sum_distrib_left m_def
exp_of_nat_mult [symmetric])
also have "(∑k≤n. of_int (coeff q k) * exp 1 ^ k) = poly (of_int_poly q) (exp 1 :: complex)"
by (simp add: poly_altdef n_def)
also have "… = 0" by fact
finally have "J = of_int (-(∑(k,n)∈{..n}×{..m}. coeff q k * poly ((pderiv ^^ n) f) (int k)))"
by (simp add: sum.cartesian_product)
also have "{..n}×{..m} = insert (0, p - 1) idxs" by (auto simp: m idxs_def)
also have "-(∑(k,n)∈…. coeff q k * poly ((pderiv ^^ n) f) (int k)) =
- (coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0) -
(∑(k, n)∈idxs. coeff q k * poly ((pderiv ^^ n) f) (of_nat k))"
by (subst sum.insert) (simp_all add: idxs_def)
also have "coeff q 0 * poly ((pderiv ^^ (p - 1)) f) 0 = coeff q 0 * M * fact (p - 1)"
proof -
have "f = [:-0, 1:] ^ (p - 1) * (∏k = 1..n. [:- of_nat k, 1:] ^ p)"
by (simp add: f_def monom_altdef)
also have "poly ((pderiv ^^ (p - 1)) …) 0 =
fact (p - 1) * poly (∏k = 1..n. [:- of_nat k, 1:] ^ p) 0"
by (rule poly_higher_pderiv_aux2)
also have "poly (∏k = 1..n. [:- of_nat k :: int, 1:] ^ p) 0 = (-1)^(n*p) * fact n ^ p"
by (induction n) (simp_all add: prod.nat_ivl_Suc' power_mult_distrib mult_ac
power_minus' power_add del: of_nat_Suc)
finally show ?thesis by (simp add: mult_ac M_def)
qed
also obtain N where "(∑(k, n)∈idxs. coeff q k * poly ((pderiv ^^ n) f) (int k)) = fact p * N"
proof -
have "∀(k, n)∈idxs. fact p dvd poly ((pderiv ^^ n) f) (of_nat k)"
proof clarify
fix k j assume idxs: "(k, j) ∈ idxs"
then consider "k = 0" "j < p - 1" | "k = 0" "j > p - 1" | "k ≠ 0" "j < p" | "k ≠ 0" "j ≥ p"
by (fastforce simp: idxs_def)
thus "fact p dvd poly ((pderiv ^^ j) f) (of_nat k)"
proof cases
case 1
thus ?thesis
by (simp add: f_def poly_higher_pderiv_aux1' monom_altdef)
next
case 2
thus ?thesis
by (simp add: f_def poly_higher_pderiv_aux3' monom_altdef fact_dvd_poly_higher_pderiv_aux')
next
case 3
thus ?thesis unfolding f_def
by (subst poly_higher_pderiv_aux1'[of _ p])
(insert idxs, auto simp: idxs_def intro!: dvd_mult)
next
case 4
thus ?thesis unfolding f_def
by (intro poly_higher_pderiv_aux3') (insert idxs, auto intro!: dvd_mult simp: idxs_def)
qed
qed
hence "fact p dvd (∑(k, n)∈idxs. coeff q k * poly ((pderiv ^^ n) f) (int k))"
by (auto intro!: dvd_sum dvd_mult simp del: of_int_fact)
with that show thesis
by blast
qed
also from p have "- (coeff q 0 * M * fact (p - 1)) - fact p * N =
- fact (p - 1) * (coeff q 0 * M + p * N)"
by (subst fact_reduce[of p]) (simp_all add: algebra_simps)
finally have J: "J = -of_int (fact (p - 1) * (coeff q 0 * M + p * N))" by simp
from p q(2) have "¬p dvd coeff q 0 * M + p * N"
by (auto simp: dvd_add_left_iff p_not_dvd_M prime_dvd_fact_iff_int prime_dvd_mult_iff
dest: dvd_imp_le_int)
hence "coeff q 0 * M + p * N ≠ 0" by (intro notI) simp_all
hence "abs (coeff q 0 * M + p * N) ≥ 1" by simp
hence "norm (of_int (coeff q 0 * M + p * N) :: complex) ≥ 1" by (simp only: norm_of_int)
hence "fact (p - 1) * … ≥ fact (p - 1) * 1" by (intro mult_left_mono) simp_all
hence J_lower: "norm J ≥ fact (p - 1)" unfolding J norm_minus_cancel of_int_mult of_int_fact
by (simp add: norm_mult)
have "norm J ≤ (∑k≤n. norm (of_int (coeff q k) * I (of_nat k)))"
unfolding J_def by (rule norm_sum)
also have "… ≤ (∑k≤n. of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p))"
proof (intro sum_mono)
fix k assume k: "k ∈ {..n}"
have "n > 0" by (rule ccontr) simp
{
fix x :: complex assume x: "x ∈ closed_segment 0 (of_nat k)"
then obtain t where t: "t ≥ 0" "t ≤ 1" "x = of_real t * of_nat k"
by (auto simp: closed_segment_def scaleR_conv_of_real)
hence "norm x = t * real k" by (simp add: norm_mult)
also from ‹t ≤ 1› k have *: "… ≤ 1 * real n" by (intro mult_mono) simp_all
finally have x': "norm x ≤ real n" by simp
from t ‹n > 0› * have x'': "x ∈ closed_segment 0 (of_nat n)"
by (auto simp: closed_segment_def scaleR_conv_of_real field_simps
intro!: exI[of _ "t * real k / real n"] )
have "norm (poly (of_int_poly f) x) =
norm x ^ (p - 1) * cmod (∏i = 1..n. x - i) ^ p"
by (simp add: poly_f norm_mult norm_power)
also from x x' x'' have "… ≤ of_nat n ^ (p - 1) * C ^ p"
by (intro mult_mono C power_mono) simp_all
finally have "norm (poly (of_int_poly f) x) ≤ real n ^ (p - 1) * C ^ p" .
} note A = this
have "norm (I (of_nat k)) ≤
cmod (of_nat k) * exp (cmod (of_nat k)) * (of_nat n ^ (p - 1) * C ^ p)"
by (intro lindemann_weierstrass_integral_bound[OF _ A]
C mult_nonneg_nonneg zero_le_power) auto
also have "… ≤ cmod (of_nat n) * exp (cmod (of_nat n)) * (of_nat n ^ (p - 1) * C ^ p)"
using k by (intro mult_mono zero_le_power mult_nonneg_nonneg C) simp_all
finally show "cmod (of_int (coeff q k) * I (of_nat k)) ≤
of_int qmax * (real n * exp (real n) * real n ^ (p - 1) * C ^ p)"
unfolding norm_mult
by (intro mult_mono) (simp_all add: qmax of_int_abs [symmetric] del: of_int_abs)
qed
also have "… = E * F ^ p" using p_pos
by (simp add: power_diff power_mult_distrib E_def F_def)
finally show "fact (p - 1) ≤ E * F ^ p" using J_lower by linarith
qed
have "(λn. E * F * F ^ (n - 1) / fact (n - 1)) ⇢ 0" (is ?P)
by (intro filterlim_compose[OF power_over_fact_tendsto_0' filterlim_minus_const_nat_at_top])
also have "?P ⟷ (λn. E * F ^ n / fact (n - 1)) ⇢ 0"
by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of "0::nat"]])
(auto simp: power_Suc [symmetric] simp del: power_Suc)
finally have "eventually (λn. E * F ^ n / fact (n - 1) < 1) at_top"
by (rule order_tendstoD) simp_all
hence "eventually (λn. E * F ^ n < fact (n - 1)) at_top" by eventually_elim simp
then obtain P where P: "⋀n. n ≥ P ⟹ E * F ^ n < fact (n - 1)"
by (auto simp: eventually_at_top_linorder)
have "∃p. prime p ∧ p > Max {nat (abs (coeff q 0)), n, P}" by (rule bigger_prime)
then obtain p where "prime p" "p > Max {nat (abs (coeff q 0)), n, P}" by blast
hence "int p > abs (coeff q 0)" "p > n" "p ≥ P" by auto
with ineq[of p] ‹prime p› have "fact (p - 1) ≤ E * F ^ p" by simp
moreover from ‹p ≥ P› have "fact (p - 1) > E * F ^ p" by (rule P)
ultimately show False by linarith
qed
corollary e_transcendental_real: "¬ algebraic (exp 1 :: real)"
proof -
have "¬algebraic (exp 1 :: complex)" by (rule e_transcendental_complex)
also have "(exp 1 :: complex) = of_real (exp 1)" using exp_of_real[of 1] by simp
also have "algebraic … ⟷ algebraic (exp 1 :: real)" by simp
finally show ?thesis .
qed
end