Hermite's integral

For a complex polynomial f and z : ℂ, Hermite's integral is F_f(z) = z ∫₀¹ exp (z (1 - t)) f(z t) dt, the integral of exp (z - u) f(u) along the segment from 0 to z. Integration by parts evaluates it in terms of the sum of all derivatives sumIDeriv f = f + f' + f'' + ⋯: F_f(z) = exp z * (sumIDeriv f)(0) - (sumIDeriv f)(z) (Polynomial.hermiteIntegral_eq_sumIDeriv).

This identity is the analytic input to Hermite's proof of the transcendence of e and to the Hermite–Lindemann proof of the Lindemann–Weierstrass theorem. For a vanishing exponential relation ∑ δⱼ exp γⱼ = 0 it shows that the polynomial expression -∑ δⱼ (sumIDeriv f)(γⱼ) (an algebraic number when the coefficients of f, the weights δⱼ and the points γⱼ are algebraic) equals the analytic quantity ∑ δⱼ F_f(γⱼ) (Polynomial.sum_mul_hermiteIntegral_of_sum_mul_exp_eq_zero), which the elementary estimate ‖F_f(z)‖ ≤ ‖z‖ exp ‖z‖ C (Polynomial.norm_hermiteIntegral_le) makes small for well-chosen auxiliary polynomials f.

Main declarations

• Polynomial.hermiteIntegral f z: Hermite's integral z ∫₀¹ exp (z (1 - t)) f(z t) dt.
• Polynomial.hermiteIntegral_eq_sumIDeriv: the evaluation by integration by parts.
• Polynomial.hermiteIntegral_eq_exp_mul_integral: the equivalent form with kernel exp (-t z).
• Polynomial.norm_hermiteIntegral_le: the bound ‖F_f(z)‖ ≤ ‖z‖ exp ‖z‖ C.
• Polynomial.sum_mul_hermiteIntegral_of_sum_mul_exp_eq_zero: the value of ∑ δⱼ F_f(γⱼ) along a vanishing exponential relation.

Implementation notes

Mathlib's Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (Y. Zhao) proves the same integration by parts for the kernel exp (-t z) in its module-private lemmas LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv and LindemannWeierstrass.integral_exp_mul_eval; the derivative computation here follows them. Since they are not exported, this file states Hermite's integral and its estimates as public API.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.1, Lemma 4.2, Corollary 4.3 and Lemma 4.4, and §4.2, Lemma 4.12.

noncomputable def Polynomial.hermiteIntegral (f : Polynomial ℂ) (z : ℂ) : ℂ

Hermite's integral F_f(z) = z ∫₀¹ exp ((1 - t) z) f(t z) dt of a complex polynomial f, the integral of exp (z - u) f(u) along the segment from 0 to z.

theorem Polynomial.hermiteIntegral_eq_sumIDeriv (f : Polynomial ℂ) (z : ℂ) : f.hermiteIntegral z = Complex.exp z * eval 0 (sumIDeriv f) - eval z (sumIDeriv f)

Hermite's identity: integration by parts evaluates Hermite's integral as F_f(z) = exp z * (sumIDeriv f)(0) - (sumIDeriv f)(z).

theorem Polynomial.hermiteIntegral_eq_exp_mul_integral (f : Polynomial ℂ) (z : ℂ) : f.hermiteIntegral z = Complex.exp z * (z * ∫ (t : ℝ) in 0..1, Complex.exp (-(t • z)) * eval (t • z) f)

Hermite's integral with the kernel exp (-t z): F_f(z) = exp z * (z ∫₀¹ exp (-t z) f(t z) dt).

theorem Polynomial.norm_hermiteIntegral_le {f : Polynomial ℂ} {z : ℂ} {C : ℝ} (hC : ∀ (u : ℂ), ‖u‖ ≤ ‖z‖ → ‖eval u f‖ ≤ C) : ‖f.hermiteIntegral z‖ ≤ ‖z‖ * Real.exp ‖z‖ * C

Hermite's estimate: if C bounds ‖f‖ on the closed disc of radius ‖z‖, then ‖F_f(z)‖ ≤ ‖z‖ exp ‖z‖ C.

@[simp]

theorem Polynomial.hermiteIntegral_zero_right (f : Polynomial ℂ) : f.hermiteIntegral 0 = 0

Hermite's integral vanishes at z = 0.

@[simp]

theorem Polynomial.hermiteIntegral_zero_left (z : ℂ) : hermiteIntegral 0 z = 0

Hermite's integral of the zero polynomial vanishes.

@[simp]

theorem Polynomial.hermiteIntegral_add (f g : Polynomial ℂ) (z : ℂ) : (f + g).hermiteIntegral z = f.hermiteIntegral z + g.hermiteIntegral z

Hermite's integral is additive in the polynomial.

@[simp]

theorem Polynomial.hermiteIntegral_smul (c : ℂ) (f : Polynomial ℂ) (z : ℂ) : (c • f).hermiteIntegral z = c • f.hermiteIntegral z

Hermite's integral is homogeneous in the polynomial.

@[simp]

theorem Polynomial.hermiteIntegral_C_mul (c : ℂ) (f : Polynomial ℂ) (z : ℂ) : (C c * f).hermiteIntegral z = c * f.hermiteIntegral z

Hermite's integral of C c * f is c times that of f.

@[simp]

theorem Polynomial.hermiteIntegral_neg (f : Polynomial ℂ) (z : ℂ) : (-f).hermiteIntegral z = -f.hermiteIntegral z

Hermite's integral commutes with negation of the polynomial.

@[simp]

theorem Polynomial.hermiteIntegral_sub (f g : Polynomial ℂ) (z : ℂ) : (f - g).hermiteIntegral z = f.hermiteIntegral z - g.hermiteIntegral z

Hermite's integral commutes with subtraction of polynomials.

@[simp]

theorem Polynomial.hermiteIntegral_sum {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℂ) (z : ℂ) : (∑ i ∈ s, f i).hermiteIntegral z = ∑ i ∈ s, (f i).hermiteIntegral z

Hermite's integral commutes with finite sums of polynomials.

@[simp]

theorem Polynomial.hermiteIntegral_C (c z : ℂ) : (C c).hermiteIntegral z = c * (Complex.exp z - 1)

Hermite's integral of a constant c is c (exp z - 1).

@[simp]

theorem Polynomial.hermiteIntegral_one (z : ℂ) : hermiteIntegral 1 z = Complex.exp z - 1

Hermite's integral of the constant polynomial 1 is exp z - 1.

@[simp]

theorem Polynomial.hermiteIntegral_X (z : ℂ) : X.hermiteIntegral z = Complex.exp z - z - 1

Hermite's integral of X is exp z - z - 1.

theorem Polynomial.sum_mul_hermiteIntegral_of_sum_mul_exp_eq_zero {ι : Type u_1} (s : Finset ι) (δ γ : ι → ℂ) (h : ∑ j ∈ s, δ j * Complex.exp (γ j) = 0) (f : Polynomial ℂ) : ∑ j ∈ s, δ j * f.hermiteIntegral (γ j) = -∑ j ∈ s, δ j * eval (γ j) (sumIDeriv f)

Hermite's integral along an exponential relation: if ∑ δⱼ exp γⱼ = 0, then ∑ δⱼ F_f(γⱼ) = -∑ δⱼ (sumIDeriv f)(γⱼ), so that the right-hand side (algebraic when the coefficients of f, the weights δⱼ and the points γⱼ are algebraic) is controlled by the analytic left-hand side.