Abs neg to Combine bounds

LemmaAbs neg#

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

Lean

Formalized as lem_mod_neg.

Sources

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

Leanlem_mod_neg

Used by 1

Used byAbs ratio

LemmaAbs ratio#

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

Lean

Formalized as lem_mod_div_and_neg.

Sources

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

Leanlem_mod_div_and_neg

Uses 3 · Used by 1

Proof usesAbs division · Nonzero rho · Abs neg

Used byB zero form

LemmaB zero form#

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

Lean

Formalized as lem_mod_Bf_at_0_eval.

Sources

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

Leanlem_mod_Bf_at_0_eval

Uses 3 · Used by 2

Proof usesAbs ratio · Nonzero rho · B at zero

Used byCombine bounds · B zero form

LemmaAbs positive#

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

Lean

Formalized as lem_mod_of_pos_real.

Sources

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

Leanlem_mod_of_pos_real

Used by 1

Used byB zero form

LemmaB zero form#

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

Lean

Formalized as lem_mod_Bf_at_0_as_ratio.

Sources

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

Leanlem_mod_Bf_at_0_as_ratio

Uses 2

Proof usesAbs positive · B zero form

LemmaProd inequality#

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

Lean

Formalized as lem_prod_ineq.

Sources

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

Leanlem_prod_ineq

Used by 1

Used byProduct power

LemmaPower bound#

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

Lean

Formalized as lem_power_ineq.

Sources

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

Leanlem_power_ineq

Used by 2

Used byPower one · Product power

LemmaPower one#

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

Lean

Formalized as lem_power_ineq_1.

Sources

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

Leanlem_power_ineq_1

Uses 1

Proof usesPower bound

LemmaProduct power#

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

Lean

Formalized as lem_prod_power_ineq.

Sources

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

Leanlem_prod_power_ineq

Uses 2 · Used by 1

Proof usesProd inequality · Power bound

Used byPower bound

LemmaProduct one#

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

Lean

Formalized as lem_prod_1.

Sources

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

Leanlem_prod_1

Used by 1

Used byPower bound

LemmaPower bound#

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

Lean

Formalized as lem_prod_power_ineq1.

Sources

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

Leanlem_prod_power_ineq1

Uses 2 · Used by 1

Proof usesProduct power · Product one

Used byModulus bound

LemmaModulus bound#

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

Lean

Formalized as lem_mod_lower_bound_1.

Sources

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

Leanlem_mod_lower_bound_1

Uses 4 · Used by 1

Proof usesOrder at least one · Order is integer · Finite zeros · Power bound

Used byLog nonnegative

LemmaB analytic#

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

Lean

Formalized as lem_Bf_is_analytic.

Sources

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

Leanlem_Bf_is_analytic

Uses 1 · Used by 1

Proof usesC is analytic

Used byDisk bound

LemmaBoundary mod#

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

Lean

Formalized as lem_mod_Bf_eq_mod_f_on_boundary.

Sources

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

Leanlem_mod_Bf_eq_mod_f_on_boundary

Used by 1

Used byBoundary bound

LemmaBoundary bound#

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

Lean

Formalized as lem_Bf_bounded_on_boundary.

Sources

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

Leanlem_Bf_bounded_on_boundary

Uses 1 · Used by 1

Proof usesBoundary mod

Used byDisk bound

LemmaMax modulus#

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

Lean

Formalized as lem_max_mod_principle_for_Bf.

Sources

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

Leanlem_max_mod_principle_for_Bf

Uses 1 · Used by 1

Proof usesMax principle

Used byDisk bound

LemmaDisk bound#

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

Lean

Formalized as lem_Bf_bounded_in_disk_from_boundary.

Sources

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

Leanlem_Bf_bounded_in_disk_from_boundary

Uses 2 · Used by 1

Proof usesB analytic · Max modulus

Used byDisk bound

LemmaDisk bound#

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

Lean

Formalized as lem_Bf_bounded_in_disk_from_f.

Sources

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

Leanlem_Bf_bounded_in_disk_from_f

Uses 2 · Used by 2

Proof usesBoundary bound · Disk bound

Used byZero bound · Log bound

LemmaZero bound#

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

Lean

Formalized as lem_Bf_at_0_le_M.

Sources

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

Leanlem_Bf_at_0_le_M

Uses 1 · Used by 1

Proof usesDisk bound

Used byJensen form

LemmaCombine bounds#

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

Lean

Formalized as lem_combine_bounds_on_Bf0.

Sources

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

Leanlem_combine_bounds_on_Bf0

Uses 1 · Used by 1

Proof usesB zero form

Used byJensen form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.