Transcendental Numbers

This project is to prove several theorems in transcendental number theory:

1. Countability argument: abstract existence of transcendental number;
2. Liouvielle theorem and hence is transcendental;
3. is transcendental;
4. is transcendental.

Part 1, countability argument

The main theorem is in algebraic_countable_over_Z.lean

theorem transcendental_number_exists : ∃ x : real, ¬ (is_algebraic ℤ x)

The other version is in algebraic_countable_over_Q.lean

theorem transcendental_number_exists : ∃ x : real, ¬ (is_algebraic ℚ x)

Part 2, Liouville theorem and an explicit Liouville number

Definition of the explicit Liouville number is in liouville_theorem.lean

def α := ∑' n, ten_pow_n_fact_inverse n

The main theorem is in liouville_theorem.lean:

theorem liouville_numbers_transcendental : ∀ x : real, liouville_number x -> ¬(is_algebraic ℤ x)

theorem transcendental_α : transcendental α := liouville_numbers_transcendental α liouville_α

Part 3, the transcendence of e

We defined e in e_transcendental.lean as :

def e : ℝ := real.exp 1

The main theorem is at e_transcendental.lean:

theorem e_transcendental : ¬ is_algebraic ℤ e :=

Almost immediately, we can prove

theorem e_irrational : irrational e

theorem e_pow_transcendental (n : ℕ) (hn : n ≥ 1) : transcendental (e^n)
theorem e_pow_n_irrational (n : ℕ) (hn : n ≥ 1) : irrational (e ^ n)

Please see this for an explanation of the proof of transcendence of $e$ with reference to Lean code.

I haven't finished documentation (not even close), but you can click around the proves I documented so far at e_trans_helpers2.lean ande_transcendental.lean.