Sum multiple to Final bound

LemmaSum multiple#

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

Lean

Formalized as logDeriv_prod_is_sum_mul.

Sources
LeanlogDeriv_prod_is_sum_mul
Uses 2 · Used by 1
Proof usesProduct sum · Power multiple
Used byStep two

LemmaStep two#

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

Lean

Formalized as Lf_deriv_step2.

Sources
LeanLf_deriv_step2
Uses 2 · Used by 1
Proof usesStep one · Sum multiple
Used byStep three

LemmaDifference form#

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

Lean

Formalized as logDeriv_Blaschke_is_diff.

Sources
LeanlogDeriv_Blaschke_is_diff
Uses 3 · Used by 1
Proof usesQuotient rule · Difference nonzero · Numerator nonzero
Used byDiff fraction

LemmaLinear rule#

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

Lean

Formalized as logDeriv_linear.

Sources
LeanlogDeriv_linear
Used by 2
Used byDenominator rule · Numerator rule

LemmaDenominator rule#

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

Lean

Formalized as logDeriv_denominator.

Sources
LeanlogDeriv_denominator
Uses 1 · Used by 1
Proof usesLinear rule
Used byDiff fraction

LemmaNumerator rule#

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

Lean

Formalized as logDeriv_numerator_pre.

Sources
LeanlogDeriv_numerator_pre
Uses 1 · Used by 1
Proof usesLinear rule
Used byNumerator form

LemmaRearranged form#

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

Lean

Formalized as logDeriv_numerator_rearranged.

Sources
LeanlogDeriv_numerator_rearranged
Used by 1
Used byNumerator form

LemmaNumerator form#

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

Lean

Formalized as logDeriv_numerator.

Sources
LeanlogDeriv_numerator
Uses 2 · Used by 1
Proof usesNumerator rule · Rearranged form
Used byDiff fraction

LemmaDiff fraction#

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

Lean

Formalized as logDeriv_Blaschke_is_diff_frac.

Sources
LeanlogDeriv_Blaschke_is_diff_frac
Uses 5 · Used by 1
Proof usesDifference form · Numerator form · Denominator rule · Numerator nonzero · Difference nonzero
Used byStep three

LemmaStep three#

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

Lean

Formalized as Lf_deriv_step3.

Sources
LeanLf_deriv_step3
Uses 2 · Used by 1
Proof usesStep two · Diff fraction
Used byFinal formula

LemmaSum difference#

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

Lean

Formalized as sum_of_diff.

Sources
Leansum_of_diff
Used by 1
Used bySum rearranged

LemmaSum rearranged#

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

Lean

Formalized as sum_rearranged.

Sources
Leansum_rearranged
Uses 2 · Used by 1
Proof usesSum difference · Finite zeros
Used byFinal formula

LemmaFinal formula#

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

Lean

Formalized as Lf_deriv_final_formula.

Sources
LeanLf_deriv_final_formula
Uses 2 · Used by 1
Proof usesStep three · Sum rearranged
Used byRearranged deriv

LemmaRearranged deriv#

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

Lean

Formalized as rearrange_Lf_deriv.

Sources
Leanrearrange_Lf_deriv
Uses 1 · Used by 1
Proof usesFinal formula
Used bySetup inequality

LemmaTriangle sum#

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

Lean

Formalized as triangle_ineq_sum.

Sources
Leantriangle_ineq_sum
Used by 1
Used bySetup inequality

LemmaSetup inequality#

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

Lean

Formalized as target_inequality_setup.

Sources
Leantarget_inequality_setup
Uses 2 · Used by 1
Proof usesTriangle sum · Rearranged deriv
Used byFinal bound

LemmaStep two#

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

Lean

Formalized as lem_sum_bound_step2.

Sources
Leanlem_sum_bound_step2
Uses 1 · Used by 1
Proof usesFinite zeros
Used byFinal sum

LemmaFinal sum#

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

Lean

Formalized as final_sum_bound.

Sources
Leanfinal_sum_bound
Uses 2 · Used by 1
Proof usesStep two · Multiplicity bound
Used byFinal bound

LemmaFinal bound#

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

Lean

Formalized as final_inequality.

Sources
Leanfinal_inequality
Uses 3 · Used by 2
Proof usesSetup inequality · Final sum · Apply BC
Used byFinal bound · Log expansion

LemmaFinal bound#

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

Lean

Formalized as final_ineq1.

Sources
Leanfinal_ineq1
Uses 1 · Used by 1
Proof usesFinal bound
Used byFinal bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.