Log growth to Trig identity

LemmaLog growth#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 4. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_2logOlog.

Sources
Leanlem_2logOlog
Used by 1
Used byLog compare

LemmaSquare log#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 12. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_logt22logt.

Sources
Leanlem_logt22logt
Used by 1
Used byLog compare

LemmaDouble log#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 20. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_log2tlogt2.

Sources
Leanlem_log2tlogt2
Used by 1
Used byLog compare

LemmaLog compare#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 28. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_log22log.

Sources
Leanlem_log22log
Uses 2 · Used by 1
Proof usesSquare log · Double log
Used byLog compare

LemmaExp rule#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 37. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_exprule.

Sources
Leanlem_exprule
Used by 1
Used byExponent split

LemmaReal scale#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 45. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_realbw.

Sources
Leanlem_realbw
Used by 1
Used byReal factor

LemmaReal series#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 52. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_sumReal.

Sources
Leanlem_sumReal
Used by 1
Used byReal sum

LemmaEuler's formula#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 61. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_Euler.

Sources
Leanlem_Euler
Used by 1
Used byReal cosine

LemmaReal cosine#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 68. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_Reecos.

Sources
Leanlem_Reecos
Uses 1 · Used by 1
Proof usesEuler's formula
Used byReal cosine

LemmaLog inverse#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 76. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_explog.

Sources
Leanlem_explog
Used by 1
Used byExp form

LemmaCos even#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 83. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_coseven.

Sources
Leanlem_coseven
Used by 1
Used byCos even

LemmaCos even#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 91. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_coseveny.

Sources
Leanlem_coseveny
Uses 1 · Used by 1
Proof usesCos even
Used byReal cosine

LemmaExp form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 101. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_niyelog.

Sources
Leanlem_niyelog
Uses 1 · Used by 1
Proof usesLog inverse
Used byReal cosine

LemmaReal cosine#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 109. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_eacosalog.

Sources
Leanlem_eacosalog
Uses 1 · Used by 1
Proof usesReal cosine
Used byReal cosine

LemmaReal cosine#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 117. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_eacosalog2.

Sources
Leanlem_eacosalog2
Uses 2 · Used by 1
Proof usesExp form · Real cosine
Used byReal cosine

LemmaReal cosine#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 125. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_eacosalog3.

Sources
Leanlem_eacosalog3
Uses 2 · Used by 1
Proof usesCos even · Real cosine
Used byCos form

LemmaDouble angle#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 135. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_cos2t.

Sources
Leanlem_cos2t
Used by 1
Used byCos square

LemmaCos square#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 142. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_cos2t2.

Sources
Leanlem_cos2t2
Uses 1 · Used by 1
Proof usesDouble angle
Used byTrig identity

LemmaSquare expand#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 150. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_cosSquare.

Sources
Leanlem_cosSquare
Used by 1
Used byTrig identity

LemmaTrig identity#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 158. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_cos2cos341.

Sources
Leanlem_cos2cos341
Uses 2 · Used by 1
Proof usesCos square · Square expand
Used byTrig positive

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.