Transcendence and irrationality

Hermite–Lindemann, Lindemann–Weierstrass, Gelfond–Schneider, Mahler functions, irrationality and linear independence of constants.

TheoremCalegari–Dimitrov–Tang linear independence theorems#●ready to prove

Let \(\chi : \mathbb{Z}/3\mathbb{Z} \to \mathbb{C}\) be given by \(\chi(0) = 0\), \(\chi(1) = 1\) and \(\chi(2) = -1\) (the nontrivial Dirichlet character modulo \(3\)), let \(\zeta\) be the Riemann zeta function and let \(L(s, \chi)\) be the Dirichlet \(L\)-function of \(\chi\). Then the complex numbers \(1\), \(\zeta(2)\) and \(L(2, \chi)\) are linearly independent over \(\mathbb{Q}\). Moreover, let \(m\) and \(n\) be integers, neither of them equal to \(-1\) or \(0\), with \(10^6 |m - n| < |n|\), and put \(\ell_m = \log(1 + 1/m)\) and \(\ell_n = \log(1 + 1/n)\). Then \(\ell_m \ell_n\) is irrational, and if \(m \ne n\), the real numbers \(1\), \(\ell_m\), \(\ell_n\) and \(\ell_m \ell_n\) are linearly independent over \(\mathbb{Q}\).

public theorem_wanted cdt_linearIndependent :
    letI χ : ZMod 3 → ℂ := ![0, 1, -1]
    LinearIndependent ℚ ![1, riemannZeta 2, ZMod.LFunction χ 2] ∧
    ∀ m n : ℤ, m ≠ -1 → m ≠ 0 → n ≠ -1 → n ≠ 0 → 10 ^ 6 * |m - n| < |n| →
      letI lm := Real.log (1 + 1 / m)
      letI ln := Real.log (1 + 1 / n)
      Irrational (lm * ln) ∧
      (m ≠ n → LinearIndependent ℚ ![1, lm, ln, lm * ln])
Sources
  • https://arxiv.org/abs/2408.15403. Problem cdt_linearIndependent of the lean-eval benchmark.

TheoremHermite–Lindemann theorem#✓fully proved

If \(\alpha\) is a nonzero complex number that is algebraic over \(\mathbb{Q}\), then \(e^{\alpha}\) is transcendental over \(\mathbb{Q}\).

theorem hermite_lindemann :
    ∀ (α : ℂ), α ≠ 0 → IsAlgebraic ℚ α → Transcendental ℚ (Complex.exp α)
Sources
  • C. Hermite, Sur la fonction exponentielle, C. R. Acad. Sci. Paris 77 (1873) for e; F. von Lindemann, Über die Zahl π, Math. Ann. 20 (1882) 213–225 extension to π; textbook in Baker, Transcendental Number Theory
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.