Schanuel's Conjecture

Reference: Wikipedia

@[reducible, inline]

abbrev transcendenceDegree (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) : ℕ

The transcendence degree of an $A$-algebra is the common cardinality of transcendence bases.

Equations

• transcendenceDegree R h = Set.univ.ncard

theorem isTranscendenceBasis_ncard_eq_transcendenceDegree (R : Type u_1) {A : Type u_2} {ι : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) (𝒷 : ι → A) (hS : IsTranscendenceBasis R 𝒷) : Set.univ.ncard = transcendenceDegree R h

The transcendence degree is independent of the choice of a transcendence basis.

theorem adjoin_transcendenceDegree_le_of_finite {A : Type u_1} {ι : Type u_2} [Field A] {S : Set A} (hS : S.Finite) : transcendenceDegree A ⋯ ≤ S.ncard

The transcendence degree of $A$ adjoined $\{x_1, ..., x_n\}$ is $\leq n$.

theorem schanuels_conjecture (n : ℕ) (z : Fin n → ℂ) (h : LinearIndependent ℚ z) : let hinj := ⋯; n ≤ transcendenceDegree ℚ hinj

Given any set of $n$ complex numbers $\{z_1, ..., z_n\}$ that are linearly independent over $\mathbb{Q}$, the field extension $\mathbb{Q}(z_1, ..., z_n, e^{z_1}, ..., e^{z_n})$ has transcendence degree at least $n$ over $\mathbb{Q}$.

Consequences of Schanuel's conjecture

theorem four_exponentials {z₁ z₂ w₁ w₂ : ℂ} (hz : LinearIndependent ℚ ![z₁, z₂]) (hw : LinearIndependent ℚ ![w₁, w₂]) : ∃ z ∈ {Complex.exp (z₁ * w₁), Complex.exp (z₁ * w₂), Complex.exp (z₂ * w₁), Complex.exp (z₂ * w₂)}, Transcendental ℚ z

The four exponentials conjecture would follow from Schanuel's conjecture: if $z_2, z_2$ and $w_1, w_2$ are two pairs of complex numbers, with each pair being linearly independent over the rational numbers, then at least one of the following four numbers is transcendental $$ e^{z_1w_1}, e^{z_1w_2}, e^{z_2w_1}, e^{z_2w_2}. $$

theorem exists_transcendental_of_two_pow_irrat_three_pow_irrat {t : ℝ} (h : Irrational t) : Irrational (2 ^ t) ∨ Irrational (3 ^ t)

The four exponential conjecture would imply that for any irrational number $t$, at least one of the numbers $2^t$ and $3^t$ is transcendental.

A number of nontrivial combinations of $e$, $\pi$ and elementary functions may also be proven to the transcendental should Schanuel's conjecture hold.

theorem exp_add_pi_transcendental : Transcendental ℚ (Real.exp 1 + Real.pi)

$e + \pi$ is transcendental.

theorem exp_mul_pi_transcendental : Transcendental ℚ (Real.exp 1 * Real.pi)

$e\pi$ is transcendental.

theorem exp_pow_pi_sq_transcendental : Transcendental ℚ (Real.exp (Real.pi ^ 2))

$e^{\pi^2}$ is transcendental.

theorem exp_exp_transcendental : Transcendental ℚ (Real.exp (Real.exp 1))

$e^e$ is transcendental.

theorem pi_pow_exp_transcendental : Transcendental ℚ (Real.pi ^ Real.exp 1)

$\pi^e$ is transcendental.

theorem pi_pow_sqrt_two_transcendental : Transcendental ℚ (Real.pi ^ √2)

$\pi^{\sqrt{2}}$ is transcendental.

theorem pi_pow_pi_transcendental : Transcendental ℚ (Real.pi ^ Real.pi)

$\pi^{\pi}$ is transcendental.

theorem pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (Real.pi ^ Real.pi ^ Real.pi)

$\pi^{\pi^{\pi}}$ is transcendental.

theorem rlog_pi_transcendental : Transcendental ℚ (Real.log Real.pi)

$\log(\pi)$ is transcendental.

theorem rlog_rlog_two_transcendental : Transcendental ℚ (Real.log (Real.log 2))

$\log(\log(2))$ is transcendental.

theorem sin_exp_transcendental : Transcendental ℚ (Real.sin (Real.exp 1))

$\sin(e)$ is transcendental.

theorem exp_add_pi_or_exp_add_mul_transcendental : Transcendental ℚ (Real.pi + Real.exp 1) ∨ Transcendental ℚ (Real.pi * Real.exp 1)

At least one of $\pi + e$ and $\pi e$ is transcendental.