Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

2 results

Clear filters
Project-declaredLean 4.32.0

Log Deriv Residue

logDerivResidue'

Plain-language statement

Suppose ff is holomorphic and nonzero on a punctured neighborhood of pp, and f(s)=Asp+O(1)f(s)=\frac{A}{s-p}+O(1) there with A0A\ne0. Then the logarithmic derivative has principal part 1/(sp)-1/(s-p): f(s)f(s)+1sp=O(1)\frac{f'(s)}{f(s)}+\frac{1}{s-p}=O(1) as sps\to p. In particular, the residue of f/ff'/f at this simple pole is 1-1.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Residue Of Tends To

ResidueOfTendsTo

Plain-language statement

Let ff be holomorphic on a punctured neighborhood of pp. If (sp)f(s)A(sp),(s-p)f(s)\longrightarrow A\qquad(s\to p), then ff differs from its principal part A/(sp)A/(s-p) by a bounded function on some punctured neighborhood of pp. In asymptotic notation, f(s)=Asp+O(1).f(s)=\frac{A}{s-p}+O(1).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record