Complex logarithm

LemmaLogarithmic derivative is analytic#

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

Lean

Formalized as log_deriv_is_analytic.

Sources
Leanlog_deriv_is_analytic
Used by 1
Used byAntiderivative of logarithmic derivative

LemmaAntiderivative of logarithmic derivative#

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

Lean

Formalized as I_is_antiderivative.

Sources
LeanI_is_antiderivative
Uses 2 · Used by 4
Proof usesDifferentiability of \(I_f(z)\) · Logarithmic derivative is analytic
Used byExponential of \(I_f\) at zero · Derivative of \(\exp(J(z))\) · Logarithmic derivative identity · Logarithm of an analytic function

DefinitionAuxiliary function#

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

Lean

Formalized as H_auxiliary.

Sources
LeanH_auxiliary
Used by 3
Used byExistence of analytic logarithm · Value of \(H\) at zero · Derivative of \(H(z)\)

LemmaExponential of \(I_f\) at zero#

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

Lean

Formalized as exp_I_at_zero.

Sources
Leanexp_I_at_zero
Uses 1 · Used by 1
Proof usesAntiderivative of logarithmic derivative
Used byValue of \(H\) at zero

LemmaValue of \(H\) at zero#

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

Lean

Formalized as H_at_zero.

Sources
LeanH_at_zero
Uses 2 · Used by 1
Proof usesAuxiliary function · Exponential of \(I_f\) at zero
Used by\(H=1\)

LemmaLogarithmic derivative identity#

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

Lean

Formalized as log_deriv_id.

Sources
Leanlog_deriv_id
Uses 1 · Used by 1
Proof usesAntiderivative of logarithmic derivative
Used byLogarithmic derivative identity

LemmaLogarithmic derivative identity#

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

Lean

Formalized as log_deriv_identity.

Sources
Leanlog_deriv_identity
Uses 1 · Used by 1
Proof usesLogarithmic derivative identity
Used byDerivative of \(H(z)\) is 0

LemmaDerivative of \(H(z)\)#

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

Lean

Formalized as H_derivative_quotient_rule.

Sources
LeanH_derivative_quotient_rule
Uses 1 · Used by 1
Proof usesAuxiliary function
Used byDerivative of \(H(z)\)

LemmaDerivative of \(\exp(J(z))\)#

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

Lean

Formalized as exp_I_derivative_chain_rule.

Sources
Leanexp_I_derivative_chain_rule
Uses 1 · Used by 1
Proof usesAntiderivative of logarithmic derivative
Used byDerivative of \(H(z)\)

LemmaDerivative of \(H(z)\)#

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

Lean

Formalized as H_derivative_calc.

Sources
LeanH_derivative_calc
Uses 2 · Used by 1
Proof usesDerivative of \(\exp(J(z))\) · Derivative of \(H(z)\)
Used byDerivative of \(H(z)\) is 0

LemmaDerivative of \(H(z)\) is 0#

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

Lean

Formalized as H_derivative_is_zero.

Sources
LeanH_derivative_is_zero
Uses 2 · Used by 1
Proof usesDerivative of \(H(z)\) · Logarithmic derivative identity
Used by\(H(z)\) is constant

Lemma\(H(z)\) is constant#

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

Lean

Formalized as H_is_constant.

Sources
LeanH_is_constant
Uses 1 · Used by 1
Proof usesDerivative of \(H(z)\) is 0
Used by\(H=1\)

Lemma\(H=1\)#

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

Lean

Formalized as H_is_one.

Sources
LeanH_is_one
Uses 2 · Used by 1
Proof usesValue of \(H\) at zero · \(H(z)\) is constant
Used byExistence of analytic logarithm

LemmaExistence of analytic logarithm#

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

Lean

Formalized as analytic_log_exists.

Sources
Leananalytic_log_exists
Uses 2 · Used by 1
Proof usesAuxiliary function · \(H=1\)
Used byModulus of \(B(z)\) in product form

LemmaModulus of \(\exp(J(z))\)#

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

Lean

Formalized as modulus_of_exp_I.

Sources
Leanmodulus_of_exp_I
Used by 1
Used byModulus of \(\exp(J(z))\)

LemmaModulus of \(B(z)\) in product form#

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

Lean

Formalized as modulus_of_B_product_form.

Sources
Leanmodulus_of_B_product_form
Uses 1 · Used by 1
Proof usesExistence of analytic logarithm
Used byModulus of \(\exp(J(z))\)

LemmaModulus of \(\exp(J(z))\)#

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

Lean

Formalized as modulus_of_exp_log.

Sources
Leanmodulus_of_exp_log
Uses 2 · Used by 1
Proof usesModulus of \(B(z)\) in product form · Modulus of \(\exp(J(z))\)
Used byLogarithm of modulus as sum

LemmaLogarithm of modulus as sum#

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

Lean

Formalized as log_modulus_as_sum.

Sources
Leanlog_modulus_as_sum
Uses 1 · Used by 1
Proof usesModulus of \(\exp(J(z))\)
Used byReal logarithm of modulus difference

LemmaReal logarithm of modulus difference#

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

Lean

Formalized as real_log_of_modulus_difference.

Sources
Leanreal_log_of_modulus_difference
Uses 1 · Used by 2
Proof usesLogarithm of modulus as sum
Used byLogarithm of an analytic function · Real part diff

LemmaLogarithm of an analytic function#

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

Lean

Formalized as log_of_analytic.

Sources
Leanlog_of_analytic
Uses 2 · Used by 3
Proof usesAntiderivative of logarithmic derivative · Real logarithm of modulus difference
Used byLf at zero · Lf analytic · Real part diff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.