Theory Hermite_Lindemann
section ‹The Hermite--Lindemann--Weierstra\ss Transcendence Theorem›
theory Hermite_Lindemann
imports
Pi_Transcendental.Pi_Transcendental
Algebraic_Numbers.Algebraic_Numbers
Algebraic_Integer_Divisibility
More_Min_Int_Poly
Complex_Lexorder
More_Polynomial_HLW
More_Multivariate_Polynomial_HLW
More_Algebraic_Numbers_HLW
Misc_HLW
begin
hide_const (open) Henstock_Kurzweil_Integration.content Module.smult
text ‹
The Hermite--Lindemann--Weierstra\ss theorem answers questions about the transcendence of
the exponential function and other related complex functions. It proves that a large number of
combinations of exponentials is always transcendental.
A first (much weaker) version of the theorem was proven by Hermite. Lindemann and Weierstra\ss then
successively generalised it shortly afterwards, and finally Baker gave another, arguably more
elegant formulation (which is the one that we will prove, and then derive the traditional version
from it).
To honour the contributions of all three of these 19th-century mathematicians, I refer to the
theorem as the Hermite--Lindemann--Weierstra\ss theorem, even though in other literature it is
often called Hermite--Lindemann or Lindemann--Weierstra\ss. To keep things short, the Isabelle
name of the theorem, however, will omit Weierstra\ss's name.
›
subsection ‹Main proof›
text ‹
Following Baker, We first prove the following special form of the theorem:
Let $m > 0$ and $q_1, \ldots, q_m \in\mathbb{Z}[X]$ be irreducible, non-constant,
and pairwise coprime polynomials. Let $\beta_1, \ldots, \beta_m$ be non-zero integers. Then
\[\sum_{i=1}^m \beta_i \sum_{q_i(\alpha) = 0} e^\alpha \neq 0\]
The difference to the final theorem is that
▸ The coefficients $\beta_i$ are non-zero integers (as opposed to arbitrary algebraic numbers)
▸ The exponents $\alpha_i$ occur in full sets of conjugates, and each set has the same
coefficient.
In a similar fashion to the proofs of the transcendence of ‹e› and ‹π›, we define some number
$J$ depending on the $\alpha_i$ and $\beta_i$ and an arbitrary sufficiently large prime ‹p›. We
then show that, on one hand, $J$ is an integer multiple of $(p-1)!$, but on the other hand it
is bounded from above by a term of the form $C_1 \cdot C_2^p$. This is then clearly a
contradiction if ‹p› is chosen large enough.
›
lemma Hermite_Lindemann_aux1:
fixes P :: "int poly set" and β :: "int poly ⇒ int"
assumes "finite P" and "P ≠ {}"
assumes distinct: "pairwise Rings.coprime P"
assumes irred: "⋀p. p ∈ P ⟹ irreducible p"
assumes nonconstant: "⋀p. p ∈ P ⟹ Polynomial.degree p > 0"
assumes β_nz: "⋀p. p ∈ P ⟹ β p ≠ 0"
defines "Roots ≡ (λp. {α::complex. poly (of_int_poly p) α = 0})"
shows "(∑p∈P. of_int (β p) * (∑α∈Roots p. exp α)) ≠ 0"
proof
note [intro] = ‹finite P›
assume sum_eq_0: "(∑p∈P. of_int (β p) * (∑α∈Roots p. exp α)) = 0"
define Roots' where "Roots' = (⋃p∈P. Roots p)"
have finite_Roots [intro]: "finite (Roots p)" if "p ∈ P" for p
using nonconstant[of p] that by (auto intro: poly_roots_finite simp: Roots_def)
have [intro]: "finite Roots'"
by (auto simp: Roots'_def)
have [simp]: "0 ∉ P"
using nonconstant[of 0] by auto
have [simp]: "p ≠ 0" if "p ∈ P" for p
using that by auto
text ‹
The polynomials in \<^term>‹P› do not have multiple roots:
›
have rsquarefree: "rsquarefree (of_int_poly q :: complex poly)" if "q ∈ P" for q
by (rule irreducible_imp_rsquarefree_of_int_poly) (use that in ‹auto intro: irred nonconstant›)
text ‹
No two different polynomials in \<^term>‹P› have roots in common:
›
have disjoint: "disjoint_family_on Roots P"
using distinct
proof (rule pairwise_imp_disjoint_family_on)
fix p q assume P: "p ∈ P" "q ∈ P" and "Rings.coprime p q"
hence "Rings.coprime (of_int_poly p :: complex poly) (of_int_poly q)"
by (intro coprime_of_int_polyI)
thus "Roots p ∩ Roots q = {}"
using poly_eq_0_coprime[of "of_int_poly p" "of_int_poly q :: complex poly"] P
by (auto simp: Roots_def)
qed
define n_roots :: "int poly ⇒ nat" ("♯_")
where "n_roots = (λp. card (Roots p))"
define n where "n = (∑p∈P. ♯p)"
have n_altdef: "n = card Roots'"
unfolding n_def Roots'_def n_roots_def using disjoint
by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
have Roots_nonempty: "Roots p ≠ {}" if "p ∈ P" for p
using nonconstant[OF that] by (auto simp: Roots_def fundamental_theorem_of_algebra constant_degree)
have "Roots' ≠ {}"
using Roots_nonempty ‹P ≠ {}› by (auto simp: Roots'_def)
have "n > 0"
using ‹Roots' ≠ {}› ‹finite Roots'› by (auto simp: n_altdef)
text ‹
We can split each polynomial in ‹P› into a product of linear factors:
›
have of_int_poly_P:
"of_int_poly q = Polynomial.smult (Polynomial.lead_coeff q) (∏x∈Roots q. [:-x, 1:])"
if "q ∈ P" for q
using complex_poly_decompose_rsquarefree[OF rsquarefree[OF that]] by (simp add: Roots_def)
text ‹
We let ‹l› be an integer such that $l\alpha$ is an algebraic integer for all our roots ‹α›:
›
define l where "l = (LCM q∈P. Polynomial.lead_coeff q)"
have alg_int: "algebraic_int (of_int l * x)" if "x ∈ Roots'" for x
proof -
from that obtain q where q: "q ∈ P" "ipoly q x = 0"
by (auto simp: Roots'_def Roots_def)
show ?thesis
by (rule algebraic_imp_algebraic_int'[of q]) (use q in ‹auto simp: l_def›)
qed
have "l ≠ 0"
using ‹finite P› by (auto simp: l_def Lcm_0_iff)
moreover have "l ≥ 0"
unfolding l_def by (rule Lcm_int_greater_eq_0)
ultimately have "l > 0" by linarith
text ‹
We can split the product of all the polynomials in ‹P› into linear factors:
›
define lc_factor where "lc_factor = (∏q∈P. l ^ Polynomial.degree q div Polynomial.lead_coeff q)"
have lc_factor: "Polynomial.smult (of_int l ^ n) (∏α'∈Roots'. [:-α',1:]) =
of_int_poly (Polynomial.smult lc_factor (∏P))"
proof -
define lc where "lc = (λq. Polynomial.lead_coeff q :: int)"
define d where "d = (Polynomial.degree :: int poly ⇒ nat)"
have "(∏q∈P. of_int_poly q) =
(∏q∈P. Polynomial.smult (lc q) (∏x∈Roots q. [:-x, 1:]) :: complex poly)"
unfolding lc_def by (intro prod.cong of_int_poly_P refl)
also have "… = Polynomial.smult (∏q∈P. lc q) (∏q∈P. (∏x∈Roots q. [:-x, 1:]))"
by (simp add: prod_smult)
also have "(∏q∈P. (∏x∈Roots q. [:-x, 1:])) = (∏x∈Roots'. [:-x, 1:])"
unfolding Roots'_def using disjoint
by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
also have "Polynomial.smult (of_int lc_factor) (Polynomial.smult (∏q∈P. lc q) …) =
Polynomial.smult (∏q∈P. of_int (l ^ d q div lc q * lc q)) (∏x∈Roots'. pCons (- x) 1)"
by (simp add: lc_factor_def prod.distrib lc_def d_def)
also have "(∏q∈P. of_int (l ^ d q div lc q * lc q)) = (∏q∈P. of_int l ^ d q :: complex)"
proof (intro prod.cong, goal_cases)
case (2 q)
have "lc q dvd l"
unfolding l_def lc_def using 2 by auto
also have "… dvd l ^ d q"
using 2 nonconstant[of q] by (intro dvd_power) (auto simp: d_def)
finally show ?case by simp
qed auto
also have "… = l ^ (∑q∈P. d q)"
by (simp add: power_sum)
also have "(∑q∈P. d q) = (∑q∈P. n_roots q)"
proof (intro sum.cong, goal_cases)
case (2 q)
thus ?case using rsquarefree[OF 2]
by (subst (asm) rsquarefree_card_degree) (auto simp: d_def n_roots_def Roots_def)
qed auto
also have "… = n"
by (simp add: n_def)
finally show ?thesis
by (simp add: of_int_hom.map_poly_hom_smult of_int_poly_hom.hom_prod)
qed
text ‹
We define ‹R› to be the radius of the smallest circle around the origin in which all our
roots lie:
›
define R :: real where "R = Max (norm ` Roots')"
have R_ge: "R ≥ norm α" if "α ∈ Roots'" for α
unfolding R_def using that by (intro Max_ge) auto
have "R ≥ 0"
proof -
from ‹Roots' ≠ {}› obtain α where "α ∈ Roots'"
by auto
have "0 ≤ norm α"
by simp
also have "… ≤ R"
by (intro R_ge) fact
finally show "R ≥ 0"
by simp
qed
text ‹
Now the main part of the proof: for any sufficiently large prime ‹p›, our assumptions
imply $(p-1)! ^ n \leq C' l^{np} (2R)^{np-1}$ for some constant $C'$:
›
define C :: "nat ⇒ real" where "C = (λp. l ^ (n * p) * (2*R) ^ (n * p - 1))"
define C' where
"C' = (∏x∈Roots'. ∑q∈P. real_of_int ¦β q¦ * (∑α∈Roots q. cmod α * exp (cmod α)))"
text ‹
We commence with the proof of the main inequality.
›
have ineq: "fact (p - 1) ^ n ≤ C' * C p ^ n"
if p: "prime p"
and p_ineqs: "∀q∈P. p > ¦β q¦"
"real p > norm (∏α∈Roots'. of_int (l^n) * (∏x∈Roots'-{α}. α - x))"
for p :: nat
proof -
have "p > 1"
using prime_gt_1_nat[OF p] .
text ‹
We define the polynomial function
\[f_i(X) = l^{np} \frac{\prod_\alpha (X-\alpha)^p}{X - \alpha_i}\]
where the product runs over all roots $\alpha$.
›
define f_poly :: "complex ⇒ complex poly" where
"f_poly = (λα. Polynomial.smult (l^(n*p)) ((∏α'∈Roots'. [:-α', 1:]^p) div [:-α, 1:]))"
have f_poly_altdef: "f_poly α = Polynomial.smult (l^(n*p))
((∏α'∈Roots'. [:-α', 1:]^(if α' = α then p - 1 else p)))"
if "α ∈ Roots'" for α
proof -
have "(∏α'∈Roots'. [:-α', 1:] ^ (if α'=α then p-1 else p)) * [:-α, 1:] =
[:- α, 1:] ^ (p - 1) * (∏x∈Roots' - {α}. [:- x, 1:] ^ p) * [:- α, 1:]"
using that by (subst prod.If_eq) (auto simp: algebra_simps)
also have "… = (∏x∈Roots' - {α}. [:- x, 1:] ^ p) * [:- α, 1:] ^ Suc (p - 1)"
by (simp only: power_Suc mult_ac)
also have "Suc (p - 1) = p"
using ‹p > 1› by auto
also have "(∏x∈Roots' - {α}. [:- x, 1:] ^ p) * [:- α, 1:] ^ p = (∏x∈Roots'. [:- x, 1:] ^ p)"
using that by (subst prod.remove[of _ α]) auto
finally have eq: "(∏α'∈Roots'. [:-α', 1:] ^ (if α'=α then p-1 else p)) * [:-α, 1:] =
(∏x∈Roots'. [:- x, 1:] ^ p)" .
show ?thesis
unfolding f_poly_def eq[symmetric] by (subst nonzero_mult_div_cancel_right) auto
qed
define f :: "complex ⇒ complex ⇒ complex"
where "f = (λα x. l^(n*p) * (∏α'∈Roots'. (x - α')^(if α' = α then p - 1 else p)))"
have eval_f: "poly (f_poly α) x = f α x" if "α ∈ Roots'" for α x
using that by (simp add: f_poly_altdef poly_prod f_def)
have deg_f: "Polynomial.degree (f_poly α) = n * p - 1" if "α ∈ Roots'" for α
proof -
have "Polynomial.degree (f_poly α) = p - 1 + (n - 1) * p"
unfolding f_poly_altdef[OF that] using that ‹l > 0› ‹finite Roots'›
by (subst prod.If_eq) (auto simp: degree_prod_sum_eq degree_power_eq degree_mult_eq n_altdef)
also have "p - 1 + (n - 1) * p = n * p - 1"
using ‹n > 0› ‹p > 1› by (cases n) auto
finally show ?thesis .
qed
text ‹
Next, we define the function $I_i(z) = \int_0^z e^{z-t} f_i(t) \text{d}t$, and,
based on that, the numbers $J_i = \sum_{i=1}^m \beta_i \sum_{q_i(x) = 0} I_i(x)$,
and the number $J$, which is the product of all the $J_i$:
›
define I :: "complex ⇒ complex ⇒ complex"
where "I = (λα x. lindemann_weierstrass_aux.I (f_poly α) x)"
define J :: "complex ⇒ complex"
where "J = (λα. ∑q∈P. β q * (∑x∈Roots q. I α x))"
define J' :: complex
where "J' = (∏α∈Roots'. J α)"
text ‹
Reusing some of the machinery from the proof that ‹e› is transcendental,
we find the following equality for $J_i$:
›
have J_eq: "J α = -(∑q∈P. of_int (β q) * (∑x∈Roots q. ∑j<n*p. poly ((pderiv ^^ j) (f_poly α)) x))"
if "α ∈ Roots'" for α
proof -
have "n * p ≥ 1 * 2"
using ‹n > 0› ‹p > 1› by (intro mult_mono) auto
hence [simp]: "{..n*p-Suc 0} = {..<n*p}"
by auto
have "J α = (∑q∈P. β q * (∑x∈Roots q. I α x))"
unfolding J_def ..
also have "… = (∑q∈P. of_int (β q) * (∑x∈Roots q. exp x * (∑j<n*p. poly ((pderiv ^^ j) (f_poly α)) 0))) -
(∑q∈P. of_int (β q) * (∑x∈Roots q. ∑j<n*p. poly ((pderiv ^^ j) (f_poly α)) x))"
unfolding I_def lindemann_weierstrass_aux.I_def
by (simp add: deg_f that ring_distribs sum_subtractf sum_distrib_left sum_distrib_right mult_ac)
also have "… = -(∑q∈P. of_int (β q) * (∑x∈Roots q. ∑j<n*p. poly ((pderiv ^^ j) (f_poly α)) x))"
unfolding sum_distrib_right [symmetric] mult.assoc [symmetric] sum_eq_0 by simp
finally show ?thesis .
qed
text ‹
The next big step is to show that $(p-1)! \mid J_i$ as an algebraic integer (i.e.
$J_i / (p-1)!$ is an algebraic integer), but $p \not\mid J_i$. This is done by brute force:
We show that every summand in the above sum has $p!$ as a factor, except for
the one corresponding to $x = \alpha_i$, $j = p - 1$, which has $(p-1)!$ as a factor but
not ‹p›.
›
have J: "fact (p - 1) alg_dvd J α" "¬of_nat p alg_dvd J α" if α: "α ∈ Roots'" for α
proof -
define h where "h = (λα' j. poly ((pderiv ^^ j) (f_poly α)) α')"
from α obtain q where q: "q ∈ P" "α ∈ Roots q"
by (auto simp: Roots'_def)
have "J α = -(∑(q, α')∈Sigma P Roots. ∑j<n*p. of_int (β q) * h α' j)"
unfolding J_eq[OF α] h_def sum_distrib_left by (subst (2) sum.Sigma) auto
also have "… = -(∑((q,α'),i)∈Sigma P Roots×{..<n*p}. of_int (β q) * h α' i)"
by (subst (2) sum.Sigma [symmetric]) (auto simp: case_prod_unfold)
finally have J_eq': "J α = - (∑((q, α'), i)∈Sigma P Roots × {..<n * p}. of_int (β q) * h α' i)" .
have h_α_pm1_eq: "h α (p-1) = of_int (l^(n*p)) * fact (p-1) * (∏α'∈Roots'-{α}. (α-α')^p)"
proof -
have "h α (p - 1) = of_int (l ^ (n * p)) *
poly ((pderiv ^^ (p-1)) (∏α'∈Roots'. [:-α',1:] ^ (if α' = α then p - 1 else p))) α"
unfolding h_def f_poly_altdef[OF α] higher_pderiv_smult poly_smult ..
also have "(∏α'∈Roots'. [:-α',1:] ^ (if α' = α then p - 1 else p)) =
[:-α,1:]^(p-1) * (∏α'∈Roots'-{α}. [:-α',1:]^p)"
using α by (subst prod.If_eq) auto
also have "poly ((pderiv ^^ (p-1)) …) α = fact (p - 1) * (∏α'∈Roots' - {α}. (α - α') ^ p)"
by (subst poly_higher_pderiv_aux2) (simp_all add: poly_prod)
finally show ?thesis by (simp only: mult.assoc)
qed
have "fact (p-1) alg_dvd h α (p-1)"
proof -
have "fact (p-1) alg_dvd fact (p-1) * (of_int (l^p) * (∏α'∈Roots'-{α}. (l*α-l*α')^p))"
by (intro alg_dvd_triv_left algebraic_int_times[of "of_int (l^p)"]
algebraic_int_prod algebraic_int_power algebraic_int_diff
alg_int α algebraic_int_of_int) auto
also have "(∏α'∈Roots'-{α}. (l*α-l*α')^p) = (∏α'∈Roots'-{α}. of_int l^p * (α-α')^p)"
by (subst power_mult_distrib [symmetric]) (simp_all add: algebra_simps)
also have "… = of_int (l ^ (p * (n-1))) * (∏α'∈Roots'-{α}. (α-α')^p)"
using α by (subst prod.distrib) (auto simp: card_Diff_subset n_altdef simp flip: power_mult)
also have "of_int (l^p) * … = of_int (l^(p+p*(n-1))) * (∏α'∈Roots'-{α}. (α-α')^p)"
unfolding mult.assoc [symmetric] power_add [symmetric] of_int_power ..
also have "p + p * (n - 1) = n * p"
using ‹n > 0› by (cases n) (auto simp: mult_ac)
also have "fact (p - 1) * (of_int (l^(n*p)) * (∏α'∈Roots'-{α}. (α-α')^p)) = h α (p-1)"
unfolding h_α_pm1_eq by (simp add: mult_ac)
finally show ?thesis .
qed
have "¬of_nat p alg_dvd of_int (β q) * h α (p-1)"
unfolding h_α_pm1_eq mult.assoc [symmetric] of_int_mult [symmetric]
proof
define r where "r = (λα. of_int (l^n) * (∏α'∈Roots'-{α}. α-α'))"
have alg_int_r: "algebraic_int (r α)" if "α ∈ Roots'" for α
proof -
have "algebraic_int (of_int l * (∏α'∈Roots'-{α}. of_int l * α - of_int l * α'))"
by (intro algebraic_int_times[OF algebraic_int_of_int] algebraic_int_prod
algebraic_int_power algebraic_int_diff alg_int that) auto
also have "… = of_int l * (∏α'∈Roots'-{α}. of_int l * (α - α'))"
by (simp add: algebra_simps flip: power_mult_distrib)
also have "… = of_int (l^(1 + (n-1))) * (∏α'∈Roots'-{α}. α - α')"
using that by (simp add: r_def prod.distrib card_Diff_subset
n_altdef power_add mult_ac flip: power_mult)
also have "1 + (n - 1) = n"
using ‹n > 0› by auto
finally show "algebraic_int (r α)"
unfolding r_def .
qed
have "(∏α'∈Roots'. r α') ∈ ℚ"
proof -
obtain Root where Root_bij: "bij_betw Root {..<n} Roots'"
using ex_bij_betw_nat_finite[OF ‹finite Roots'›] unfolding n_altdef atLeast0LessThan by metis
have Root_in_Roots': "Root i ∈ Roots'" if "i < n" for i
using Root_bij that by (auto simp: bij_betw_def)
define R :: "complex mpoly" where
"R = (∏i<n. Const (of_int (l^n)) * (∏j∈{..<n}-{i}. Var i - Var j))"
have "insertion Root R ∈ ℚ"
proof (rule symmetric_poly_of_roots_in_subring)
show "symmetric_mpoly {..<n} R"
unfolding R_def
proof (rule symmetric_mpoly_symmetric_prod'[of _ "λπ. π"], goal_cases)
case (2 i π)
from ‹π permutes {..<n}› have [simp]: "bij π"
by (rule permutes_bij)
have "mpoly_map_vars π (Const (of_int (l ^ n)) *
(∏j∈{..<n} - {i}. Var i - Var j):: complex mpoly) =
Const (of_int l ^ n) * (∏j∈{..<n} - {i}. Var (π i) - Var (π j))"
by simp
also have "(∏j∈{..<n} - {i}. Var (π i) - Var (π j)) =
(∏j∈{..<n} - {π i}. Var (π i) - Var j)"
using 2 permutes_in_image[OF 2(2), of i]
by (intro prod.reindex_bij_betw bij_betw_Diff permutes_imp_bij[OF 2(2)])
(auto simp: bij_betw_singleton)
finally show ?case by simp
qed
next
show "vars R ⊆ {..<n}" unfolding R_def
by (intro order.trans[OF vars_prod] UN_least order.trans[OF vars_mult]
Un_least order.trans[OF vars_power] order.trans[OF vars_diff])
(auto simp: vars_Var)
next
show "ring_closed (ℚ :: complex set)"
by unfold_locales auto
then interpret ring_closed "ℚ :: complex set" .
show "∀m. MPoly_Type.coeff R m ∈ ℚ"
unfolding R_def
by (intro allI coeff_prod_closed coeff_mult_closed coeff_power_closed)
(auto simp: mpoly_coeff_Const coeff_Var when_def)
next
let ?lc = "of_int (∏p∈P. Polynomial.lead_coeff p) :: complex"
have "(∏q∈P. of_int_poly q) = (∏q∈P. Polynomial.smult
(of_int (Polynomial.lead_coeff q)) (∏x∈Roots q. [:-x, 1:]))"
by (intro prod.cong of_int_poly_P refl)
also have "… = Polynomial.smult ?lc (∏q∈P. ∏x∈Roots q. [:-x, 1:])"
by (simp add: prod_smult)
also have "(∏q∈P. ∏x∈Roots q. [:-x, 1:]) = (∏x∈Roots'. [:-x, 1:])"
unfolding Roots'_def using disjoint
by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
also have "… = (∏i<n. [:- Root i, 1:])"
by (intro prod.reindex_bij_betw [symmetric] Root_bij)
finally show "of_int_poly (∏P) = Polynomial.smult ?lc (∏i<n. [:- Root i, 1:])"
by (simp add: of_int_poly_hom.hom_prod)
have "prod Polynomial.lead_coeff P ≠ 0"
by (intro prod_nonzeroI) auto
thus "inverse ?lc * ?lc = 1" "inverse ?lc ∈ ℚ"
by (auto simp: field_simps simp flip: of_int_prod)
qed auto
also have "insertion Root R = (∏i<n. of_int (l^n) * (∏j∈{..<n}-{i}. Root i - Root j))"
by (simp add: R_def insertion_prod insertion_mult insertion_power insertion_diff)
also have "… = (∏i<n. of_int (l^n) * (∏α'∈Roots'-{Root i}. Root i - α'))"
proof (intro prod.cong, goal_cases)
case (2 i)
hence "(∏j∈{..<n}-{i}. Root i - Root j) = (∏α'∈Roots'-{Root i}. Root i - α')"
by (intro prod.reindex_bij_betw bij_betw_Diff Root_bij)
(auto intro: Root_in_Roots' simp: bij_betw_singleton)
thus ?case by simp
qed auto
also have "… = (∏α'∈Roots'. r α')"
unfolding r_def by (intro prod.reindex_bij_betw Root_bij)
finally show "(∏α'∈Roots'. r α') ∈ ℚ" .
qed
moreover have "algebraic_int (∏α'∈Roots'. r α')"
by (intro algebraic_int_prod alg_int_r)
ultimately have is_int: "(∏α'∈Roots'. r α') ∈ ℤ"
using rational_algebraic_int_is_int by blast
then obtain R' where R': "(∏α'∈Roots'. r α') = of_int R'"
by (elim Ints_cases)
have "(∏α'∈Roots'. r α') ≠ 0"
using ‹l > 0› by (intro prod_nonzeroI) (auto simp: r_def ‹finite Roots'›)
with R' have [simp]: "R' ≠ 0"
by auto
assume "of_nat p alg_dvd of_int (β q * l^(n*p)) * fact (p-1) * (∏α'∈Roots'-{α}. (α-α') ^ p)"
also have "… = of_int (β q) * fact (p-1) * r α ^ p"
by (simp add: r_def mult_ac power_mult_distrib power_mult prod_power_distrib)
also have "… alg_dvd of_int (β q) * fact (p-1) * r α ^ p * (∏α'∈Roots'-{α}. r α') ^ p"
by (intro alg_dvd_triv_left algebraic_int_prod alg_int_r algebraic_int_power) auto
also have "… = of_int (β q) * fact (p-1) * (∏α'∈Roots'. r α') ^ p"
using α by (subst (2) prod.remove[of _ "α"]) (auto simp: mult_ac power_mult_distrib)
also have "… = of_int (β q * fact (p - 1) * R' ^ p)"
by (simp add: R')
also have "of_nat p = of_int (int p)"
by simp
finally have "int p dvd β q * fact (p - 1) * R' ^ p"
by (subst (asm) alg_dvd_of_int_iff)
moreover have "prime (int p)"
using ‹prime p› by auto
ultimately have "int p dvd β q ∨ int p dvd fact (p - 1) ∨ int p dvd R' ^ p"
by (simp add: prime_dvd_mult_iff)
moreover have "¬int p dvd β q"
proof
assume "int p dvd β q"
hence "int p ≤ ¦β q¦"
using β_nz[of q] dvd_imp_le_int[of "β q" "int p"] q by auto
with p_ineqs(1) q show False by auto
qed
moreover have "¬int p dvd fact (p - 1)"
proof -
have "¬p dvd fact (p - 1)"
using ‹p > 1› p by (subst prime_dvd_fact_iff) auto
hence "¬int p dvd int (fact (p - 1))"
by (subst int_dvd_int_iff)
thus ?thesis unfolding of_nat_fact .
qed
moreover have "¬int p dvd R' ^ p"
proof
assume "int p dvd R' ^ p"
hence "int p dvd R'"
using ‹prime (int p)› prime_dvd_power by metis
hence "int p ≤ ¦R'¦"
using β_nz[of q] dvd_imp_le_int[of R' "int p"] q by auto
hence "real p ≤ real_of_int ¦R'¦"
by linarith
also have "… = norm (∏α∈Roots'. r α)"
unfolding R' by simp
finally show False unfolding r_def using p_ineqs(2)
by linarith
qed
ultimately show False
by blast
qed
have fact_p_dvd: "fact p alg_dvd h α' j" if "α' ∈ Roots'" "α' ≠ α ∨ j ≠ p - 1" for α' j
proof (cases "j ≥ p")
case False
with that have j: "j < (if α' = α then p - 1 else p)"
by auto
have "h α' j = 0"
unfolding h_def f_poly_altdef[OF α]
by (intro poly_higher_pderiv_aux1'[OF j] dvd_smult dvd_prodI that) auto
thus ?thesis by simp
next
case True
define e where "e = (λx. if x = α then p - 1 else p)"
define Q where "Q = (∏x∈Roots'. [:-x, 1:] ^ e x)"
define Q' where "Q' = Polynomial.smult (of_int (l^(n*p+j))) (pcompose Q [:0, 1 / of_int l:])"
have "poly ((pderiv ^^ j) Q) α' / l ^ j =
poly ((pderiv ^^ j) (pcompose Q [:0, 1 / of_int l:])) (l * α')"
using ‹l > 0› by (simp add: higher_pderiv_pcompose_linear poly_pcompose field_simps)
have "sum e Roots' = (n - 1) * p + (p - 1)"
unfolding e_def using α
by (subst sum.If_eq) (auto simp: card_Diff_subset n_altdef algebra_simps)
also have "… = n * p - 1"
using ‹n > 0› ‹p > 1› by (cases n) auto
finally have [simp]: "sum e Roots' = n * p - 1" .
have "h α' j = of_int (l^(n*p)) * poly ((pderiv ^^ j) Q) α'"
unfolding h_def f_poly_altdef[OF α] higher_pderiv_smult poly_smult e_def Q_def ..
also have "poly ((pderiv ^^ j) Q) α' =
of_int l ^ j * poly ((pderiv ^^ j) (pcompose Q [:0, 1 / of_int l:])) (l * α')"
using ‹l > 0› by (simp add: higher_pderiv_pcompose_linear poly_pcompose field_simps)
also have "of_int (l ^ (n * p)) * … = poly ((pderiv ^^ j) Q') (l * α')"
by (simp add: Q'_def higher_pderiv_smult power_add)
also have "fact p alg_dvd …"
proof (rule fact_alg_dvd_poly_higher_pderiv)
show "j ≥ p" by fact
show "algebraic_int (of_int l * α')"
by (rule alg_int) fact
interpret alg_int: ring_closed "{x::complex. algebraic_int x}"
by standard auto
show "algebraic_int (poly.coeff Q' i)" for i
proof (cases "i ≤ Polynomial.degree Q'")
case False
thus ?thesis
by (simp add: coeff_eq_0)
next
case True
hence "i ≤ n * p - 1" using ‹l > 0›
by (simp add: Q'_def degree_prod_sum_eq Q_def degree_power_eq)
also have "n * p > 0"
using ‹n > 0› ‹p > 1› by auto
hence "n * p - 1 < n * p"
by simp
finally have i: "i < n * p" .
have "poly.coeff Q' i = of_int l ^ (n * p + j) / of_int l ^ i * poly.coeff Q i"
by (simp add: Q'_def coeff_pcompose_linear field_simps)
also have "of_int l ^ (n * p + j) = (of_int l ^ (n * p + j - i) :: complex) * of_int l ^ i"
unfolding power_add [symmetric] using i by simp
hence "of_int l ^ (n * p + j) / of_int l ^ i = (of_int l ^ (n * p + j - i) :: complex)"
using ‹l > 0› by (simp add: field_simps)
also have "… * poly.coeff Q i =
(∑X∈{X. X ⊆ (SIGMA x:Roots'. {..<e x}) ∧ i = n * p - Suc (card X)}.
of_int l ^ (n * p + j - (n * p - Suc (card X))) * ((- 1) ^ card X * prod fst X))"
unfolding Q_def by (subst coeff_prod_linear_factors) (auto simp: sum_distrib_left)
also have "algebraic_int …"
proof (intro algebraic_int_sum, goal_cases)
case (1 X)
hence X: "X ⊆ (SIGMA x:Roots'. {..<e x})"
by auto
have card_eq: "card (SIGMA x:Roots'. {..<e x}) = n * p - 1"
by (subst card_SigmaI) auto
from X have "card X ≤ card (SIGMA x:Roots'. {..<e x})"
by (intro card_mono) auto
hence "card X ≤ n * p - 1"
using card_eq by auto
also have "… < n * p"
using ‹n * p > 0› by simp
finally have card_less: "card X < n * p" .
have "algebraic_int ((-1) ^ card X * of_int l ^ (j + 1) * (∏x∈X. of_int l * fst x))"
using X by (intro algebraic_int_times algebraic_int_prod alg_int) auto
thus ?case
using card_less by (simp add: power_add prod.distrib mult_ac)
qed
finally show ?thesis .
qed
qed
finally show ?thesis .
qed
have p_dvd: "of_nat p alg_dvd h α' j" if "α' ∈ Roots'" "α' ≠ α ∨ j ≠ p - 1" for α' j
proof -
have "of_nat p alg_dvd (of_nat (fact p) :: complex)"
by (intro alg_dvd_of_nat dvd_fact) (use ‹p > 1› in auto)
hence "of_nat p alg_dvd (fact p :: complex)"
by simp
also have "… alg_dvd h α' j"
using that by (intro fact_p_dvd)
finally show ?thesis .
qed
show "fact (p - 1) alg_dvd J α"
unfolding J_eq'
proof (intro alg_dvd_uminus_right alg_dvd_sum, safe intro!: alg_dvd_mult algebraic_int_of_int)
fix q α' j
assume "q ∈ P" "α' ∈ Roots q" "j < n * p"
hence "α' ∈ Roots'"
by (auto simp: Roots'_def)
show "fact (p - 1) alg_dvd h α' j"
proof (cases "α' = α ∧ j = p - 1")
case True
thus ?thesis using ‹fact (p - 1) alg_dvd h α (p - 1)›
by simp
next
case False
have "of_int (fact (p - 1)) alg_dvd (of_int (fact p) :: complex)"
by (intro alg_dvd_of_int fact_dvd) auto
hence "fact (p - 1) alg_dvd (fact p :: complex)"
by simp
also have "… alg_dvd h α' j"
using False ‹α' ∈ Roots'› by (intro fact_p_dvd) auto
finally show ?thesis .
qed
qed
show "¬of_nat p alg_dvd J α"
unfolding J_eq' alg_dvd_uminus_right_iff
proof (rule not_alg_dvd_sum)
have "p - 1 < 1 * p"
using ‹p > 1› by simp
also have "1 * p ≤ n * p"
using ‹n > 0› by (intro mult_right_mono) auto
finally show "((q, α), p - 1) ∈ Sigma P Roots × {..<n*p}"
using q ‹n > 0› by auto
next
fix z assume z: "z ∈ Sigma P Roots × {..<n*p}-{((q,α),p-1)}"
from z have "snd (fst z) ∈ Roots'"
by (auto simp: Roots'_def)
moreover have "fst (fst z) = q" if "α ∈ Roots (fst (fst z))"
proof -
have "α ∈ Roots (fst (fst z)) ∩ Roots q" "q ∈ P" "fst (fst z) ∈ P"
using that q z by auto
with disjoint show ?thesis
unfolding disjoint_family_on_def by blast
qed
ultimately have "of_nat p alg_dvd h (snd (fst z)) (snd z)"
using z by (intro p_dvd) auto
thus "of_nat p alg_dvd (case z of (x, xa) ⇒ (case x of (q, α') ⇒ λi. of_int (β q) * h α' i) xa)"
using z by auto
qed (use ‹¬of_nat p alg_dvd of_int (β q) * h α (p-1)› in auto)
qed
text ‹
Our next goal is to show that $J$ is rational. This is done by repeated applications
of the fundamental theorem of symmetric polynomials, exploiting the fact that $J$ is
symmetric in all the $\alpha_i$ for each set of conjugates.
›
define g :: "int poly poly"
where "g = synthetic_div (map_poly (λx. [:x:])
((Polynomial.smult lc_factor (∏P)) ^ p)) [:0, 1:]"
have g: "map_poly (λp. ipoly p α) g = f_poly α" if α: "α ∈ Roots'" for α
proof -
interpret α: comm_ring_hom "λp. ipoly p α"
by standard (auto simp: of_int_hom.poly_map_poly_eval_poly of_int_poly_hom.hom_mult)
define Q :: "int poly" where "Q = (Polynomial.smult lc_factor (∏P)) ^ p"
have "f_poly α = Polynomial.smult (of_int (l^(n*p))) ((∏α'∈Roots'. [:-α',1:])^p) div [:-α,1:]"
unfolding f_poly_def div_smult_left [symmetric] prod_power_distrib[symmetric] ..
also have "of_int (l^(n*p)) = (of_int l^n)^p"
by (simp add: power_mult)
also have "Polynomial.smult … ((∏α'∈Roots'. [:-α',1:])^p) =
(Polynomial.smult (of_int l ^ n) (∏α'∈Roots'. [:-α',1:])) ^ p"
by (simp only: smult_power)
also have "… = of_int_poly Q"
by (subst lc_factor) (simp_all add: Q_def of_int_poly_hom.hom_power)
also have "… div [:-α, 1:] = synthetic_div (of_int_poly Q) α"
unfolding synthetic_div_altdef ..
also have "… = synthetic_div (map_poly (λp. ipoly p α) (map_poly (λx. [:x:]) Q)) (ipoly [:0, 1:] α)"
by (simp add: map_poly_map_poly o_def)
also have "… = map_poly (λp. ipoly p α) g"
unfolding g_def Q_def by (rule α.synthetic_div_hom)
finally show ?thesis ..
qed
obtain Q where Q: "J α = -(∑q∈P. of_int (β q) * eval_poly of_rat (Q q) α)"
if "α ∈ Roots'" for α
proof -
define g' :: "nat ⇒ complex poly poly"
where "g' = (λj. (map_poly of_int_poly ((pderiv ^^ j) g)))"
obtain root :: "int poly ⇒ nat ⇒ complex"
where root: "⋀q. q ∈ P ⟹ bij_betw (root q) {..<♯q} (Roots q)"
using ex_bij_betw_nat_finite[OF finite_Roots] unfolding n_roots_def atLeast0LessThan
by metis
have "∃Q'. map_poly of_rat Q' = (∑x∈Roots q. poly (g' j) [:x:])" if q: "q ∈ P" for q j
proof -
define Q :: "nat ⇒ complex poly mpoly"
where "Q = (λj. (∑i<♯q. mpoly_of_poly i (g' j)))"
define ratpolys :: "complex poly set" where "ratpolys = {p. ∀i. poly.coeff p i ∈ ℚ}"
have "insertion ((λx. [:x:]) ∘ root q) (Q j) ∈ ratpolys"
proof (rule symmetric_poly_of_roots_in_subring)
show "ring_closed ratpolys"
by standard (auto simp: ratpolys_def intro!: coeff_mult_semiring_closed)
show "∀m. MPoly_Type.coeff (Q j) m ∈ ratpolys"
by (auto simp: Q_def ratpolys_def Polynomial.coeff_sum coeff_mpoly_of_poly when_def g'_def
intro!: sum_in_Rats)
show "vars (Q j) ⊆ {..<♯q}" unfolding Q_def
by (intro order.trans[OF vars_sum] UN_least order.trans[OF vars_mpoly_of_poly]) auto
show "symmetric_mpoly {..<♯q} (Q j)" unfolding Q_def
by (rule symmetric_mpoly_symmetric_sum[of _ id]) (auto simp: permutes_bij)
interpret coeff_lift_hom: map_poly_idom_hom "λx. [:x:]"
by standard
define lc :: complex where "lc = of_int (Polynomial.lead_coeff q)"
have "of_int_poly q = Polynomial.smult (Polynomial.lead_coeff q) (∏x∈Roots q. [:-x, 1:])"
by (rule of_int_poly_P) fact
also have "poly_lift … = Polynomial.smult [:lc:] (∏a∈Roots q. [:-[:a:], 1:])"
by (simp add: poly_lift_def map_poly_smult coeff_lift_hom.hom_prod lc_def)
also have "(∏a∈Roots q. [:-[:a:], 1:]) = (∏i<♯q. [:-[:root q i:], 1:])"
by (intro prod.reindex_bij_betw [symmetric] root q)
also have "… = (∏i<♯q. [:- ((λx. [:x:]) ∘ root q) i, 1:])"
by simp
finally show "poly_lift (Ring_Hom_Poly.of_int_poly q) = Polynomial.smult [:lc:] …" .
have "lc ≠ 0"
using q by (auto simp: lc_def)
thus "[:inverse lc:] * [:lc:] = 1"
by (simp add: field_simps)
qed (auto simp: ratpolys_def coeff_pCons split: nat.splits)
also have "insertion ((λx. [:x:]) ∘ root q) (Q j) = (∑i<♯q. poly (g' j) [:root q i:])"
by (simp add: Q_def insertion_sum poly_sum)
also have "… = (∑x∈Roots q. poly (g' j) [:x:])"
by (intro sum.reindex_bij_betw root q)
finally have "∀i. poly.coeff (∑x∈Roots q. poly (g' j) [:x:]) i ∈ ℚ"
by (auto simp: ratpolys_def)
thus ?thesis
using ratpolyE by metis
qed
then obtain Q where Q: "⋀q j. q ∈ P ⟹ map_poly of_rat (Q q j) = (∑x∈Roots q. poly (g' j) [:x:])"
by metis
define Q' where "Q' = (λq. ∑j<n*p. Q q j)"
have "J α = - (∑q∈P. of_int (β q) * eval_poly of_rat (Q' q) α)" if α: "α ∈ Roots'" for α
proof -
have "J α = -(∑q∈P. of_int (β q) * (∑x∈Roots q. ∑j<n * p. poly ((pderiv ^^ j) (f_poly α)) x))"
(is "_ = -?S") unfolding J_eq[OF α] ..
also have "?S = (∑q∈P. of_int (β q) * eval_poly of_rat (Q' q) α)"
proof (rule sum.cong, goal_cases)
case q: (2 q)
interpret α: idom_hom "λp. ipoly p α"
by standard (auto simp: of_int_hom.poly_map_poly_eval_poly of_int_poly_hom.hom_mult)
have "(∑x∈Roots q. ∑j<n * p. poly ((pderiv ^^ j) (f_poly α)) x) =
(∑j<n * p. ∑x∈Roots q. poly ((pderiv ^^ j) (f_poly α)) x)"
by (rule sum.swap)
also have "… = (∑j<n * p. eval_poly of_rat (Q q j) α)"
proof (rule sum.cong, goal_cases)
case j: (2 j)
have "(∑x∈Roots q. poly ((pderiv ^^ j) (f_poly α)) x) =
(∑x∈Roots q. poly (poly (g' j) [:x:]) α)"
proof (rule sum.cong, goal_cases)
case (2 x)
have "poly ((pderiv ^^ j) (f_poly α)) x =
poly ((pderiv ^^ j) (map_poly (λp. ipoly p α) g)) x"
by (subst g[OF α, symmetric]) (rule refl)
also have "… = poly (eval_poly ((λp. [:poly p α:]) ∘ of_int_poly) ((pderiv ^^ j) g) [:0, 1:]) x"
unfolding o_def α.map_poly_higher_pderiv [symmetric]
by (simp only: α.map_poly_eval_poly)
also have "… = poly (eval_poly (λp. [:poly p α:])
(map_poly of_int_poly ((pderiv ^^ j) g)) [:0, 1:]) x"
unfolding eval_poly_def by (subst map_poly_map_poly) auto
also have "… = poly (poly (map_poly of_int_poly ((pderiv ^^ j) g)) [:x:]) α"
by (rule poly_poly_eq [symmetric])
also have "… = poly (poly (g' j) [:x:]) α"
by (simp add: g'_def)
finally show ?case .
qed auto
also have "… = poly (∑x∈Roots q. poly (g' j) [:x:]) α"
by (simp add: poly_sum)
also have "… = eval_poly of_rat (Q q j) α"
using q by (simp add: Q eval_poly_def)
finally show ?case .
qed auto
also have "… = eval_poly of_rat (Q' q) α"
by (simp add: Q'_def of_rat_hom.eval_poly_sum)
finally show ?case by simp
qed auto
finally show "J α = - (∑q∈P. of_int (β q) * eval_poly of_rat (Q' q) α)" .
qed
thus ?thesis using that[of Q'] by metis
qed
have "J' ∈ ℚ"
proof -
have "(∏α∈Roots q. J α) ∈ ℚ" if q: "q ∈ P" for q
proof -
obtain root where root: "bij_betw root {..<♯q} (Roots q)"
using ex_bij_betw_nat_finite[OF finite_Roots[OF q]]
unfolding atLeast0LessThan n_roots_def by metis
define Q' :: "complex poly"
where "Q' = -(∑q∈P. Polynomial.smult (of_int (β q)) (map_poly of_rat (Q q)))"
have "(∏α∈Roots q. J α) = (∏α∈Roots q. -(∑q∈P. of_int (β q) * eval_poly of_rat (Q q) α))"
by (intro prod.cong refl Q) (auto simp: Roots'_def q)
also have "… = (∏α∈Roots q. poly Q' α)"
by (simp add: Q'_def poly_sum eval_poly_def)
also have "… = (∏i<♯q. poly Q' (root i))"
by (intro prod.reindex_bij_betw [symmetric] root)
also have "… = insertion root (∏i<♯q. mpoly_of_poly i Q')"
by (simp add: insertion_prod)
also have "… ∈ ℚ"
proof (rule symmetric_poly_of_roots_in_subring)
show "ring_closed (ℚ :: complex set)"
by standard auto
then interpret Q: ring_closed "ℚ :: complex set" .
show "∀m. MPoly_Type.coeff (∏i<♯q. mpoly_of_poly i Q') m ∈ ℚ"
by (auto intro!: Q.coeff_prod_closed sum_in_Rats
simp: coeff_mpoly_of_poly when_def Q'_def Polynomial.coeff_sum)
show "symmetric_mpoly {..<♯q} (∏i<♯q. mpoly_of_poly i Q')"
by (intro symmetric_mpoly_symmetric_prod'[of _ id]) (auto simp: permutes_bij)
show "vars (∏i<♯q. mpoly_of_poly i Q') ⊆ {..<♯q}"
by (intro order.trans[OF vars_prod] order.trans[OF vars_mpoly_of_poly] UN_least) auto
define lc where "lc = (of_int (Polynomial.lead_coeff q) :: complex)"
have "of_int_poly q = Polynomial.smult lc (∏x∈Roots q. [:- x, 1:])"
unfolding lc_def by (rule of_int_poly_P) fact
also have "(∏x∈Roots q. [:- x, 1:]) = (∏i<♯q. [:- root i, 1:])"
by (intro prod.reindex_bij_betw [symmetric] root)
finally show "of_int_poly q = Polynomial.smult lc (∏i<♯q. [:- root i, 1:])" .
have "lc ≠ 0"
using q by (auto simp: lc_def)
thus "inverse lc * lc = 1" "inverse lc ∈ ℚ"
by (auto simp: lc_def)
qed auto
finally show ?thesis .
qed
hence "(∏q∈P. ∏α∈Roots q. J α) ∈ ℚ"
by (rule Rats_prod)
also have "(∏q∈P. ∏α∈Roots q. J α) = J'"
unfolding Roots'_def J'_def using disjoint
by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
finally show "J' ∈ ℚ" .
qed
text ‹
Since ‹J'› is clearly an algebraic integer, we now know that it is in fact an integer.
›
moreover have "algebraic_int J'"
unfolding J'_def
proof (intro algebraic_int_prod)
fix x assume "x ∈ Roots'"
hence "fact (p - 1) alg_dvd J x"
by (intro J)
thus "algebraic_int (J x)"
by (rule alg_dvd_imp_algebraic_int) auto
qed
ultimately have "J' ∈ ℤ"
using rational_algebraic_int_is_int by blast
text ‹
It is also non-zero, as none of the $J_i$ have $p$ as a factor and such cannot be zero.
›
have "J' ≠ 0"
unfolding J'_def
proof (intro prod_nonzeroI)
fix α assume "α ∈ Roots'"
hence "¬of_nat p alg_dvd J α"
using J(2)[of α] by auto
thus "J α ≠ 0"
by auto
qed
text ‹
It then clearly follows that $(p-1)!^n \leq J$:
›
have "fact (p - 1) ^ n alg_dvd J'"
proof -
have "fact (p - 1) ^ n = (∏α∈Roots'. fact (p - 1))"
by (simp add: n_altdef)
also have "… alg_dvd J'"
unfolding J'_def by (intro prod_alg_dvd_prod J(1))
finally show ?thesis .
qed
have "fact (p - 1) ^ n ≤ norm J'"
proof -
from ‹J' ∈ ℤ› obtain J'' where [simp]: "J' = of_int J''"
by (elim Ints_cases)
have "of_int (fact (p - 1) ^ n) = (fact (p - 1) ^ n :: complex)"
by simp
also have "… alg_dvd J'"
by fact
also have "J' = of_int J''"
by fact
finally have "fact (p - 1) ^ n dvd J''"
by (subst (asm) alg_dvd_of_int_iff)
moreover from ‹J' ≠ 0› have "J'' ≠ 0"
by auto
ultimately have "¦J''¦ ≥ ¦fact (p - 1) ^ n¦"
by (intro dvd_imp_le_int)
hence "real_of_int ¦J''¦ ≥ real_of_int ¦fact (p - 1) ^ n¦"
by linarith
also have "real_of_int ¦J''¦ = norm J'"
by simp
finally show ?thesis
by simp
qed
text ‹The standard M-L bound for $I_i(x)$ shows the following inequality:›
also have "norm J' ≤ C' * C p ^ n"
proof -
have "norm J' = (∏x∈Roots'. norm (J x))"
unfolding J'_def prod_norm [symmetric] ..
also have "… ≤ (∏x∈Roots'. ∑q∈P. real_of_int ¦β q¦ * (∑α∈Roots q. cmod α * exp (cmod α) * C p))"
proof (intro prod_mono conjI)
fix x assume x: "x ∈ Roots'"
show "norm (J x) ≤ (∑q∈P. real_of_int ¦β q¦ * (∑α∈Roots q. norm α * exp (norm α) * C p))"
unfolding J_def
proof (intro sum_norm_le)
fix q assume "q ∈ P"
show "norm (of_int (β q) * sum (I x) (Roots q)) ≤
real_of_int ¦β q¦ * (∑α∈Roots q. norm α * exp (norm α) * C p)"
unfolding norm_mult norm_of_int of_int_abs
proof (intro mult_left_mono sum_norm_le)
fix α assume "α ∈ Roots q"
hence α: "α ∈ Roots'"
using ‹q ∈ P› by (auto simp: Roots'_def)
show "norm (I x α) ≤ norm α * exp (norm α) * C p"
unfolding I_def
proof (intro lindemann_weierstrass_aux.lindemann_weierstrass_integral_bound)
fix t assume "t ∈ closed_segment 0 α"
also have "closed_segment 0 α ⊆ cball 0 R"
using ‹R ≥ 0› R_ge[OF α] by (intro closed_segment_subset) auto
finally have "norm t ≤ R" by simp
have norm_diff_le: "norm (t - y) ≤ 2 * R" if "y ∈ Roots'" for y
proof -
have "norm (t - y) ≤ norm t + norm y"
by (meson norm_triangle_ineq4)
also have "… ≤ R + R"
by (intro add_mono[OF ‹norm t ≤ R› R_ge] that)
finally show ?thesis by simp
qed
have "norm (poly (f_poly x) t) =
¦real_of_int l¦ ^ (n * p) * (∏y∈Roots'. cmod (t - y) ^ (if y = x then p - 1 else p))"
by (simp add: eval_f x f_def norm_mult norm_power flip: prod_norm)
also have "… ≤ ¦real_of_int l¦ ^ (n * p) * (∏y∈Roots'. (2*R) ^ (if y = x then p - 1 else p))"
by (intro mult_left_mono prod_mono conjI power_mono norm_diff_le) auto
also have "… = ¦real_of_int l¦^(n*p) * (2^(p-1) * R^(p-1) * (2^p*R^p)^(n-1))"
using x by (subst prod.If_eq) (auto simp: card_Diff_subset n_altdef)
also have "2^(p-1) * R^(p-1) * (2^p*R^p)^(n-1) = (2^((p-1)+p*(n-1))) * (R^((p-1)+p*(n-1)))"
unfolding power_mult power_mult_distrib power_add by (simp add: mult_ac)
also have "(p-1)+p*(n-1) = p*n - 1"
using ‹n > 0› ‹p > 1› by (cases n) (auto simp: algebra_simps)
also have "2 ^ (p * n - 1) * R ^ (p * n - 1) = (2*R)^(n * p-1)"
unfolding power_mult_distrib by (simp add: mult_ac)
finally show "norm (poly (f_poly x) t) ≤ C p"
unfolding C_def using ‹l > 0› by simp
qed (use ‹R ≥ 0› ‹l > 0› in ‹auto simp: C_def›)
qed auto
qed
qed auto
also have "… = C' * C p ^ n"
by (simp add: C'_def power_mult_distrib n_altdef flip: sum_distrib_right mult.assoc)
finally show ?thesis .
qed
text ‹And with that, we have our inequality:›
finally show "fact (p - 1) ^ n ≤ C' * C p ^ n" .
qed
text ‹
Some simple asymptotic estimates show that this is clearly a contradiction, since
the left-hand side grows much faster than the right-hand side and there are infinitely many
sufficiently large primes:
›
have freq: "frequently prime sequentially"
using frequently_prime_cofinite unfolding cofinite_eq_sequentially .
have ev: "eventually (λp. (∀q∈P. int p > ¦β q¦) ∧
real p > norm (∏α∈Roots'. of_int (l^n) * (∏α'∈Roots'-{α}. (α-α')))) sequentially"
by (intro eventually_ball_finite ‹finite P› ballI eventually_conj filterlim_real_sequentially
eventually_compose_filterlim[OF eventually_gt_at_top] filterlim_int_sequentially)
have "frequently (λp. fact (p - 1) ^ n ≤ C' * C p ^ n) sequentially"
by (rule frequently_eventually_mono[OF freq ev]) (use ineq in blast)
moreover have "eventually (λp. fact (p - 1) ^ n > C' * C p ^ n) sequentially"
proof (cases "R = 0")
case True
have "eventually (λp. p * n > 1) at_top" using ‹n > 0›
by (intro eventually_compose_filterlim[OF eventually_gt_at_top] mult_nat_right_at_top)
thus ?thesis
by eventually_elim (use ‹n > 0› True in ‹auto simp: C_def power_0_left mult_ac›)
next
case False
hence "R > 0"
using ‹R ≥ 0› by auto
define D :: real where "D = (2 * R * ¦real_of_int l¦) ^ n"
have "D > 0"
using ‹R > 0› ‹l > 0› unfolding D_def by (intro zero_less_power) auto
have "(λp. C' * C p ^ n) ∈ O(λp. C p ^ n)"
by simp
also have "(λp. C p ^ n) ∈ O(λp. ((2 * R * l) ^ (n * p)) ^ n)"
proof (rule landau_o.big_power[OF bigthetaD1])
have np: "eventually (λp. p * n > 0) at_top" using ‹n > 0›
by (intro eventually_compose_filterlim[OF eventually_gt_at_top] mult_nat_right_at_top)
have "eventually (λp. (2 * R) * C p = (2 * R * l) ^ (n * p)) at_top"
using np
proof eventually_elim
case (elim p)
have "2 * R * C p = l ^ (n * p) * (2 * R) ^ (Suc (n * p - 1))"
by (simp add: C_def algebra_simps)
also have "Suc (n * p - 1) = n * p"
using elim by auto
finally show ?case
by (simp add: algebra_simps)
qed
hence "(λp. (2 * R) * C p) ∈ Θ(λp. (2 * R * l) ^ (n * p))"
by (intro bigthetaI_cong)
thus "C ∈ Θ(λp. (2 * R * l) ^ (n * p))"
using ‹R > 0› by simp
qed
also have "… = O(λp. (D ^ p) ^ n)"
using ‹l > 0› by (simp flip: power_mult add: power2_eq_square mult_ac D_def)
also have "(λp. (D ^ p) ^ n) ∈ o(λp. fact (p - 1) ^ n)"
proof (intro landau_o.small_power)
have "eventually (λp. D ^ p = D * D ^ (p - 1)) at_top"
using eventually_gt_at_top[of 0]
by eventually_elim (use ‹D > 0› in ‹auto simp flip: power_Suc›)
hence "(λp. D ^ p) ∈ Θ(λp. D * D ^ (p - 1))"
by (intro bigthetaI_cong)
hence "(λp. D ^ p) ∈ Θ(λp. D ^ (p - 1))"
using ‹D > 0› by simp
also have "(λp. D ^ (p - 1)) ∈ o(λp. fact (p - 1))"
by (intro smalloI_tendsto[OF filterlim_compose[OF power_over_fact_tendsto_0]]
filterlim_minus_const_nat_at_top) auto
finally show "(λp. D ^ p) ∈ o(λx. fact (x - 1))" .
qed fact+
finally have smallo: "(λp. C' * C p ^ n) ∈ o(λp. fact (p - 1) ^ n)" .
have "eventually (λp. ¦C' * C p ^ n¦ ≤ 1/2 * fact (p - 1) ^ n) at_top"
using landau_o.smallD[OF smallo, of "1/2"] by simp
thus "eventually (λp. C' * C p ^ n < fact (p - 1) ^ n) at_top"
proof eventually_elim
case (elim p)
have "C' * C p ^ n ≤ ¦C' * C p ^ n¦"
by simp
also have "… ≤ 1/2 * fact (p - 1) ^ n"
by fact
also have "… < fact (p - 1) ^ n"
by simp
finally show ?case .
qed
qed
ultimately have "frequently (λp::nat. False) sequentially"
by (rule frequently_eventually_mono) auto
thus False
by simp
qed
subsection ‹Removing the restriction of full sets of conjugates›
text ‹
We will now remove the restriction that the $\alpha_i$ must occur in full sets of conjugates
by multiplying the equality with all permutations of roots.
›
lemma Hermite_Lindemann_aux2:
fixes X :: "complex set" and β :: "complex ⇒ int"
assumes "finite X"
assumes nz: "⋀x. x ∈ X ⟹ β x ≠ 0"
assumes alg: "⋀x. x ∈ X ⟹ algebraic x"
assumes sum0: "(∑x∈X. of_int (β x) * exp x) = 0"
shows "X = {}"
proof (rule ccontr)
assume "X ≠ {}"
note [intro] = ‹finite X›
text ‹
Let ‹P› be the smallest integer polynomial whose roots are a superset of ‹X›:
›
define P :: "int poly" where "P = ∏(min_int_poly ` X)"
define Roots :: "complex set" where "Roots = {x. ipoly P x = 0}"
have [simp]: "P ≠ 0"
using ‹finite X› by (auto simp: P_def)
have [intro]: "finite Roots"
unfolding Roots_def by (intro poly_roots_finite) auto
have "X ⊆ Roots"
proof safe
fix x assume "x ∈ X"
hence "ipoly (min_int_poly x) x = 0"
by (intro ipoly_min_int_poly alg)
thus "x ∈ Roots"
using ‹finite X› ‹x ∈ X›
by (auto simp: Roots_def P_def of_int_poly_hom.hom_prod poly_prod)
qed
have "squarefree (of_int_poly P :: complex poly)"
unfolding P_def of_int_poly_hom.hom_prod
proof (rule squarefree_prod_coprime; safe)
fix x assume "x ∈ X"
thus "squarefree (of_int_poly (min_int_poly x) :: complex poly)"
by (intro squarefree_of_int_polyI) auto
next
fix x y assume xy: "x ∈ X" "y ∈ X" "min_int_poly x ≠ min_int_poly y"
thus "Rings.coprime (of_int_poly (min_int_poly x)) (of_int_poly (min_int_poly y) :: complex poly)"
by (intro coprime_of_int_polyI[OF primes_coprime]) auto
qed
text ‹
Since we will need a numbering of these roots, we obtain one:
›
define n where "n = card Roots"
obtain Root where Root: "bij_betw Root {..<n} Roots"
using ex_bij_betw_nat_finite[OF ‹finite Roots›] unfolding n_def atLeast0LessThan by metis
define unRoot :: "complex ⇒ nat" where "unRoot = inv_into {..<n} Root"
have unRoot: "bij_betw unRoot Roots {..<n}"
unfolding unRoot_def by (intro bij_betw_inv_into Root)
have unRoot_Root [simp]: "unRoot (Root i) = i" if "i < n" for i
unfolding unRoot_def using Root that by (subst inv_into_f_f) (auto simp: bij_betw_def)
have Root_unRoot [simp]: "Root (unRoot x) = x" if "x ∈ Roots" for x
unfolding unRoot_def using Root that by (subst f_inv_into_f) (auto simp: bij_betw_def)
have [simp, intro]: "Root i ∈ Roots" if "i < n" for i
using Root that by (auto simp: bij_betw_def)
have [simp, intro]: "unRoot x < n" if "x ∈ Roots" for x
using unRoot that by (auto simp: bij_betw_def)
text ‹
We will also need to convert between permutations of natural numbers less than ‹n› and
permutations of the roots:
›
define convert_perm :: "(nat ⇒ nat) ⇒ (complex ⇒ complex)" where
"convert_perm = (λσ x. if x ∈ Roots then Root (σ (unRoot x)) else x)"
have bij_convert: "bij_betw convert_perm {σ. σ permutes {..<n}} {σ. σ permutes Roots}"
using bij_betw_permutations[OF Root] unfolding convert_perm_def unRoot_def .
have permutes_convert_perm [intro]: "convert_perm σ permutes Roots" if "σ permutes {..<n}" for σ
using that bij_convert unfolding bij_betw_def by blast
have convert_perm_compose: "convert_perm (π ∘ σ) = convert_perm π ∘ convert_perm σ"
if "π permutes {..<n}" "σ permutes {..<n}" for σ π
proof (intro ext)
fix x show "convert_perm (π ∘ σ) x = (convert_perm π ∘ convert_perm σ) x"
proof (cases "x ∈ Roots")
case True
thus ?thesis
using permutes_in_image[OF that(2), of "unRoot x"]
by (auto simp: convert_perm_def bij_betw_def)
qed (auto simp: convert_perm_def)
qed
text ‹
We extend the coefficient vector to the new roots by setting their coefficients to 0:
›
define β' where "β' = (λx. if x ∈ X then β x else 0)"
text ‹
We now define the set of all permutations of our roots:
›
define perms where "perms = {π. π permutes Roots}"
have [intro]: "finite perms"
unfolding perms_def by (rule finite_permutations) auto
have [simp]: "card perms = fact n"
unfolding perms_def n_def by (intro card_permutations) auto
text ‹
The following is the set of all ‹n!›-tuples of roots, disregarding permutation of components.
In other words: all multisets of roots with size ‹n!›.
›
define Roots_ms :: "complex multiset set" where
"Roots_ms = {X. set_mset X ⊆ Roots ∧ size X = fact n}"
have [intro]: "finite Roots_ms"
unfolding Roots_ms_def by (rule finite_multisets_of_size) auto
text ‹
Next, the following is the set of ‹n!›-tuples whose entries are precisely the multiset ‹X›:
›
define tuples :: "complex multiset ⇒ ((complex ⇒ complex) ⇒ complex) set" where
"tuples = (λX. {f∈perms →⇩E Roots. image_mset f (mset_set perms) = X})"
have fin_tuples [intro]: "finite (tuples X)" for X
unfolding tuples_def by (rule finite_subset[of _ "perms →⇩E Roots", OF _ finite_PiE]) auto
define tuples' :: "(complex multiset × ((complex ⇒ complex) ⇒ complex)) set" where
"tuples' = (SIGMA X:Roots_ms. tuples X)"
text ‹
The following shows that our \<^term>‹tuples› definition is stable under permutation of
the roots.
›
have bij_convert': "bij_betw (λf. f ∘ (λg. σ ∘ g)) (tuples X) (tuples X)"
if σ: "σ permutes Roots" for σ X
proof (rule bij_betwI)
have *: "(λf. f ∘ (∘) σ) ∈ tuples X → tuples X" if σ: "σ permutes Roots" for σ
proof
fix f assume f: "f ∈ tuples X"
show "f ∘ (∘) σ ∈ tuples X"
unfolding tuples_def
proof safe
fix σ'
assume σ': "σ' ∈ perms"
show "(f ∘ (∘) σ) σ' ∈ Roots"
using permutes_compose[OF _ σ, of σ'] σ σ' f by (auto simp: perms_def tuples_def)
next
fix σ'
assume σ': "σ' ∉ perms"
have "¬(σ ∘ σ') permutes Roots"
proof
assume "(σ ∘ σ') permutes Roots"
hence "inv_into UNIV σ ∘ (σ ∘ σ') permutes Roots"
by (rule permutes_compose) (use permutes_inv[OF σ] in simp_all)
also have "inv_into UNIV σ ∘ (σ ∘ σ') = σ'"
by (auto simp: fun_eq_iff permutes_inverses[OF σ])
finally show False using σ' by (simp add: perms_def)
qed
thus "(f ∘ (∘) σ) σ' = undefined"
using f by (auto simp: perms_def tuples_def)
next
have "image_mset (f ∘ (∘) σ) (mset_set perms) =
image_mset f (image_mset ((∘) σ) (mset_set perms))"
by (rule multiset.map_comp [symmetric])
also have "image_mset ((∘) σ) (mset_set perms) = mset_set perms"
using bij_betw_permutes_compose_left[OF σ]
by (subst image_mset_mset_set) (auto simp: bij_betw_def perms_def)
also have "image_mset f … = X"
using f by (auto simp: tuples_def)
finally show "image_mset (f ∘ (∘) σ) (mset_set perms) = X" .
qed
qed
show "(λf. f ∘ (∘) σ) ∈ tuples X → tuples X"
by (rule *) fact
show "(λf. f ∘ (∘) (inv_into UNIV σ)) ∈ tuples X → tuples X"
by (intro * permutes_inv) fact
show "f ∘ (∘) σ ∘ (∘) (inv_into UNIV σ) = f" if "f ∈ tuples X" for f
by (auto simp: fun_eq_iff o_def permutes_inverses[OF σ])
show "f ∘ (∘) (inv_into UNIV σ) ∘ (∘) σ = f" if "f ∈ tuples X" for f
by (auto simp: fun_eq_iff o_def permutes_inverses[OF σ])
qed
text ‹
Next, we define the multiset of of possible exponents that we can get for a given
‹n!›-multiset of roots,
›
define R :: "complex multiset ⇒ complex multiset" where
"R = (λX. image_mset (λf. ∑σ∈perms. σ (f σ)) (mset_set (tuples X)))"
text ‹
We show that, for each such multiset, there is a content-free integer polynomial that has
exactly these exponents as roots. This shows that they form a full set of conjugates (but
note this polynomial is not necessarily squarefree).
The proof is yet another application of the fundamental theorem of symmetric polynomials.
›
obtain Q :: "complex multiset ⇒ int poly"
where Q: "⋀X. X ∈ Roots_ms ⟹ poly_roots (of_int_poly (Q X)) = R X"
"⋀X. X ∈ Roots_ms ⟹ content (Q X) = 1"
proof -
{
fix X :: "complex multiset"
assume X: "X ∈ Roots_ms"
define Q :: "complex poly mpoly" where
"Q = (∏f∈tuples X. Const [:0, 1:] -
(∑σ | σ permutes {..<n}. Var (σ (unRoot (f (convert_perm σ))))))"
define Q1 where "Q1 = (∏f∈tuples X. [:- (∑σ | σ permutes Roots. σ (f σ)), 1:])"
define ratpolys :: "complex poly set" where "ratpolys = {p. ∀i. poly.coeff p i ∈ ℚ}"
have "insertion (λx. [:Root x:]) Q ∈ ratpolys"
proof (rule symmetric_poly_of_roots_in_subring[where l = "λx. [:x:]"])
show "ring_closed ratpolys"
unfolding ratpolys_def by standard (auto intro: coeff_mult_semiring_closed)
then interpret ratpolys: ring_closed ratpolys .
have "pCons 0 1 ∈ ratpolys "
by (auto simp: ratpolys_def coeff_pCons split: nat.splits)
thus "∀m. MPoly_Type.coeff Q m ∈ ratpolys"
unfolding Q_def
by (intro allI ratpolys.coeff_prod_closed)
(auto intro!: ratpolys.minus_closed ratpolys.sum_closed ratpolys.uminus_closed simp: coeff_Var mpoly_coeff_Const when_def)
next
show "ring_homomorphism (λx::complex. [:x:])" ..
next
have "σ (unRoot (f (convert_perm σ))) < n" if "f ∈ tuples X" "σ permutes {..<n}" for f σ
proof -
have "convert_perm σ ∈ perms"
using bij_convert that(2) by (auto simp: bij_betw_def perms_def)
hence "f (convert_perm σ) ∈ Roots"
using that by (auto simp: tuples_def)
thus ?thesis
using permutes_in_image[OF that(2)] by simp
qed
thus "vars Q ⊆ {..<n}"
unfolding Q_def
by (intro order.trans[OF vars_prod] UN_least order.trans[OF vars_sum]
order.trans[OF vars_diff] Un_least) (auto simp: vars_Var)
next
define lc :: complex where "lc = of_int (Polynomial.lead_coeff P)"
show "[:inverse lc:] ∈ ratpolys"
by (auto simp: ratpolys_def coeff_pCons lc_def split: nat.splits)
show "∀i. [:poly.coeff (of_int_poly P) i:] ∈ ratpolys"
by (auto simp: ratpolys_def coeff_pCons split: nat.splits)
have "lc ≠ 0"
by (auto simp: lc_def)
thus "[:inverse lc:] * [:lc:] = 1"
by auto
have "rsquarefree (of_int_poly P :: complex poly)"
using ‹squarefree (of_int_poly P :: complex poly)› by (intro squarefree_imp_rsquarefree)
hence "of_int_poly P = Polynomial.smult lc (∏x∈Roots. [:-x, 1:])"
unfolding lc_def Roots_def of_int_hom.hom_lead_coeff[symmetric]
by (rule complex_poly_decompose_rsquarefree [symmetric])
also have "(∏x∈Roots. [:-x, 1:]) = (∏i<n. [:-Root i, 1:])"
by (rule prod.reindex_bij_betw[OF Root, symmetric])
finally show "of_int_poly P = Polynomial.smult lc (∏i<n. [:- Root i, 1:])" .
next
show "symmetric_mpoly {..<n} Q"
unfolding symmetric_mpoly_def
proof safe
fix π assume π: "π permutes {..<n}"
have "mpoly_map_vars π Q = (∏f∈tuples X. Const (pCons 0 1) - (∑ σ | σ permutes {..<n}.
Var ((π ∘ σ) (unRoot (f (convert_perm σ))))))"
by (simp add: Q_def permutes_bij[OF π])
also have "… = (∏f∈tuples X. Const (pCons 0 1) - (∑ σ | σ permutes {..<n}.
Var ((π ∘ σ) (unRoot ((f ∘ (λσ. convert_perm π ∘ σ)) (convert_perm σ))))))"
using π by (intro prod.reindex_bij_betw [OF bij_convert', symmetric]) auto
also have "… = Q"
unfolding Q_def
proof (rule prod.cong, goal_cases)
case (2 f)
have "(∑ σ | σ permutes {..<n}. Var ((π ∘ σ) (unRoot ((f ∘ (λσ. convert_perm π ∘ σ)) (convert_perm σ))))) =
(∑ σ | σ permutes {..<n}. Var ((π ∘ σ) (unRoot (f (convert_perm (π ∘ σ))))))"
using π by (intro sum.cong refl, subst convert_perm_compose) simp_all
also have "… = (∑ σ | σ permutes {..<n}. Var (σ (unRoot (f (convert_perm σ)))))"
using π by (rule setum_permutations_compose_left [symmetric])
finally show ?case by simp
qed auto
finally show "mpoly_map_vars π Q = Q" .
qed
qed auto
also have "insertion (λx. [:Root x:]) Q = Q1"
unfolding Q_def Q1_def insertion_prod insertion_sum insertion_diff insertion_Const insertion_Var
proof (intro prod.cong, goal_cases)
case f: (2 f)
have "(∑σ | σ permutes {..<n}. [:Root (σ (unRoot (f (convert_perm σ)))):]) =
(∑σ | σ permutes {..<n}. [:convert_perm σ (f (convert_perm σ)):])"
proof (rule sum.cong, goal_cases)
case (2 σ)
have "convert_perm σ permutes Roots"
using bij_convert 2 by (auto simp: bij_betw_def)
hence "f (convert_perm σ) ∈ Roots"
using f by (auto simp: tuples_def perms_def)
thus ?case by (simp add: convert_perm_def)
qed simp_all
also have "… = (∑σ | σ permutes Roots. [:σ (f σ):])"
by (rule sum.reindex_bij_betw[OF bij_convert])
finally show ?case
by (simp flip: pCons_one coeff_lift_hom.hom_sum)
qed simp_all
finally have "Q1 ∈ ratpolys"
by auto
then obtain Q2 :: "rat poly" where Q2: "Q1 = map_poly of_rat Q2"
unfolding ratpolys_def using ratpolyE[of Q1] by blast
have "Q1 ≠ 0"
unfolding Q1_def using fin_tuples[of X] by auto
with Q2 have "Q2 ≠ 0"
by auto
obtain Q3 :: "int poly" and lc :: rat
where Q3: "Q2 = Polynomial.smult lc (of_int_poly Q3)" and "lc > 0" and "content Q3 = 1"
using rat_to_normalized_int_poly_exists[OF ‹Q2 ≠ 0›] by metis
have "poly_roots (of_int_poly Q3) = poly_roots (map_poly (of_rat ∘ of_int) Q3)"
by simp
also have "map_poly (of_rat ∘ of_int) Q3 = map_poly of_rat (map_poly of_int Q3)"
by (subst map_poly_map_poly) auto
also have "poly_roots … = poly_roots (Polynomial.smult (of_rat lc) …)"
using ‹lc > 0› by simp
also have "Polynomial.smult (of_rat lc) (map_poly of_rat (map_poly of_int Q3)) =
map_poly of_rat (Polynomial.smult lc (map_poly of_int Q3))"
by (simp add: of_rat_hom.map_poly_hom_smult)
also have "… = Q1"
by (simp only: Q3 [symmetric] Q2 [symmetric])
also have "poly_roots Q1 = R X"
unfolding Q1_def
by (subst poly_roots_prod, force, subst poly_roots_linear)
(auto simp: R_def perms_def sum_mset_image_mset_singleton sum_unfold_sum_mset)
finally have "∃Q. poly_roots (of_int_poly Q) = R X ∧ content Q = 1"
using ‹content Q3 = 1› by metis
}
hence "∃Q. ∀X∈Roots_ms. poly_roots (of_int_poly (Q X)) = R X ∧ content (Q X) = 1"
by metis
thus ?thesis using that by metis
qed
text ‹
We can now collect all the $e^{\sum \alpha_i}$ that happen to be equal and let the following
be their coefficients:
›
define β'' :: "int poly ⇒ int"
where "β'' = (λq. ∑X∈Roots_ms. int (count (prime_factorization (Q X)) q) * (∏x∈#X. β' x))"
have supp_β'': "{q. β'' q ≠ 0} ⊆ (⋃X∈Roots_ms. prime_factors (Q X))"
unfolding β''_def using sum.not_neutral_contains_not_neutral by fastforce
text ‹
We have to prove that ‹β''› is not zero everywhere. We do this by selecting the nonzero term
with the maximal exponent (w.r.t. the lexicographic ordering on the complex numbers) in every
factor of the product and show that there is no other summand corresponding to these, so
that their non-zero coefficient cannot get cancelled.
›
have "{q. β'' q ≠ 0} ≠ {}"
proof -
define f where "f = restrict (λσ. inv_into UNIV σ (complex_lex.Max (σ ` X))) perms"
have f: "f ∈ perms → X"
proof
fix σ assume σ: "σ ∈ perms"
have "complex_lex.Max (σ ` X) ∈ σ ` X"
using ‹X ≠ {}› by (intro complex_lex.Max_in finite_imageI) auto
thus "f σ ∈ X"
using σ by (auto simp: f_def permutes_inverses[of σ Roots] perms_def)
qed
hence f': "f ∈ perms →⇩E Roots"
using ‹X ⊆ Roots› by (auto simp: f_def PiE_def)
define Y where "Y = image_mset f (mset_set perms)"
have "Y ∈ Roots_ms" using f' ‹finite perms›
by (auto simp: Roots_ms_def Y_def)
have "(∑σ∈perms. σ (f σ)) ∈# R Y"
proof -
from f' have "f ∈ tuples Y"
unfolding tuples_def Y_def by simp
thus ?thesis
unfolding R_def using fin_tuples[of Y] by auto
qed
also have "R Y = poly_roots (of_int_poly (Q Y))"
by (rule Q(1) [symmetric]) fact
also have "… = (∑p∈#prime_factorization (Q Y). poly_roots (of_int_poly p))"
by (rule poly_roots_of_int_conv_sum_prime_factors)
finally obtain q where q: "q ∈ prime_factors (Q Y)" "(∑σ∈perms. σ (f σ)) ∈# poly_roots (of_int_poly q)"
by auto
have "β'' q = (∑X∈{Y}. int (count (prime_factorization (Q X)) q) * prod_mset (image_mset β' X))"
unfolding β''_def
proof (intro sum.mono_neutral_right ballI)
fix Y' assume Y': "Y' ∈ Roots_ms - {Y}"
show "int (count (prime_factorization (Q Y')) q) * ∏⇩# (image_mset β' Y') = 0"
proof (cases "set_mset Y' ⊆ X")
case Y'_subset: True
have "q ∉ prime_factors (Q Y')"
proof
assume q': "q ∈ prime_factors (Q Y')"
have "poly_roots (of_int_poly q :: complex poly) ⊆#
poly_roots (of_int_poly (Q Y'))"
using q' by (intro dvd_imp_poly_roots_subset of_int_poly_hom.hom_dvd) auto
with q(2) have "(∑σ∈perms. σ (f σ)) ∈# poly_roots (of_int_poly (Q Y'))"
by (meson mset_subset_eqD)
also have "poly_roots (of_int_poly (Q Y')) = R Y'"
using Q(1)[of Y'] Y' by auto
finally obtain g where g: "g ∈ tuples Y'" "(∑σ∈perms. σ (f σ)) = (∑σ∈perms. σ (g σ))"
unfolding R_def using fin_tuples[of Y'] by auto
moreover have "(∑σ∈perms. σ (g σ)) <⇩ℂ (∑σ∈perms. σ (f σ))"
proof (rule sum_strict_mono_ex1_complex_lex)
show le: "∀σ∈perms. σ (g σ) ≤⇩ℂ σ (f σ)"
proof
fix σ assume σ: "σ ∈ perms"
hence σ': "σ permutes Roots"
by (auto simp: perms_def)
have "image_mset g (mset_set perms) = Y'"
using g by (auto simp: tuples_def)
also have "set_mset … ⊆ X"
by fact
finally have "g ` perms ⊆ X"
using ‹finite perms› by auto
hence "σ (g σ) ≤⇩ℂ complex_lex.Max (σ ` X)"
using ‹finite perms› σ
by (intro complex_lex.Max.coboundedI finite_imageI imageI)
(auto simp: tuples_def)
also have "… = σ (f σ)"
using σ by (simp add: f_def permutes_inverses[OF σ'])
finally show "σ (g σ) ≤⇩ℂ σ (f σ)" .
qed
have "image_mset g (mset_set perms) ≠ image_mset f (mset_set perms)"
using Y' g by (auto simp: tuples_def Y_def)
then obtain σ where σ: "σ ∈# mset_set perms" "g σ ≠ f σ"
by (meson multiset.map_cong)
have "σ permutes Roots"
using σ ‹finite perms› by (auto simp: perms_def)
have "σ (g σ) ≠ σ (f σ)"
using permutes_inj[OF ‹σ permutes Roots›] σ by (auto simp: inj_def)
moreover have "σ (g σ) ≤⇩ℂ σ (f σ)"
using le σ ‹finite perms› by auto
ultimately have "σ (g σ) <⇩ℂ σ (f σ)"
by simp
thus "∃σ∈perms. σ (g σ) <⇩ℂ σ (f σ)"
using σ ‹finite perms› by auto
qed (use ‹finite perms› in simp_all)
ultimately show False by simp
qed
thus ?thesis by auto
qed (auto simp: β'_def)
qed (use ‹Y ∈ Roots_ms› in auto)
also have "… = int (count (prime_factorization (Q Y)) q) * prod_mset (image_mset β' Y)"
by simp
also have "… ≠ 0"
using q nz ‹finite X› ‹X ≠ {}› ‹finite perms› f by (auto simp: β'_def Y_def)
finally show "{q. β'' q ≠ 0} ≠ {}"
by auto
qed
text ‹
We are now ready for the final push: we start with the original sum that we know to be zero,
multiply it with the other permutations, and then multiply out the sum.
›
have "0 = (∑x∈X. β x * exp x)"
using sum0 ..
also have "… = (∑x∈Roots. β' x * exp x)"
by (intro sum.mono_neutral_cong_left ‹X ⊆ Roots›) (auto simp: β'_def)
also have "… dvd (∏σ∈perms. ∑x∈Roots. β' x * exp (σ x))"
by (rule dvd_prodI[OF ‹finite perms›])
(use permutes_id[of Roots] in ‹simp_all add: id_def perms_def›)
also have "… = (∑f∈perms →⇩E Roots. ∏σ∈perms. β' (f σ) * exp (σ (f σ)))"
by (rule prod_sum_PiE) auto
also have "… = (∑f∈perms →⇩E Roots. (∏σ∈perms. β' (f σ)) * exp (∑σ∈perms. σ (f σ)))"
using ‹finite perms› by (simp add: prod.distrib exp_sum)
also have "… = (∑(X,f)∈tuples'. (∏σ∈perms. β' (f σ)) * exp (∑σ∈perms. σ (f σ)))"
using ‹finite perms›
by (intro sum.reindex_bij_witness[of _ snd "λf. (image_mset f (mset_set perms), f)"])
(auto simp: tuples'_def tuples_def Roots_ms_def PiE_def Pi_def)
also have "… = (∑(X,f)∈tuples'. (∏x∈#X. β' x) * exp (∑σ∈perms. σ (f σ)))"
proof (safe intro!: sum.cong)
fix X :: "complex multiset" and f :: "(complex ⇒ complex) ⇒ complex"
assume "(X, f) ∈ tuples'"
hence X: "X ∈ Roots_ms" "X = image_mset f (mset_set perms)" and f: "f ∈ perms →⇩E Roots"
by (auto simp: tuples'_def tuples_def)
have "(∏σ∈perms. β' (f σ)) = (∏σ∈#mset_set perms. β' (f σ))"
by (meson prod_unfold_prod_mset)
also have "… = (∏x∈#X. β' x)"
unfolding X(2) by (simp add: multiset.map_comp o_def)
finally show "(∏σ∈perms. β' (f σ)) * exp (∑σ∈perms. σ (f σ)) =
(∏x∈#X. β' x) * exp (∑σ∈perms. σ (f σ))" by simp
qed
also have "… = (∑X∈Roots_ms. ∑f∈tuples X. (∏x∈#X. β' x) * exp (∑σ∈perms. σ (f σ)))"
unfolding tuples'_def by (intro sum.Sigma [symmetric]) auto
also have "… = (∑X∈Roots_ms. of_int (∏x∈#X. β' x) * (∑f∈tuples X. exp (∑σ∈perms. σ (f σ))))"
by (simp add: sum_distrib_left)
also have "… = (∑X∈Roots_ms. of_int (∏x∈#X. β' x) * (∑x∈#R X. exp x))"
by (simp only: R_def multiset.map_comp o_def sum_unfold_sum_mset)
also have "… = (∑X∈Roots_ms. of_int (∏x∈#X. β' x) * (∑x∈#poly_roots (of_int_poly (Q X)). exp x))"
by (intro sum.cong) (simp_all flip: Q)
text ‹
Our problem now is that the polynomials ‹Q X› can still contain multiple roots and that their
roots might not be disjoint. We therefore split them all into irreducible factors and collect
equal terms.
›
also have "… = (∑X∈Roots_ms. (∑p. of_int (int (count (prime_factorization (Q X)) p) *
(∏x∈#X. β' x)) * (∑x | ipoly p x = 0. exp x)))"
proof (rule sum.cong, goal_cases)
case (2 X)
have "(∑x∈#poly_roots (of_int_poly (Q X) :: complex poly). exp x) =
(∑x ∈# (∑p∈#prime_factorization (Q X). poly_roots (of_int_poly p)). exp x)"
by (subst poly_roots_of_int_conv_sum_prime_factors) (rule refl)
also have "… = (∑p∈#prime_factorization (Q X). ∑x∈#poly_roots (of_int_poly p). exp x)"
by (rule sum_mset_image_mset_sum_mset_image_mset)
also have "rsquarefree (of_int_poly p :: complex poly)" if "p ∈ prime_factors (Q X)" for p
proof (rule irreducible_imp_rsquarefree_of_int_poly)
have "prime p"
using that by auto
thus "irreducible p"
by blast
next
show "Polynomial.degree p > 0"
by (intro content_1_imp_nonconstant_prime_factors[OF Q(2) that] 2)
qed
hence "(∑p∈#prime_factorization (Q X). ∑x∈#poly_roots (of_int_poly p). exp x) =
(∑p∈#prime_factorization (Q X). ∑x | ipoly p x = 0. exp (x :: complex))"
unfolding sum_unfold_sum_mset
by (intro arg_cong[of _ _ sum_mset] image_mset_cong sum.cong refl,
subst rsquarefree_poly_roots_eq) auto
also have "… = (∑p. count (prime_factorization (Q X)) p * (∑x | ipoly p x = 0. exp (x :: complex)))"
by (rule sum_mset_conv_Sum_any)
also have "of_int (∏x∈#X. β' x) * … =
(∑p. of_int (int (count (prime_factorization (Q X)) p) * (∏x∈#X. β' x)) * (∑x | ipoly p x = 0. exp x))"
by (subst Sum_any_right_distrib) (auto simp: mult_ac)
finally show ?case by simp
qed auto
also have "… = (∑q. of_int (β'' q) * (∑x | ipoly q x = 0. exp x))"
unfolding β''_def of_int_sum
by (subst Sum_any_sum_swap [symmetric]) (auto simp: sum_distrib_right)
also have "… = (∑q | β'' q ≠ 0. of_int (β'' q) * (∑x | ipoly q x = 0. exp x))"
by (intro Sum_any.expand_superset finite_subset[OF supp_β'']) auto
finally have "(∑q | β'' q ≠ 0. of_int (β'' q) * (∑x | ipoly q x = 0. exp (x :: complex))) = 0"
by simp
text ‹
We are now in the situation of our the specialised Hermite--Lindemann Theorem we proved
earlier and can easily derive a contradiction.
›
moreover have "(∑q | β'' q ≠ 0. of_int (β'' q) * (∑x | ipoly q x = 0. exp (x :: complex))) ≠ 0"
proof (rule Hermite_Lindemann_aux1)
show "finite {q. β'' q ≠ 0}"
by (rule finite_subset[OF supp_β'']) auto
next
show "pairwise Rings.coprime {q. β'' q ≠ 0}"
proof (rule pairwiseI, clarify)
fix p q assume pq: "p ≠ q" "β'' p ≠ 0" "β'' q ≠ 0"
hence "prime p" "prime q"
using supp_β'' Q(2) by auto
with pq show "Rings.coprime p q"
by (simp add: primes_coprime)
qed
next
fix q :: "int poly"
assume q: "q ∈ {q. β'' q ≠ 0}"
also note supp_β''
finally obtain X where X: "X ∈ Roots_ms" "q ∈ prime_factors (Q X)"
by blast
show "irreducible q"
using X by (intro prime_elem_imp_irreducible prime_imp_prime_elem) auto
show "Polynomial.degree q > 0" using X
by (intro content_1_imp_nonconstant_prime_factors[OF Q(2)[of X]])
qed (use ‹{x. β'' x ≠ 0} ≠ {}› in auto)
ultimately show False by contradiction
qed
subsection ‹Removing the restriction to integer coefficients›
text ‹
Next, we weaken the restriction that the $\beta_i$ must be integers to the restriction
that they must be rationals. This is done simply by multiplying with the least common multiple
of the demoninators.
›
lemma Hermite_Lindemann_aux3:
fixes X :: "complex set" and β :: "complex ⇒ rat"
assumes "finite X"
assumes nz: "⋀x. x ∈ X ⟹ β x ≠ 0"
assumes alg: "⋀x. x ∈ X ⟹ algebraic x"
assumes sum0: "(∑x∈X. of_rat (β x) * exp x) = 0"
shows "X = {}"
proof -
define l :: int where "l = Lcm ((snd ∘ quotient_of ∘ β) ` X)"
have [simp]: "snd (quotient_of r) ≠ 0" for r
using quotient_of_denom_pos'[of r] by simp
have [simp]: "l ≠ 0"
using ‹finite X› by (auto simp: l_def Lcm_0_iff)
have "of_int l * β x ∈ ℤ" if "x ∈ X" for x
proof -
define a b where "a = fst (quotient_of (β x))" and "b = snd (quotient_of (β x))"
have "b > 0"
using quotient_of_denom_pos'[of "β x"] by (auto simp: b_def)
have "β x = of_int a / of_int b"
by (intro quotient_of_div) (auto simp: a_def b_def)
also have "of_int l * … = of_int (l * a) / of_int b"
using ‹b > 0› by (simp add: field_simps)
also have "… ∈ ℤ" using that
by (intro of_int_divide_in_Ints) (auto simp: l_def b_def)
finally show ?thesis .
qed
hence "∀x∈X. ∃n. of_int n = of_int l * β x"
using Ints_cases by metis
then obtain β' where β': "of_int (β' x) = of_int l * β x" if "x ∈ X" for x
by metis
show ?thesis
proof (rule Hermite_Lindemann_aux2)
have "0 = of_int l * (∑x∈X. of_rat (β x) * exp x :: complex)"
by (simp add: sum0)
also have "… = (∑x∈X. of_int (β' x) * exp x)"
unfolding sum_distrib_left
proof (rule sum.cong, goal_cases)
case (2 x)
have "of_int l * of_rat (β x) = of_rat (of_int l * β x)"
by (simp add: of_rat_mult)
also have "of_int l * β x = of_int (β' x)"
using 2 by (rule β' [symmetric])
finally show ?case by (simp add: mult_ac)
qed simp_all
finally show "… = 0" ..
next
fix x assume "x ∈ X"
hence "of_int (β' x) ≠ (0 :: rat)" using nz
by (subst β') auto
thus "β' x ≠ 0"
by auto
qed (use alg ‹finite X› in auto)
qed
text ‹
Next, we weaken the restriction that the $\beta_i$ must be rational to them being algebraic.
Similarly to before, this is done by multiplying over all possible permutations of the $\beta_i$
(in some sense) to introduce more symmetry, from which it then follows by the fundamental theorem
of symmetric polynomials that the resulting coefficients are rational.
›
lemma Hermite_Lindemann_aux4:
fixes β :: "complex ⇒ complex"
assumes [intro]: "finite X"
assumes alg1: "⋀x. x ∈ X ⟹ algebraic x"
assumes alg2: "⋀x. x ∈ X ⟹ algebraic (β x)"
assumes nz: "⋀x. x ∈ X ⟹ β x ≠ 0"
assumes sum0: "(∑x∈X. β x * exp x) = 0"
shows "X = {}"
proof (rule ccontr)
assume X: "X ≠ {}"
note [intro!] = finite_PiE
text ‹
We now take more or less the same approach as before, except that now we find a polynomial
that has all of the conjugates of the coefficients ‹β› as roots. Note that this is a slight
deviation from Baker's proof, who picks one polynomial for each ‹β› independently. I did it
this way because, as Bernard~\<^cite>‹"bernard"› observed, it makes the proof a bit easier.
›
define P :: "int poly" where "P = ∏((min_int_poly ∘ β) ` X)"
define Roots :: "complex set" where "Roots = {x. ipoly P x = 0}"
have "0 ∉ Roots" using ‹finite X› alg2 nz
by (auto simp: Roots_def P_def poly_prod)
have [simp]: "P ≠ 0"
using ‹finite X› by (auto simp: P_def)
have [intro]: "finite Roots"
unfolding Roots_def by (intro poly_roots_finite) auto
have "β ` X ⊆ Roots"
proof safe
fix x assume "x ∈ X"
hence "ipoly (min_int_poly (β x)) (β x) = 0"
by (intro ipoly_min_int_poly alg2)
thus "β x ∈ Roots"
using ‹finite X› ‹x ∈ X›
by (auto simp: Roots_def P_def of_int_poly_hom.hom_prod poly_prod)
qed
have "squarefree (of_int_poly P :: complex poly)"
unfolding P_def of_int_poly_hom.hom_prod o_def
proof (rule squarefree_prod_coprime; safe)
fix x assume "x ∈ X"
thus "squarefree (of_int_poly (min_int_poly (β x)) :: complex poly)"
by (intro squarefree_of_int_polyI) auto
next
fix x y assume xy: "x ∈ X" "y ∈ X" "min_int_poly (β x) ≠ min_int_poly (β y)"
thus "Rings.coprime (of_int_poly (min_int_poly (β x)))
(of_int_poly (min_int_poly (β y)) :: complex poly)"
by (intro coprime_of_int_polyI[OF primes_coprime]) auto
qed
define n where "n = card Roots"
define m where "m = card X"
have "Roots ≠ {}"
using ‹β ` X ⊆ Roots› ‹X ≠ {}› by auto
hence "n > 0" "m > 0"
using ‹finite Roots› ‹finite X› ‹X ≠ {}› by (auto simp: n_def m_def)
have fin1 [simp]: "finite (X →⇩E Roots)"
by auto
have [simp]: "card (X →⇩E Roots) = n ^ m"
by (subst card_PiE) (auto simp: m_def n_def)
text ‹
We again find a bijection between the roots and the natural numbers less than ‹n›:
›
obtain Root where Root: "bij_betw Root {..<n} Roots"
using ex_bij_betw_nat_finite[OF ‹finite Roots›] unfolding n_def atLeast0LessThan by metis
define unRoot :: "complex ⇒ nat" where "unRoot = inv_into {..<n} Root"
have unRoot: "bij_betw unRoot Roots {..<n}"
unfolding unRoot_def by (intro bij_betw_inv_into Root)
have unRoot_Root [simp]: "unRoot (Root i) = i" if "i < n" for i
unfolding unRoot_def using Root that by (subst inv_into_f_f) (auto simp: bij_betw_def)
have Root_unRoot [simp]: "Root (unRoot x) = x" if "x ∈ Roots" for x
unfolding unRoot_def using Root that by (subst f_inv_into_f) (auto simp: bij_betw_def)
have [simp, intro]: "Root i ∈ Roots" if "i < n" for i
using Root that by (auto simp: bij_betw_def)
have [simp, intro]: "unRoot x < n" if "x ∈ Roots" for x
using unRoot that by (auto simp: bij_betw_def)
text ‹
And we again define the set of multisets and tuples that we will get in the expanded product.
›
define Roots_ms :: "complex multiset set" where
"Roots_ms = {Y. set_mset Y ⊆ X ∧ size Y = n ^ m}"
have [intro]: "finite Roots_ms"
unfolding Roots_ms_def by (rule finite_multisets_of_size) auto
define tuples :: "complex multiset ⇒ ((complex ⇒ complex) ⇒ complex) set"
where "tuples = (λY. {f∈(X →⇩E Roots) →⇩E X. image_mset f (mset_set (X →⇩E Roots)) = Y})"
have [intro]: "finite (tuples Y)" for Y
unfolding tuples_def by (rule finite_subset[of _ "(X →⇩E Roots) →⇩E X"]) auto
text ‹
We will also need to convert permutations over the natural and over the roots again.
›
define convert_perm :: "(nat ⇒ nat) ⇒ (complex ⇒ complex)" where
"convert_perm = (λσ x. if x ∈ Roots then Root (σ (unRoot x)) else x)"
have bij_convert: "bij_betw convert_perm {σ. σ permutes {..<n}} {σ. σ permutes Roots}"
using bij_betw_permutations[OF Root] unfolding convert_perm_def unRoot_def .
have permutes_convert_perm [intro]: "convert_perm σ permutes Roots" if "σ permutes {..<n}" for σ
using that bij_convert unfolding bij_betw_def by blast
text ‹
We also need a small lemma showing that our tuples are stable under permutation of the roots.
›
have bij_betw_compose_perm:
"bij_betw (λf. restrict (λg. f (restrict (π ∘ g) X)) (X →⇩E Roots)) (tuples Y) (tuples Y)"
if π: "π permutes Roots" and "Y ∈ Roots_ms" for π Y
proof (rule bij_betwI)
have *: "(λf. restrict (λg. f (restrict (π ∘ g) X)) (X →⇩E Roots)) ∈ tuples Y → tuples Y"
if π: "π permutes Roots" for π
proof
fix f assume f: "f ∈ tuples Y"
hence f': "f ∈ (X →⇩E Roots) →⇩E X"
by (auto simp: tuples_def)
define f' where "f' = (λg. f (restrict (π ∘ g) X))"
have "f' ∈ (X →⇩E Roots) → X" unfolding f'_def
using f' bij_betw_apply[OF bij_betw_compose_left_perm_PiE[OF π, of X]] by blast
hence "restrict f' (X →⇩E Roots) ∈ (X →⇩E Roots) →⇩E X"
by simp
moreover have "image_mset (restrict f' (X →⇩E Roots)) (mset_set (X →⇩E Roots)) = Y"
proof -
have "image_mset (restrict f' (X →⇩E Roots)) (mset_set (X →⇩E Roots)) =
image_mset f' (mset_set (X →⇩E Roots))"
by (intro image_mset_cong) auto
also have "… = image_mset f (image_mset (λg. restrict (π ∘ g) X) (mset_set (X →⇩E Roots)))"
unfolding f'_def o_def multiset.map_comp by (simp add: o_def)
also have "image_mset (λg. restrict (π ∘ g) X) (mset_set (X →⇩E Roots)) =
mset_set (X →⇩E Roots)"
by (intro bij_betw_image_mset_set bij_betw_compose_left_perm_PiE π)
also have "image_mset f … = Y"
using f by (simp add: tuples_def)
finally show ?thesis .
qed
ultimately show "restrict f' (X →⇩E Roots) ∈ tuples Y"
by (auto simp: tuples_def)
qed
show "(λf. restrict (λg. f (restrict (π ∘ g) X)) (X →⇩E Roots)) ∈ tuples Y → tuples Y"
by (intro * π)
show "(λf. restrict (λg. f (restrict (inv_into UNIV π ∘ g) X)) (X →⇩E Roots)) ∈ tuples Y → tuples Y"
by (intro * permutes_inv π)
next
have *: "(λg∈X →⇩E Roots. (λg∈X →⇩E Roots. f (restrict (π ∘ g) X))
(restrict (inv_into UNIV π ∘ g) X)) = f" (is "?lhs = _")
if f: "f ∈ tuples Y" and π: "π permutes Roots" for f π
proof
fix g show "?lhs g = f g"
proof (cases "g ∈ X →⇩E Roots")
case True
have "restrict (π ∘ restrict (inv_into UNIV π ∘ g) X) X = g"
using True
by (intro ext) (auto simp: permutes_inverses[OF π])
thus ?thesis using True
by (auto simp: permutes_in_image[OF permutes_inv[OF π]])
qed (use f in ‹auto simp: tuples_def›)
qed
show "(λg∈X →⇩E Roots. (λg∈X →⇩E Roots. f (restrict (π ∘ g) X))
(restrict (inv_into UNIV π ∘ g) X)) = f" if "f ∈ tuples Y" for f
using *[OF that π] .
show "(λg∈X →⇩E Roots. (λg∈X →⇩E Roots. f (restrict (inv_into UNIV π ∘ g) X))
(restrict (π ∘ g) X)) = f" if "f ∈ tuples Y" for f
using *[OF that permutes_inv[OF π]] permutes_inv_inv[OF π] by simp
qed
text ‹
We show that the coefficients in the expanded new sum are rational -- again using the
fundamental theorem of symmetric polynomials.
›
define β' :: "complex multiset ⇒ complex"
where "β' = (λY. ∑f∈tuples Y. ∏g∈X →⇩E Roots. g (f g))"
have "β' Y ∈ ℚ" if Y: "Y ∈ Roots_ms" for Y
proof -
define Q :: "complex mpoly"
where "Q = (∑f∈tuples Y. ∏g∈X →⇩E Roots. Var (unRoot (g (f g))))"
have "insertion Root Q ∈ ℚ"
proof (rule symmetric_poly_of_roots_in_subring)
show "ring_closed (ℚ :: complex set)"
by standard auto
then interpret ring_closed "ℚ :: complex set" .
show "∀m. coeff Q m ∈ ℚ"
by (auto simp: Q_def coeff_Var when_def intro!: sum_in_Rats coeff_prod_closed)
next
show "symmetric_mpoly {..<n} Q"
unfolding symmetric_mpoly_def
proof safe
fix π assume π: "π permutes {..<n}"
define π' where "π' = convert_perm (inv_into UNIV π)"
have π': "π' permutes Roots"
unfolding π'_def by (intro permutes_convert_perm permutes_inv π)
have "mpoly_map_vars π Q = (∑f∈tuples Y. ∏g∈X →⇩E Roots. Var (π (unRoot (g (f g)))))"
unfolding Q_def by (simp add: permutes_bij[OF π])
also have "… = (∑f∈tuples Y. ∏g∈X →⇩E Roots. Var (unRoot (g (f (restrict (π' ∘ g) X)))))"
proof (rule sum.cong, goal_cases)
case (2 f)
have f: "f ∈ (X →⇩E Roots) →⇩E X"
using 2 by (auto simp: tuples_def)
have "(∏g∈X →⇩E Roots. Var (π (unRoot (g (f g))))) =
(∏g∈X →⇩E Roots. Var (π (unRoot (restrict (π' ∘ g) X (f (restrict (π' ∘ g) X))))))"
using π' by (intro prod.reindex_bij_betw [symmetric] bij_betw_compose_left_perm_PiE)
also have "… = (∏g∈X →⇩E Roots. Var (unRoot (g (f (restrict (π' ∘ g) X)))))"
proof (intro prod.cong refl arg_cong[of _ _ Var])
fix g assume g: "g ∈ X →⇩E Roots"
have "restrict (π' ∘ g) X ∈ X →⇩E Roots"
using bij_betw_compose_left_perm_PiE[OF π', of X] g unfolding bij_betw_def by blast
hence *: "f (restrict (π' ∘ g) X) ∈ X"
by (rule PiE_mem[OF f])
hence **: "g (f (restrict (π' ∘ g) X)) ∈ Roots"
by (rule PiE_mem[OF g])
have "unRoot (restrict (π' ∘ g) X (f (restrict (π' ∘ g) X))) =
unRoot (Root (inv_into UNIV π (unRoot (g (f (restrict (π' ∘ g) X))))))"
using * ** by (subst π'_def) (auto simp: convert_perm_def)
also have "inv_into UNIV π (unRoot (g (f (restrict (π' ∘ g) X)))) ∈ {..<n}"
using ** by (subst permutes_in_image[OF permutes_inv[OF π]]) auto
hence "unRoot (Root (inv_into UNIV π (unRoot (g (f (restrict (π' ∘ g) X)))))) =
inv_into UNIV π (unRoot (g (f (restrict (π' ∘ g) X))))"
by (intro unRoot_Root) auto
also have "π … = unRoot (g (f (restrict (π' ∘ g) X)))"
by (rule permutes_inverses[OF π])
finally show "π (unRoot (restrict (π' ∘ g) X (f (restrict (π' ∘ g) X)))) =
unRoot (g (f (restrict (π' ∘ g) X)))" .
qed
finally show ?case .
qed simp_all
also have "… = (∑x∈tuples Y. ∏g∈X →⇩E Roots. Var (unRoot (g ((λg∈X →⇩E Roots. x (restrict (π' ∘ g) X)) g))))"
by (intro sum.cong prod.cong refl) auto
also have "… = Q"
unfolding Q_def
by (rule sum.reindex_bij_betw[OF bij_betw_compose_perm]) (use π' Y in simp_all)
finally show "mpoly_map_vars π Q = Q" .
qed
next
show "vars Q ⊆ {..<n}"
unfolding Q_def
by (intro order.trans[OF vars_sum] UN_least order.trans[OF vars_prod])
(auto simp: vars_Var tuples_def)
next
define lc where "lc = Polynomial.lead_coeff P"
have "lc ≠ 0"
unfolding lc_def by auto
thus "inverse (of_int lc) * (of_int lc :: complex) = 1" and "inverse (of_int lc) ∈ ℚ"
by auto
have "rsquarefree (of_int_poly P :: complex poly)"
using ‹squarefree (of_int_poly P :: complex poly)› by (intro squarefree_imp_rsquarefree)
hence "of_int_poly P = Polynomial.smult (of_int lc) (∏x∈Roots. [:-x, 1:])"
unfolding lc_def of_int_hom.hom_lead_coeff[symmetric] Roots_def
by (rule complex_poly_decompose_rsquarefree [symmetric])
also have "(∏x∈Roots. [:-x, 1:]) = (∏i<n. [:-Root i, 1:])"
by (rule prod.reindex_bij_betw[OF Root, symmetric])
finally show "of_int_poly P = Polynomial.smult (of_int lc) (∏i<n. [:- Root i, 1:])" .
qed auto
also have "insertion Root Q = (∑f∈tuples Y. ∏g∈X →⇩E Roots. Root (unRoot (g (f g))))"
by (simp add: Q_def insertion_sum insertion_prod)
also have "… = β' Y"
unfolding β'_def by (intro sum.cong prod.cong refl Root_unRoot) (auto simp: tuples_def)
finally show ?thesis .
qed
hence "∀Y∈Roots_ms. ∃x. β' Y = of_rat x"
by (auto elim!: Rats_cases)
then obtain β'' :: "complex multiset ⇒ rat"
where β'': "⋀Y. Y ∈ Roots_ms ⟹ β' Y = of_rat (β'' Y)"
by metis
text ‹
We again collect all the terms that happen to have equal exponents and call their
coefficients ‹β''›:
›
define β''' :: "complex ⇒ rat" where "β''' = (λα. ∑Y∈Roots_ms. (β'' Y when ∑⇩#Y = α))"
have supp_β''': "{x. β''' x ≠ 0} ⊆ sum_mset ` Roots_ms"
by (auto simp: β'''_def when_def elim!: sum.not_neutral_contains_not_neutral split: if_splits)
text ‹
We again start with the sum that we now to be zero and multiply it with all the sums that can
be obtained with different choices for the roots.
›
have "0 = (∑x∈X. β x * exp x)"
using sum0 ..
also have "… = (∑x∈X. restrict β X x * exp x)"
by (intro sum.cong) auto
also have "… dvd (∏f ∈ X →⇩E Roots. ∑x∈X. f x * exp x)"
by (rule dvd_prodI) (use ‹β ` X ⊆ Roots› in ‹auto simp: id_def›)
also have "… = (∑f∈(X →⇩E Roots) →⇩E X. ∏g∈X →⇩E Roots. g (f g) * exp (f g))"
by (rule prod_sum_PiE) auto
also have "… = (∑f∈(X →⇩E Roots) →⇩E X. (∏g∈X →⇩E Roots. g (f g)) * exp (∑g∈X →⇩E Roots. f g))"
by (simp add: prod.distrib exp_sum)
also have "… = (∑(Y,f)∈Sigma Roots_ms tuples.
(∏g∈X →⇩E Roots. g (f g)) * exp (∑g∈X →⇩E Roots. f g))"
by (intro sum.reindex_bij_witness[of _ snd "λf. (image_mset f (mset_set (X →⇩E Roots)), f)"])
(auto simp: Roots_ms_def tuples_def)
also have "… = (∑(Y,f)∈Sigma Roots_ms tuples. (∏g∈X →⇩E Roots. g (f g)) * exp (∑⇩#Y))"
by (intro sum.cong) (auto simp: tuples_def sum_unfold_sum_mset)
also have "… = (∑Y∈Roots_ms. β' Y * exp (∑⇩#Y))"
unfolding β'_def sum_distrib_right by (rule sum.Sigma [symmetric]) auto
also have "… = (∑Y∈Roots_ms. of_rat (β'' Y) * exp (∑⇩#Y))"
by (intro sum.cong) (auto simp: β'')
also have "… = (∑Y∈Roots_ms. Sum_any (λα. of_rat (β'' Y when ∑⇩# Y = α) * exp α))"
proof (rule sum.cong, goal_cases)
case (2 Y)
have "Sum_any (λα. of_rat (β'' Y when ∑⇩# Y = α) * exp α) =
(∑α∈{∑⇩# Y}. of_rat (β'' Y when ∑⇩# Y = α) * exp α)"
by (intro Sum_any.expand_superset) auto
thus ?case by simp
qed auto
also have "… = Sum_any (λα. of_rat (β''' α) * exp α)"
unfolding β'''_def of_rat_sum sum_distrib_right by (subst Sum_any_sum_swap) auto
also have "… = (∑α | β''' α ≠ 0. of_rat (β''' α) * exp α)"
by (intro Sum_any.expand_superset finite_subset[OF supp_β''']) auto
finally have "(∑α | β''' α ≠ 0. of_rat (β''' α) * exp α) = 0"
by auto
text ‹
We are now in the situation of our previous version of the theorem and can apply it to find
that all the coefficients are zero.
›
have "{α. β''' α ≠ 0} = {}"
proof (rule Hermite_Lindemann_aux3)
show "finite {α. β''' α ≠ 0}"
by (rule finite_subset[OF supp_β''']) auto
next
show "(∑α | β''' α ≠ 0. of_rat (β''' α) * exp α) = 0"
by fact
next
fix α assume α: "α ∈ {α. β''' α ≠ 0}"
then obtain Y where Y: "Y ∈ Roots_ms" "α = sum_mset Y"
using supp_β''' by auto
thus "algebraic α" using alg1
by (auto simp: Roots_ms_def)
qed auto
text ‹
However, similarly to before, we can show that the coefficient corresponding to the
term with the lexicographically greatest exponent (which is obtained by picking the
term with the lexicographically greatest term in each of the factors of our big product)
is non-zero.
›
moreover have "∃α. β''' α ≠ 0"
proof -
define α_max where "α_max = complex_lex.Max X"
have [simp]: "α_max ∈ X"
unfolding α_max_def using ‹X ≠ {}› by (intro complex_lex.Max_in) auto
define Y_max :: "complex multiset" where "Y_max = replicate_mset (n ^ m) α_max"
define f_max where "f_max = restrict (λ_. α_max) (X →⇩E Roots)"
have [simp]: "Y_max ∈ Roots_ms"
by (auto simp: Y_max_def Roots_ms_def)
have "tuples Y_max = {f_max}"
proof safe
have "image_mset (λ_∈X →⇩E Roots. α_max) (mset_set (X →⇩E Roots)) =
image_mset (λ_. α_max) (mset_set (X →⇩E Roots))"
by (intro image_mset_cong) auto
thus "f_max ∈ tuples Y_max"
by (auto simp: f_max_def tuples_def Y_max_def image_mset_const_eq)
next
fix f assume "f ∈ tuples Y_max"
hence f: "f ∈ (X →⇩E Roots) →⇩E X" "image_mset f (mset_set (X →⇩E Roots)) = Y_max"
by (auto simp: tuples_def)
hence "∀g ∈# mset_set (X →⇩E Roots). f g = α_max"
by (intro image_mset_eq_replicate_msetD[where n = "n ^ m"]) (auto simp: Y_max_def)
thus "f = f_max"
using f by (auto simp: Y_max_def fun_eq_iff f_max_def)
qed
have "β''' (of_nat (n ^ m) * α_max) = (∑Y∈Roots_ms. β'' Y when ∑⇩# Y = of_nat (n ^ m) * α_max)"
unfolding β'''_def Roots_ms_def ..
also have "∑⇩# Y ≠ of_nat n ^ m * α_max" if "Y ∈ Roots_ms" "Y ≠ Y_max" for Y
proof -
have "¬set_mset Y ⊆ {α_max}"
using set_mset_subset_singletonD[of Y "α_max"] that
by (auto simp: Roots_ms_def Y_max_def split: if_splits)
then obtain y where y: "y ∈# Y" "y ≠ α_max"
by auto
have "y ∈ X" "set_mset (Y - {#y#}) ⊆ X"
using y that by (auto simp: Roots_ms_def dest: in_diffD)
hence "y ≤⇩ℂ α_max"
using y unfolding α_max_def by (intro complex_lex.Max_ge) auto
with y have "y <⇩ℂ α_max"
by auto
have *: "Y = {#y#} + (Y - {#y#})"
using y by simp
have "sum_mset Y = y + sum_mset (Y - {#y#})"
by (subst *) auto
also have "… <⇩ℂ α_max + sum_mset (Y - {#y#})"
by (intro complex_lex.add_strict_right_mono) fact
also have "… ≤⇩ℂ α_max + sum_mset (replicate_mset (n ^ m - 1) α_max)"
unfolding α_max_def using that y ‹set_mset (Y - {#y#}) ⊆ X›
by (intro complex_lex.add_left_mono sum_mset_mono_complex_lex
rel_mset_replicate_mset_right complex_lex.Max_ge)
(auto simp: Roots_ms_def size_Diff_singleton)
also have "… = of_nat (Suc (n ^ m - 1)) * α_max"
by (simp add: algebra_simps)
also have "Suc (n ^ m - 1) = n ^ m"
using ‹n > 0› by simp
finally show ?thesis by simp
qed
hence "(∑Y∈Roots_ms. β'' Y when ∑⇩# Y = of_nat (n ^ m) * α_max) = (∑Y∈{Y_max}. β'' Y when ∑⇩# Y = of_nat (n ^ m) * α_max)"
by (intro sum.mono_neutral_right ballI) auto
also have "… = β'' Y_max"
by (auto simp: when_def Y_max_def)
also have "of_rat … = β' Y_max"
using β''[of Y_max] by auto
also have "… = (∏g∈X →⇩E Roots. g (f_max g))"
by (auto simp: β'_def ‹tuples Y_max = {f_max}›)
also have "… = (∏g∈X →⇩E Roots. g α_max)"
by (intro prod.cong) (auto simp: f_max_def)
also have "… ≠ 0"
using ‹0 ∉ Roots› ‹α_max ∈ X› by (intro prod_nonzeroI) (metis PiE_mem)
finally show ?thesis by blast
qed
ultimately show False by blast
qed
subsection ‹The final theorem›
text ‹
We now additionally allow some of the $\beta_i$ to be zero:
›
lemma Hermite_Lindemann':
fixes β :: "complex ⇒ complex"
assumes "finite X"
assumes "⋀x. x ∈ X ⟹ algebraic x"
assumes "⋀x. x ∈ X ⟹ algebraic (β x)"
assumes "(∑x∈X. β x * exp x) = 0"
shows "∀x∈X. β x = 0"
proof -
have "{x∈X. β x ≠ 0} = {}"
proof (rule Hermite_Lindemann_aux4)
have "(∑x | x ∈ X ∧ β x ≠ 0. β x * exp x) = (∑x∈X. β x * exp x)"
by (intro sum.mono_neutral_left assms(1)) auto
also have "… = 0"
by fact
finally show "(∑x | x ∈ X ∧ β x ≠ 0. β x * exp x) = 0" .
qed (use assms in auto)
thus ?thesis by blast
qed
text ‹
Lastly, we switch to indexed summation in order to obtain a version of the theorem that
is somewhat nicer to use:
›
theorem Hermite_Lindemann:
fixes α β :: "'a ⇒ complex"
assumes "finite I"
assumes "⋀x. x ∈ I ⟹ algebraic (α x)"
assumes "⋀x. x ∈ I ⟹ algebraic (β x)"
assumes "inj_on α I"
assumes "(∑x∈I. β x * exp (α x)) = 0"
shows "∀x∈I. β x = 0"
proof -
define f where "f = inv_into I α"
have [simp]: "f (α x) = x" if "x ∈ I" for x
using that by (auto simp: f_def inv_into_f_f[OF assms(4)])
have "∀x∈α`I. (β ∘ f) x = 0"
proof (rule Hermite_Lindemann')
have "0 = (∑x∈I. β x * exp (α x))"
using assms(5) ..
also have "… = (∑x∈I. (β ∘ f) (α x) * exp (α x))"
by (intro sum.cong) auto
also have "… = (∑x∈α`I. (β ∘ f) x * exp x)"
using assms(4) by (subst sum.reindex) auto
finally show "(∑x∈α ` I. (β ∘ f) x * exp x) = 0" ..
qed (use assms in auto)
thus ?thesis by auto
qed
text ‹
The following version using lists instead of sequences is even more convenient to use
in practice:
›
corollary Hermite_Lindemann_list:
fixes xs :: "(complex × complex) list"
assumes alg: "∀(x,y)∈set xs. algebraic x ∧ algebraic y"
assumes distinct: "distinct (map snd xs)"
assumes sum0: "(∑(c,α)←xs. c * exp α) = 0"
shows "∀c∈(fst ` set xs). c = 0"
proof -
define n where "n = length xs"
have *: "∀i∈{..<n}. fst (xs ! i) = 0"
proof (rule Hermite_Lindemann)
from distinct have "inj_on (λi. map snd xs ! i) {..<n}"
by (intro inj_on_nth) (auto simp: n_def)
also have "?this ⟷ inj_on (λi. snd (xs ! i)) {..<n}"
by (intro inj_on_cong) (auto simp: n_def)
finally show "inj_on (λi. snd (xs ! i)) {..<n}" .
next
have "0 = (∑(c,α)←xs. c * exp α)"
using sum0 ..
also have "… = (∑i<n. fst (xs ! i) * exp (snd (xs ! i)))"
unfolding sum_list_sum_nth
by (intro sum.cong) (auto simp: n_def case_prod_unfold)
finally show "… = 0" ..
next
fix i assume i: "i ∈ {..<n}"
hence "(fst (xs ! i), snd (xs ! i)) ∈ set xs"
by (auto simp: n_def)
with alg show "algebraic (fst (xs ! i))" "algebraic (snd (xs ! i))"
by blast+
qed auto
show ?thesis
proof (intro ballI, elim imageE)
fix c x assume cx: "c = fst x" "x ∈ set xs"
then obtain i where "i ∈ {..<n}" "x = xs ! i"
by (auto simp: set_conv_nth n_def)
with * cx show "c = 0" by blast
qed
qed
subsection ‹The traditional formulation of the theorem›
text ‹
What we proved above was actually Baker's reformulation of the theorem. Thus, we now also derive
the original one, which uses linear independence and algebraic independence.
It states that if $\alpha_1, \ldots, \alpha_n$ are algebraic numbers that are linearly
independent over ‹ℤ›, then $e^{\alpha_1}, \ldots, e^{\alpha_n}$ are algebraically independent
over ‹ℚ›.
›
text ‹
Linear independence over the integers is just independence of a set of complex numbers when
viewing the complex numbers as a ‹ℤ›-module.
›
definition linearly_independent_over_int :: "'a :: field_char_0 set ⇒ bool" where
"linearly_independent_over_int = module.independent (λr x. of_int r * x)"
text ‹
Algebraic independence over the rationals means that the given set ‹X› of numbers fulfils
no non-trivial polynomial equation with rational coefficients, i.e. there is no non-zero
multivariate polynomial with rational coefficients that, when inserting the numbers from ‹X›,
becomes zero.
Note that we could easily replace `rational coefficients' with `algebraic coefficients' here
and the proof would still go through without any modifications.
›
definition algebraically_independent_over_rat :: "nat ⇒ (nat ⇒ 'a :: field_char_0) ⇒ bool" where
"algebraically_independent_over_rat n a ⟷
(∀p. vars p ⊆ {..<n} ∧ (∀m. coeff p m ∈ ℚ) ∧ insertion a p = 0 ⟶ p = 0)"
corollary Hermite_Lindemann_original:
fixes n :: nat and α :: "nat ⇒ complex"
assumes "inj_on α {..<n}"
assumes "⋀i. i < n ⟹ algebraic (α i)"
assumes "linearly_independent_over_int (α ` {..<n})"
shows "algebraically_independent_over_rat n (λi. exp (α i))"
unfolding algebraically_independent_over_rat_def
proof safe
fix p assume p: "vars p ⊆ {..<n}" "∀m. coeff p m ∈ ℚ" "insertion (λi. exp (α i)) p = 0"
define α' where "α' = (λm. ∑i<n. of_nat (lookup m i) * α i)"
define I where "I = {m. coeff p m ≠ 0}"
have lookup_eq_0: "lookup m i = 0" if "m ∈ I" "i ∉ {..<n}" for i m
proof -
have "keys m ⊆ vars p"
using that coeff_notin_vars[of m p] by (auto simp: I_def)
thus "lookup m i = 0"
using in_keys_iff[of i m] that p(1) by blast
qed
have "∀x∈I. coeff p x = 0"
proof (rule Hermite_Lindemann)
show "finite I"
by (auto simp: I_def)
next
show "algebraic (α' m)" if "m ∈ I" for m
unfolding α'_def using assms(2) by fastforce
next
show "algebraic (coeff p m)" if "m ∈ I" for m
unfolding α'_def using p(2) by blast
next
show "inj_on α' I"
proof
fix m1 m2 assume m12: "m1 ∈ I" "m2 ∈ I" "α' m1 = α' m2"
define lu :: "(nat ⇒⇩0 nat) ⇒ nat ⇒ int" where "lu = (λm i. int (lookup m i))"
interpret int: Modules.module "λr x. of_int r * (x :: complex)"
by standard (auto simp: algebra_simps of_rat_mult of_rat_add)
define idx where "idx = inv_into {..<n} α"
have "lu m1 i = lu m2 i" if "i < n" for i
proof -
have "lu m1 (idx (α i)) - lu m2 (idx (α i)) = 0"
proof (rule int.independentD)
show "int.independent (α ` {..<n})"
using assms(3) by (simp add: linearly_independent_over_int_def)
next
have "(∑x∈α`{..<n}. of_int (lu m1 (idx x) - lu m2 (idx x)) * x) =
(∑i<n. of_int (lu m1 (idx (α i)) - lu m2 (idx (α i))) * α i)"
using assms(1) by (subst sum.reindex) auto
also have "… = (∑i<n. of_int (lu m1 i - lu m2 i) * α i)"
by (intro sum.cong) (auto simp: idx_def inv_into_f_f[OF assms(1)])
also have "… = 0"
using m12 by (simp add: α'_def ring_distribs of_rat_diff sum_subtractf lu_def)
finally show "(∑x∈α`{..<n}. of_int (lu m1 (idx x) - lu m2 (idx x)) * x) = 0"
by (simp add: α'_def ring_distribs of_rat_diff sum_subtractf lu_def)
qed (use that in auto)
thus ?thesis
using that by (auto simp: idx_def inv_into_f_f[OF assms(1)])
qed
hence "lookup m1 i = lookup m2 i" for i
using m12 by (cases "i < n") (auto simp: lu_def lookup_eq_0)
thus "m1 = m2"
by (rule poly_mapping_eqI)
qed
next
have "0 = insertion (λi. exp (α i)) p"
using p(3) ..
also have "… = (∑m∈I. coeff p m * Prod_any (λi. exp (α i) ^ lookup m i))"
unfolding insertion_altdef by (rule Sum_any.expand_superset) (auto simp: I_def)
also have "… = (∑m∈I. coeff p m * exp (α' m))"
proof (intro sum.cong, goal_cases)
case (2 m)
have "Prod_any (λi. exp (α i) ^ lookup m i) = (∏i<n. exp (α i) ^ lookup m i)"
using 2 lookup_eq_0[of m] by (intro Prod_any.expand_superset; force)
also have "… = exp (α' m)"
by (simp add: exp_sum exp_of_nat_mult α'_def)
finally show ?case by simp
qed simp_all
finally show "(∑m∈I. coeff p m * exp (α' m)) = 0" ..
qed
thus "p = 0"
by (intro mpoly_eqI) (auto simp: I_def)
qed
subsection ‹Simple corollaries›
text ‹
Now, we derive all the usual obvious corollaries of the theorem in the obvious way.
First, the exponential of a non-zero algebraic number is transcendental.
›
corollary algebraic_exp_complex_iff:
assumes "algebraic x"
shows "algebraic (exp x :: complex) ⟷ x = 0"
using Hermite_Lindemann_list[of "[(1, x), (-exp x, 0)]"] assms by auto
text ‹
More generally, any sum of exponentials with algebraic coefficients and exponents is
transcendental if the exponents are all distinct and non-zero and at least one coefficient
is non-zero.
›
corollary sum_of_exp_transcendentalI:
fixes xs :: "(complex × complex) list"
assumes "∀(x,y)∈set xs. algebraic x ∧ algebraic y ∧ y ≠ 0"
assumes "∃x∈fst`set xs. x ≠ 0"
assumes distinct: "distinct (map snd xs)"
shows "¬algebraic (∑(c,α)←xs. c * exp α)"
proof
define S where "S = (∑(c,α)←xs. c * exp α)"
assume S: "algebraic S"
have "∀c∈fst`set ((-S,0) # xs). c = 0"
proof (rule Hermite_Lindemann_list)
show "(∑(c, α)←(- S, 0) # xs. c * exp α) = 0"
by (auto simp: S_def)
qed (use S assms in auto)
with assms(2) show False
by auto
qed
text ‹
Any complex logarithm of an algebraic number other than 1 is transcendental
(no matter which branch cut).
›
corollary transcendental_complex_logarithm:
assumes "algebraic x" "exp y = (x :: complex)" "x ≠ 1"
shows "¬algebraic y"
using algebraic_exp_complex_iff[of y] assms by auto
text ‹
In particular, this holds for the standard branch of the logarithm.
›
corollary transcendental_Ln:
assumes "algebraic x" "x ≠ 0" "x ≠ 1"
shows "¬algebraic (Ln x)"
by (rule transcendental_complex_logarithm) (use assms in auto)
text ‹
The transcendence of ‹e› and ‹π›, which I have already formalised directly in other AFP
entries, now follows as a simple corollary.
›
corollary exp_1_complex_transcendental: "¬algebraic (exp 1 :: complex)"
by (subst algebraic_exp_complex_iff) auto
corollary pi_transcendental: "¬algebraic pi"
proof -
have "¬algebraic (𝗂 * pi)"
by (rule transcendental_complex_logarithm[of "-1"]) auto
thus ?thesis by simp
qed
subsection ‹Transcendence of the trigonometric and hyperbolic functions›
text ‹
In a similar fashion, we can also prove the transcendence of all the trigonometric and
hyperbolic functions such as $\sin$, $\tan$, $\sinh$, $\arcsin$, etc.
›
lemma transcendental_sinh:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (sinh z :: complex)"
proof -
have "¬algebraic (∑(a,b)←[(1/2, z), (-1/2, -z)]. a * exp b)"
using assms by (intro sum_of_exp_transcendentalI) auto
also have "(∑(a,b)←[(1/2, z), (-1/2, -z)]. a * exp b) = sinh z"
by (simp add: sinh_def field_simps scaleR_conv_of_real)
finally show ?thesis .
qed
lemma transcendental_cosh:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (cosh z :: complex)"
proof -
have "¬algebraic (∑(a,b)←[(1/2, z), (1/2, -z)]. a * exp b)"
using assms by (intro sum_of_exp_transcendentalI) auto
also have "(∑(a,b)←[(1/2, z), (1/2, -z)]. a * exp b) = cosh z"
by (simp add: cosh_def field_simps scaleR_conv_of_real)
finally show ?thesis .
qed
lemma transcendental_sin:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (sin z :: complex)"
unfolding sin_conv_sinh using transcendental_sinh[of "𝗂 * z"] assms by simp
lemma transcendental_cos:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (cos z :: complex)"
unfolding cos_conv_cosh using transcendental_cosh[of "𝗂 * z"] assms by simp
lemma tan_square_neq_neg1: "tan (z :: complex) ^ 2 ≠ -1"
proof
assume "tan z ^ 2 = -1"
hence "sin z ^ 2 = -(cos z ^ 2)"
by (auto simp: tan_def divide_simps split: if_splits)
also have "cos z ^ 2 = 1 - sin z ^ 2"
by (simp add: cos_squared_eq)
finally show False
by simp
qed
lemma transcendental_tan:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (tan z :: complex)"
proof
assume "algebraic (tan z)"
have nz1: "real_of_int n + 1 / 2 ≠ 0" for n
proof -
have "real_of_int (2 * n + 1) / real_of_int 2 ∉ ℤ"
by (intro fraction_not_in_ints) auto
also have "real_of_int (2 * n + 1) / real_of_int 2 = real_of_int n + 1 / 2"
by simp
finally show "… ≠ 0"
by auto
qed
have nz2: "1 + tan z ^ 2 ≠ 0"
using tan_square_neq_neg1[of z] by (subst add_eq_0_iff)
have nz3: "cos z ≠ 0"
proof
assume "cos z = 0"
then obtain n where "z = complex_of_real (real_of_int n * pi) + complex_of_real pi / 2"
by (subst (asm) cos_eq_0) blast
also have "… = complex_of_real ((real_of_int n + 1 / 2) * pi)"
by (simp add: ring_distribs)
also have "algebraic … ⟷ algebraic ((real_of_int n + 1 / 2) * pi)"
by (rule algebraic_of_real_iff)
also have "¬algebraic ((real_of_int n + 1 / 2) * pi)"
using nz1[of n] transcendental_pi by simp
finally show False using assms(1) by contradiction
qed
from nz3 have *: "sin z ^ 2 = tan z ^ 2 * cos z ^ 2"
by (simp add: tan_def field_simps)
also have "cos z ^ 2 = 1 - sin z ^ 2"
by (simp add: cos_squared_eq)
finally have "sin z ^ 2 * (1 + tan z ^ 2) = tan z ^ 2"
by (simp add: algebra_simps)
hence "sin z ^ 2 = tan z ^ 2 / (1 + tan z ^ 2)"
using nz2 by (simp add: field_simps)
also have "algebraic (tan z ^ 2 / (1 + tan z ^ 2))"
using ‹algebraic (tan z)› by auto
finally have "algebraic (sin z ^ 2)" .
hence "algebraic (sin z)"
by simp
thus False
using transcendental_sin[OF ‹algebraic z› ‹z ≠ 0›] by contradiction
qed
lemma transcendental_cot:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (cot z :: complex)"
proof -
have "¬algebraic (tan z)"
by (rule transcendental_tan) fact+
also have "algebraic (tan z) ⟷ algebraic (inverse (tan z))"
by simp
also have "inverse (tan z) = cot z"
by (simp add: cot_def tan_def)
finally show ?thesis .
qed
lemma transcendental_tanh:
assumes "algebraic z" "z ≠ 0" "cosh z ≠ 0"
shows "¬algebraic (tanh z :: complex)"
using transcendental_tan[of "𝗂 * z"] assms unfolding tanh_conv_tan by simp
lemma transcendental_Arcsin:
assumes "algebraic z" "z ≠ 0"
shows "¬algebraic (Arcsin z)"
proof -
have "𝗂 * z + csqrt (1 - z⇧2) ≠ 0"
using Arcsin_body_lemma by blast
moreover have "𝗂 * z + csqrt (1 - z⇧2) ≠ 1"
proof
assume "𝗂 * z + csqrt (1 - z⇧2) = 1"
hence "Arcsin z = 0"
by (simp add: Arcsin_def)
hence "sin (Arcsin z) = 0"
by (simp only: sin_zero)
also have "sin (Arcsin z) = z"
by simp
finally show False using ‹z ≠ 0› by simp
qed
ultimately have "¬ algebraic (Ln (𝗂 * z + csqrt (1 - z⇧2)))"
using assms by (intro transcendental_Ln) auto
thus ?thesis
by (simp add: Arcsin_def)
qed
lemma transcendental_Arccos:
assumes "algebraic z" "z ≠ 1"
shows "¬algebraic (Arccos z)"
proof -
have "z + 𝗂 * csqrt (1 - z⇧2) ≠ 0"
using Arccos_body_lemma by blast
moreover have "z + 𝗂 * csqrt (1 - z⇧2) ≠ 1"
proof
assume "z + 𝗂 * csqrt (1 - z⇧2) = 1"
hence "Arccos z = 0"
by (simp add: Arccos_def)
hence "cos (Arccos z) = 1"
by (simp only: cos_zero)
also have "cos (Arccos z) = z"
by simp
finally show False using ‹z ≠ 1› by simp
qed
ultimately have "¬ algebraic (Ln (z + 𝗂 * csqrt (1 - z⇧2)))"
using assms by (intro transcendental_Ln) auto
thus ?thesis
by (simp add: Arccos_def)
qed
lemma transcendental_Arctan:
assumes "algebraic z" "z ∉ {0, 𝗂, -𝗂}"
shows "¬algebraic (Arctan z)"
proof -
have "𝗂 * z ≠ 1" "1 + 𝗂 * z ≠ 0"
using assms(2) by (auto simp: complex_eq_iff)
hence "¬ algebraic (Ln ((1 - 𝗂 * z) / (1 + 𝗂 * z)))"
using assms by (intro transcendental_Ln) auto
thus ?thesis
by (simp add: Arctan_def)
qed
end