OAI/NumberTheory/Ostmann/ZeroDensity/AnalyticLogBall.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A normalized logarithm on a zero-free disk

This is the local analytic bridge used to bound logarithmic derivatives on zero-free disks. It is obtained by integrating the actual logarithmic derivative.

  1. theorem OAI.Ostmann.exists_normalized_log_on_ball line 18
  2. theorem OAI.Ostmann.normalized_log_re line 43