Exponentials of nonzero rational arguments are transcendental

The elementary rounding kernels also encounter algebraic boundaries, for example when a hyperbolic function is written in terms of an exponential. Irrationality alone does not rule out equality with those boundaries.

The proof uses mathlib’s Lindemann–Weierstrass polynomial approximation at finitely many integer roots at once. An assumed integer linear relation between their exponentials gives a nonzero integer whose absolute value tends to zero. Applying this to the powers in a polynomial proves transcendence.

theorem FloatLib.Numerics.Enclosure.int_add_sum_exp_intCast_ne_zero {ι : Type u_1} (s : Finset ι) (argument : ι → ℤ) (hargument : ∀ k ∈ s, argument k ≠ 0) (a : ι → ℤ) (a₀ : ℤ) (ha₀ : a₀ ≠ 0) : ↑a₀ + ∑ k ∈ s, ↑(a k) * Real.exp ↑(argument k) ≠ 0

An integer linear combination of exponentials at nonzero integer arguments cannot cancel a nonzero integer constant.

theorem FloatLib.Numerics.Enclosure.transcendental_int_exp_intCast (m : ℤ) (hm : m ≠ 0) : Transcendental ℤ (Real.exp ↑m)

A nonzero integer argument has an exponential transcendental over the integers.

theorem FloatLib.Numerics.Enclosure.transcendental_exp_intCast (m : ℤ) (hm : m ≠ 0) : Transcendental ℚ (Real.exp ↑m)

A nonzero integer argument has an exponential transcendental over the rationals.

theorem FloatLib.Numerics.Enclosure.transcendental_exp_ratCast (q : ℚ) (hq : q ≠ 0) : Transcendental ℚ (Real.exp ↑q)

Every nonzero rational argument has a transcendental exponential.