Jensen form to Zeros bound

LemmaJensen form#

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

Lean

Formalized as lem_jensen_inequality_form.

Sources
Leanlem_jensen_inequality_form
Uses 2 · Used by 1
Proof usesZero bound · Combine bounds
Used byJensen log

LemmaLog monotone#

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

Lean

Formalized as lem_log_mono_inc.

Sources
Leanlem_log_mono_inc
Used by 3
Used byJensen log · Log bound · Log nonnegative

LemmaJensen log#

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

Lean

Formalized as lem_jensen_log_form.

Sources
Leanlem_jensen_log_form
Uses 2 · Used by 1
Proof usesLog monotone · Jensen form
Used byMultiplicity bound

LemmaThree exceeds e#

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

Lean

Formalized as lem_three_gt_e.

Sources
Leanlem_three_gt_e
Used by 6
Used byCombined bound · Inequality · Delta range · Log bound · Order sum · Bound on \(\zeta'/\zeta\)

LemmaMultiplicity bound#

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

Lean

Formalized as lem_sum_m_rho_bound.

Sources
Leanlem_sum_m_rho_bound
Uses 1 · Used by 3
Proof usesJensen log
Used byOnes bound · Final sum · Order bound

LemmaSum inequality#

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

Lean

Formalized as lem_sum_ineq.

Sources
Leanlem_sum_ineq
Used by 1
Used byMultiplicity one

LemmaMultiplicity one#

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

Lean

Formalized as lem_sum_m_rho_1.

Sources
Leanlem_sum_m_rho_1
Uses 3 · Used by 1
Proof usesFinite zeros · Order at least one · Sum inequality
Used byOnes bound

LemmaOnes bound#

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

Lean

Formalized as lem_sum_1_bound.

Sources
Leanlem_sum_1_bound
Uses 2 · Used by 1
Proof usesMultiplicity one · Multiplicity bound
Used byZeros bound

LemmaCount identity#

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

Lean

Formalized as lem_sum_1_is_card.

Sources
Leanlem_sum_1_is_card
Used by 1
Used byZeros bound

LemmaZeros bound#

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

Lean

Formalized as lem_num_zeros_bound.

Sources
Leanlem_num_zeros_bound
Uses 3
Proof usesFinite zeros · Ones bound · Count identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.