Commit 790e2692 by Lawrence Paulson

### Hermite_Lindemann website

parent a9fb9e1730a7
 ... ... @@ -664,6 +664,39 @@ abstract = developed in the AFP entry on the transcendence of e.

[Hermite_Lindemann] title = The Hermite–Lindemann–Weierstraß Transcendence Theorem author = Manuel Eberl topic = Mathematics/Number theory date = 2021-03-03 notify = eberlm@in.tum.de abstract =

This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.

The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.

Like the previous formalisation in Coq by Bernard, I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.

This has a number of direct corollaries, e.g.:

• $e$ and $\pi$ are transcendental
• $e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$
• $\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$
[DFS_Framework] title = A Framework for Verifying Depth-First Search Algorithms author = Peter Lammich , René Neumann ... ...
 ... ... @@ -156,7 +156,7 @@ To this end, we mechanized several results on resultants, which also required us
Berlekamp_Zassenhaus, Sturm_Sequences
Used by: LLL_Basis_Reduction
Hermite_Lindemann, LLL_Basis_Reduction
... ...
 The Hermite–Lindemann–Weierstraß Transcendence Theorem - Archive of Formal Proofs

The Hermite–Lindemann–Weierstraß Transcendence Theorem

Title: The Hermite–Lindemann–Weierstraß Transcendence Theorem
Author: Manuel Eberl
Submission date: 2021-03-03
Abstract:

This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.

The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.

Like the previous formalisation in Coq by Bernard, I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.

This has a number of direct corollaries, e.g.:

• $e$ and $\pi$ are transcendental
• $e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$
• $\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$
BibTeX:
@article{Hermite_Lindemann-AFP,
author  = {Manuel Eberl},
title   = {The Hermite–Lindemann–Weierstraß Transcendence Theorem},
journal = {Archive of Formal Proofs},
month   = mar,
year    = 2021,
note    = {\url{https://isa-afp.org/entries/Hermite_Lindemann.html},
Formal proof development},
ISSN    = {2150-914x},
}
Depends on: Algebraic_Numbers, Pi_Transcendental, Power_Sum_Polynomials

\ No newline at end of file
 ... ... @@ -143,7 +143,9 @@ developed in the AFP entry on the transcendence of
Depends on: E_Transcendental, Symmetric_Polynomials
Used by: Hermite_Lindemann
... ...
 ... ... @@ -174,7 +174,9 @@ i>k.

Depends on: Polynomial_Factorization, Symmetric_Polynomials
Used by: Hermite_Lindemann
... ...
 ... ... @@ -95,6 +95,14 @@ of a scientific journal, is indexed by Mnacho Echenim
2021-03-03: The Hermite–Lindemann–Weierstraß Transcendence Theorem
Author: Manuel Eberl
... ...
 ... ... @@ -22,6 +22,39 @@ also known as von Neumann measurements, which are based on elements of spectral theory. We also formalized the CHSH inequality, an inequality involving expectations in a probability space that is violated by quantum measurements, thus proving that quantum mechanics cannot be modeled with an underlying local hidden-variable theory. The Hermite–Lindemann–Weierstraß Transcendence Theorem https://www.isa-afp.org/entries/Hermite_Lindemann.html https://www.isa-afp.org/entries/Hermite_Lindemann.html Manuel Eberl 03 Mar 2021 00:00:00 +0000 <p>This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.</p> <p>The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.</p> <p>Like the <a href="https://doi.org/10.1007/978-3-319-66107-0_5">previous formalisation in Coq by Bernard</a>, I proceeded by formalising <a href="https://doi.org/10.1017/CBO9780511565977">Baker's version of the theorem and proof</a> and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.</p> <p>This has a number of direct corollaries, e.g.:</p> <ul> <li>$e$ and $\pi$ are transcendental</li> <li>$e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$</li> <li>$\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$</li> </ul> Mereology ... ... @@ -562,30 +595,5 @@ href="https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html">Goe and <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>. From Abstract to Concrete Gödel's Incompleteness Theorems—Part II https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We validate an abstract formulation of G&ouml;del's Second Incompleteness Theorem from a <a href="https://www.isa-afp.org/entries/Goedel_Incompleteness.html">separate AFP entry</a> by instantiating it to the case of <i>finite consistent extensions of the Hereditarily Finite (HF) Set theory</i>, i.e., consistent FOL theories extending the HF Set theory with a finite set of axioms. The instantiation draws heavily on infrastructure previously developed by Larry Paulson in his <a href="https://www.isa-afp.org/entries/Incompleteness.html">direct formalisation of the concrete result</a>. It strengthens Paulson's formalization of G&ouml;del's Second from that entry by <i>not</i> assuming soundness, and in fact not relying on any notion of model or semantic interpretation. The strengthening was obtained by first replacing some of Paulson’s semantic arguments with proofs within his HF calculus, and then plugging in some of Paulson's (modified) lemmas to instantiate our soundness-free G&ouml;del's Second locale.
This diff is collapsed.
 ... ... @@ -771,6 +771,7 @@ Minkowskis_Theorem   E_Transcendental   Pi_Transcendental   Hermite_Lindemann   Liouville_Numbers   Prime_Harmonic_Series   Fermat3_4   ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!