Formal exponential sums

A formal exponential sum with coefficients and exponents in a commutative ring K is an element x = ∑ δ_γ [γ] of the additive monoid algebra K[K], where [γ] * [γ'] = [γ + γ']. This file develops the two operations on such sums used in the Hermite–Lindemann proof of the Lindemann–Weierstrass theorem.

• expEval K : K[K] →ₐ[K] ℂ evaluates a formal sum at the exponential function, ∑ δ_γ [γ] ↦ ∑ δ_γ exp γ, for any K-algebra structure on ℂ. It is the algebra lift of the exponential character, so it is multiplicative by construction. For an intermediate field L of ℂ / ℚ the Lindemann–Weierstrass theorem states that expEval L is injective when L consists of algebraic numbers; it is not injective for L = ⊤, since exp (2πi) = exp 0.
• galConj τ : K[K] ≃ₐ[F] K[K] is the conjugation ∑ δ_γ [γ] ↦ ∑ τ(δ_γ) [τ γ] by an automorphism τ of the F-algebra K, acting simultaneously on coefficients and exponents. It is a group homomorphism in τ, and a sum is fixed by every galConj τ exactly when each τ sends its coefficient at γ to its coefficient at τ γ (forall_galConj_eq_iff). Taking the product of all conjugates produces fixed sums (galConj_prod_galConj), which is how the proof reduces the general theorem to Galois-invariant exponential relations.

The evaluation is not Galois-equivariant: expEval of galConj τ x is in general a different complex number from expEval x.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.2, Theorem 4.11.
• Y. Zhao, formalization of the Lindemann–Weierstrass theorem in Lean, Basic.lean, the proof of algebraicIndependent_exp, which works with exponential sums in AddMonoidAlgebra.

noncomputable def TauCeti.LindemannWeierstrass.galConj {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) : AddMonoidAlgebra K K ≃ₐ[F] AddMonoidAlgebra K K

Conjugation of formal exponential sums ∑ δ_γ [γ] ↦ ∑ τ(δ_γ) [τ γ] by an automorphism τ of the F-algebra K, acting on coefficients and exponents simultaneously.

@[simp]

theorem TauCeti.LindemannWeierstrass.coeff_galConj {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) (x : AddMonoidAlgebra K K) (γ : K) : ((galConj τ) x).coeff γ = τ (x.coeff (τ.symm γ))

The coefficient of galConj τ x at γ is the conjugate of the coefficient of x at τ⁻¹ γ.

theorem TauCeti.LindemannWeierstrass.coeff_galConj_apply {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) (x : AddMonoidAlgebra K K) (γ : K) : ((galConj τ) x).coeff (τ γ) = τ (x.coeff γ)

The coefficient of galConj τ x at τ γ is the conjugate of the coefficient of x at γ.

@[simp]

theorem TauCeti.LindemannWeierstrass.galConj_single {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) (γ δ : K) : (galConj τ) (AddMonoidAlgebra.single γ δ) = AddMonoidAlgebra.single (τ γ) (τ δ)

Conjugation sends the monomial δ [γ] to τ(δ) [τ γ].

@[simp]

theorem TauCeti.LindemannWeierstrass.galConj_refl {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] : galConj AlgEquiv.refl = AlgEquiv.refl

Conjugation by the identity is the identity.

@[simp]

theorem TauCeti.LindemannWeierstrass.galConj_trans {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ σ : K ≃ₐ[F] K) : galConj (τ.trans σ) = (galConj τ).trans (galConj σ)

Conjugation is compatible with composition of automorphisms.

@[simp]

theorem TauCeti.LindemannWeierstrass.galConj_symm {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) : (galConj τ).symm = galConj τ.symm

The inverse of conjugation by τ is conjugation by τ⁻¹.

@[simp]

theorem TauCeti.LindemannWeierstrass.support_galConj {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (τ : K ≃ₐ[F] K) (x : AddMonoidAlgebra K K) : ((galConj τ) x).coeff.support = Finset.map (↑τ).toEmbedding x.coeff.support

Conjugation moves the support of a formal sum by τ.

theorem TauCeti.LindemannWeierstrass.forall_galConj_eq_iff {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] {x : AddMonoidAlgebra K K} : (∀ (τ : K ≃ₐ[F] K), (galConj τ) x = x) ↔ ∀ (τ : K ≃ₐ[F] K) (γ : K), x.coeff (τ γ) = τ (x.coeff γ)

A formal sum is fixed by every conjugation exactly when each automorphism maps its coefficient at γ to its coefficient at τ γ.

theorem TauCeti.LindemannWeierstrass.galConj_prod_galConj {F : Type u_1} {K : Type u_2} [CommSemiring F] [CommSemiring K] [Algebra F K] [Fintype (K ≃ₐ[F] K)] (σ : K ≃ₐ[F] K) (x : AddMonoidAlgebra K K) : (galConj σ) (∏ τ : K ≃ₐ[F] K, (galConj τ) x) = ∏ τ : K ≃ₐ[F] K, (galConj τ) x

The product of all conjugates of a formal sum is fixed by every conjugation.

noncomputable def TauCeti.LindemannWeierstrass.expEval (K : Type u_1) [CommSemiring K] [Algebra K ℂ] : AddMonoidAlgebra K K →ₐ[K] ℂ

Evaluation of formal exponential sums at the exponential function, ∑ δ_γ [γ] ↦ ∑ δ_γ exp γ.

@[simp]

theorem TauCeti.LindemannWeierstrass.expEval_single {K : Type u_1} [CommSemiring K] [Algebra K ℂ] (γ c : K) : (expEval K) (AddMonoidAlgebra.single γ c) = (algebraMap K ℂ) c * Complex.exp ((algebraMap K ℂ) γ)

The exponential evaluation of the monomial c [γ] is c * exp γ.

theorem TauCeti.LindemannWeierstrass.expEval_apply {K : Type u_1} [CommSemiring K] [Algebra K ℂ] (x : AddMonoidAlgebra K K) : (expEval K) x = ∑ γ ∈ x.coeff.support, (algebraMap K ℂ) (x.coeff γ) * Complex.exp ((algebraMap K ℂ) γ)

The exponential evaluation of ∑ δ_γ [γ] is the finite sum ∑ δ_γ exp γ.

Examples