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 Of Analytic Function

LogOfAnalyticFunction

Plain-language statement

Let 0<r<R0<r<R, and let BB be analytic and nonvanishing on the closed disc zR|z|\le R. Then there is an analytic function JBJ_B on z<R|z|<R with JB(0)=0J_B(0)=0, JB(z)=B(z)B(z)(zr),J_B'(z)=\frac{B'(z)}{B(z)}\quad(|z|\le r), and ReJB(z)=logB(z)logB(0)(z<R).\operatorname{Re}J_B(z)=\log|B(z)|-\log|B(0)|\quad(|z|<R). Thus JBJ_B is a normalized analytic logarithm of B/B(0)B/B(0).

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record