Log \(L_f\)

LemmaDisk analytic#

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

Lean

Formalized as Bf_is_analytic_on_disk.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 987

LeanBf_is_analytic_on_disk

Uses 2 · Used by 1

Proof usesBlaschke diff · C is analytic

Used byOne minus B

LemmaNever zero#

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

Lean

Formalized as Bf_never_zero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 996

LeanBf_never_zero

Uses 2 · Used by 2

Proof usesBlaschke nonzero · C never zero

Used byB zero · Log bound

LemmaB zero#

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

Lean

Formalized as Bf0_not_zero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1006

LeanBf0_not_zero

Uses 1 · Used by 1

Proof usesNever zero

Used byOne minus B

LemmaLf analytic#

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

Lean

Formalized as Lf_is_analytic.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1015

LeanLf_is_analytic

Uses 1 · Used by 1

Proof usesLogarithm of an analytic function

Used byApply BC

LemmaLf at zero#

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

Lean

Formalized as Lf_at_0_is_0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1024

LeanLf_at_0_is_0

Uses 1 · Used by 1

Proof usesLogarithm of an analytic function

Used byApply BC

LemmaReal part diff#

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

Lean

Formalized as re_Lf_as_diff_of_log_mods.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1034

Leanre_Lf_as_diff_of_log_mods

Uses 2 · Used by 1

Proof usesLogarithm of an analytic function · Real logarithm of modulus difference

Used byReal part bound

LemmaLog bound#

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

Lean

Formalized as log_Bf_le_log_B.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1044

Leanlog_Bf_le_log_B

Uses 1 · Used by 1

Proof usesLog monotone

Used byLog bound

LemmaLog bound#

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

Lean

Formalized as log_Bf_le_log_B2.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1053

Leanlog_Bf_le_log_B2

Uses 2 · Used by 1

Proof usesLog bound · Never zero

Used byLog bound

LemmaLog bound#

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

Lean

Formalized as log_Bf_le_log_B3.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1061

Leanlog_Bf_le_log_B3

Uses 2 · Used by 1

Proof usesLog bound · Disk bound

Used byReal part bound

LemmaLog nonnegative#

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

Lean

Formalized as log_Bf0_ge_0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1069

Leanlog_Bf0_ge_0

Uses 2 · Used by 1

Proof usesLog monotone · Modulus bound

Used byReal part bound

LemmaReal part bound#

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

Lean

Formalized as re_Lf_le_log_B.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1077

Leanre_Lf_le_log_B

Uses 3 · Used by 1

Proof usesReal part diff · Log bound · Log nonnegative

Used byApply BC

LemmaBC inequality#

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

Lean

Formalized as lem_BCII.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1086

Leanlem_BCII

Uses 1 · Used by 1

Proof usesBorel-Carathéodory II

Used byApply BC

LemmaApply BC#

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

Lean

Formalized as apply_BC_to_Lf.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1097

Leanapply_BC_to_Lf

Uses 4 · Used by 1

Proof usesBC inequality · Lf analytic · Lf at zero · Real part bound

Used byFinal bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.