Log Derivative

LemmaDisk inclusion#

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

Lean

Formalized as DRinD1.

Sources
LeanDRinD1
Used by 1
Used byIdentity theorem R

DefinitionZero set#

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

Lean

Formalized as zerosetKfR.

Sources
LeanzerosetKfR
Used by 9
Used byf nonzero off K · Order is integer · Zero value · Disk bound · Disk bound · Zero containment · Zero in disk · Outside zeros · Difference nonzero

LemmaZero containment#

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

Lean

Formalized as lemKinDR.

Sources
LeanlemKinDR
Uses 1 · Used by 1
Proof usesZero set
Used byZeros accumulate

LemmaZero in disk#

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

Lean

Formalized as lemKRinK1.

Sources
LeanlemKRinK1
Uses 1 · Used by 1
Proof usesZero set
Used byIdentity on K

LemmaAccumulation point#

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

Lean

Formalized as lem_bolzano_weierstrass.

Sources
Leanlem_bolzano_weierstrass
Used by 1
Used byZeros accumulate

LemmaZeros accumulate#

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

Lean

Formalized as lem_zeros_have_limit_point.

Sources
Leanlem_zeros_have_limit_point
Uses 3 · Used by 1
Proof usesCompactness · Zero containment · Accumulation point
Used byInfinite zeros imply

LemmaIdentity theorem#

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

Lean

Formalized as lem_identity_theorem.

Sources
Leanlem_identity_theorem
Used by 1
Used byIdentity theorem R

LemmaIdentity theorem R#

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

Lean

Formalized as lem_identity_theoremR.

Sources
Leanlem_identity_theoremR
Uses 2 · Used by 1
Proof usesIdentity theorem · Disk inclusion
Used byIdentity on K

LemmaIdentity on K#

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

Lean

Formalized as lem_identity_theoremKR.

Sources
Leanlem_identity_theoremKR
Uses 2 · Used by 1
Proof usesIdentity theorem R · Zero in disk
Used byInfinite zeros imply

LemmaInfinite zeros imply#

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

Lean

Formalized as lem_identity_infiniteKR.

Sources
Leanlem_identity_infiniteKR
Uses 2 · Used by 1
Proof usesIdentity on K · Zeros accumulate
Used byFinite zeros

LemmaFinite zeros#

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

Lean

Formalized as lem_Contra_finiteKR.

Sources
Leanlem_Contra_finiteKR
Uses 1 · Used by 17
Proof usesInfinite zeros imply
Used byC analytic off K · C near zero · h ratio analytic · Product split · B division · B product pow · Blaschke diff · Blaschke nonzero · Modulus bound · Zeros bound · Multiplicity one · Product nonzero · Product sum · Step two · Sum rearranged · Finite set · Finite set

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.