Diff off pole to Log expansion

LemmaDiff off pole#

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

Lean

Formalized as zetadiffAtnot1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 802

LeanzetadiffAtnot1

Used by 1

Used byAnalytic off

LemmaAt to within#

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

Lean

Formalized as DiffAtWithinAt.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 812

LeanDiffAtWithinAt

Used by 1

Used byAt to on

LemmaWithin to on#

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

Lean

Formalized as DiffWithinAtallOn.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 822

LeanDiffWithinAtallOn

Used by 1

Used byAt to on

LemmaAt to on#

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

Lean

Formalized as DiffAtOn.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 832

LeanDiffAtOn

Uses 2 · Used by 1

Proof usesWithin to on · At to within

Used byAt gives anal

LemmaDiff to anal#

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

Lean

Formalized as DiffOnanalOnNhd.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 845

LeanDiffOnanalOnNhd

Used by 1

Used byAt gives anal

LemmaAt gives anal#

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

Lean

Formalized as DiffAtallanalOnNhd.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 855

LeanDiffAtallanalOnNhd

Uses 2 · Used by 1

Proof usesAt to on · Diff to anal

Used byAnalytic off

LemmaAnalytic off#

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

Lean

Formalized as zetaanalOnnot1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 867

LeanzetaanalOnnot1

Uses 2 · Used by 2

Proof usesDiff off pole · At gives anal

Used byAnalytic off · Disk analytic

LemmaDisk avoid#

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

Lean

Formalized as D1cinTt_pre.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 879

LeanD1cinTt_pre

Used by 1

Used byDisk subset

LemmaDisk subset#

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

Lean

Formalized as D1cinTt.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 890

LeanD1cinTt

Uses 1 · Used by 1

Proof usesDisk avoid

Used byDisk analytic

LemmaDisk analytic#

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

Lean

Formalized as zetaanalOnD1c_general.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 901

LeanzetaanalOnD1c_general

Uses 2 · Used by 4

Proof usesAnalytic off · Disk subset

Used byLog expansion · Finite set · Order nat · Order bound

LemmaZero free#

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

Lean

Formalized as sigmageq1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 913

Leansigmageq1

Used by 1

Used byPoint nonzero

LemmaPoint nonzero#

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

Lean

Formalized as zetacnot0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 922

Leanzetacnot0

Uses 1 · Used by 4

Proof usesZero free

Used byLog expansion · Finite set · Order nat · Order bound

LemmaNormalize analytic#

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

Lean

Formalized as fc_analytic_normalized.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 934

Leanfc_analytic_normalized

Used by 1

Used byFinal bound

LemmaLog derivative#

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

Lean

Formalized as fc_log_deriv.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 944

Leanfc_log_deriv

Used by 1

Used byFinal bound

LemmaShift bound#

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

Lean

Formalized as fc_bound.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 953

Leanfc_bound

Used by 2

Used byFinal bound · Order bound

LemmaZero shift#

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

Lean

Formalized as fc_zeros.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 962

Leanfc_zeros

Used by 3

Used byFinal bound · Finite set · Order bound

LemmaOrder shift#

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

Lean

Formalized as fc_m_order.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 972

Leanfc_m_order

Used by 3

Used byFinal bound · Order nat · Order bound

LemmaDisk minus K#

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

Lean

Formalized as DminusK.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 982

LeanDminusK

Used by 1

Used byLog expansion

LemmaFinal bound#

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

Lean

Formalized as final_ineq2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 993

Leanfinal_ineq2

Uses 6 · Used by 1

Proof usesFinal bound · Normalize analytic · Shift bound · Log derivative · Zero shift · Order shift

Used byLog expansion

LemmaLog expansion#

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

Lean

Formalized as log_Deriv_Expansion_Zeta.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT3_RiemannZeta.tex, line 1004

Leanlog_Deriv_Expansion_Zeta

Uses 5 · Used by 1

Proof usesFinal bound · Disk analytic · Point nonzero · Final bound · Disk minus K

Used byExpand bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.