Order is integer to C nonzero on K

LemmaOrder is integer#

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

Lean

Formalized as lem_m_rho_is_nat.

Sources
Leanlem_m_rho_is_nat
Uses 2 · Used by 4
Proof usesZero set · Not zero
Used byOrder at least one · Modulus bound · Scaled real · Order nat

LemmaOrder at least one#

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

Lean

Formalized as lem_m_rho_ge_1.

Sources
Leanlem_m_rho_ge_1
Uses 2 · Used by 4
Proof usesOrder is integer · Zero value
Used byC analytic off K · h ratio analytic · Modulus bound · Multiplicity one

LemmaAnalytic division#

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

Lean

Formalized as lem_analDiv.

Sources
Leanlem_analDiv
Used by 1
Used byRatio analytic

LemmaDenominator analytic#

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

Lean

Formalized as lem_denomAnalAt.

Sources
Leanlem_denomAnalAt
Used by 1
Used byRatio analytic

LemmaRatio analytic#

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

Lean

Formalized as lem_ratioAnalAt.

Sources
Leanlem_ratioAnalAt
Uses 2 · Used by 2
Proof usesAnalytic division · Denominator analytic
Used byC analytic off K · h ratio analytic

LemmaZero factorization#

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

Lean

Formalized as lem_analytic_zero_factor.

Sources
Leanlem_analytic_zero_factor
Used by 3
Used byC near zero · C nonzero on K · h ratio analytic

LemmaC analytic off K#

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

Lean

Formalized as lem_Cf_analytic_off_K.

Sources
Leanlem_Cf_analytic_off_K
Uses 3 · Used by 1
Proof usesRatio analytic · Finite zeros · Order at least one
Used byC is analytic

LemmaC at zero#

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

Lean

Formalized as lem_Cf_at_sigma_onK.

Sources
Leanlem_Cf_at_sigma_onK
Used by 1
Used byC local form

LemmaZeros isolated#

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

Lean

Formalized as lem_K_isolated.

Sources
Leanlem_K_isolated
Used by 1
Used byC near zero

LemmaC near zero#

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

Lean

Formalized as lem_Cf_at_sigma_offK0.

Sources
Leanlem_Cf_at_sigma_offK0
Uses 3 · Used by 1
Proof usesFinite zeros · Zeros isolated · Zero factorization
Used byC off K

LemmaProduct split#

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

Lean

Formalized as lem_prod_no_sigma1.

Sources
Leanlem_prod_no_sigma1
Uses 1 · Used by 1
Proof usesFinite zeros
Used byProduct quotient

LemmaProduct quotient#

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

Lean

Formalized as lem_prod_no_sigma2.

Sources
Leanlem_prod_no_sigma2
Uses 1 · Used by 1
Proof usesProduct split
Used byC off K

LemmaC off K#

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

Lean

Formalized as lem_Cf_at_sigma_offK.

Sources
Leanlem_Cf_at_sigma_offK
Uses 2 · Used by 1
Proof usesC near zero · Product quotient
Used byC local form

LemmaC local form#

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

Lean

Formalized as lem_Cf_at_sigma.

Sources
Leanlem_Cf_at_sigma
Uses 2 · Used by 1
Proof usesC off K · C at zero
Used byC analytic at K

Lemmah ratio analytic#

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

Lean

Formalized as lem_h_ratio_anal.

Sources
Leanlem_h_ratio_anal
Uses 4 · Used by 1
Proof usesRatio analytic · Zero factorization · Finite zeros · Order at least one
Used byC analytic at K

LemmaC analytic at K#

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

Lean

Formalized as lem_Cf_analytic_at_K.

Sources
Leanlem_Cf_analytic_at_K
Uses 2 · Used by 1
Proof usesC local form · h ratio analytic
Used byC is analytic

LemmaC is analytic#

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

Lean

Formalized as lem_Cf_is_analytic.

Sources
Leanlem_Cf_is_analytic
Uses 2 · Used by 2
Proof usesC analytic off K · C analytic at K
Used byB analytic · Disk analytic

Lemmaf nonzero off K#

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

Lean

Formalized as lem_f_nonzero_off_K.

Sources
Leanlem_f_nonzero_off_K
Uses 1 · Used by 1
Proof usesZero set
Used byC nonzero off K

LemmaC nonzero off K#

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

Lean

Formalized as lem_Cf_nonzero_off_K.

Sources
Leanlem_Cf_nonzero_off_K
Uses 1 · Used by 1
Proof usesf nonzero off K
Used byC never zero

LemmaC nonzero on K#

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

Lean

Formalized as lem_Cf_nonzero_on_K.

Sources
Leanlem_Cf_nonzero_on_K
Uses 1 · Used by 1
Proof usesZero factorization
Used byC never zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.