OAI/NumberTheory/JointDickman/Analysis/AnalyticLogBranch.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Analytic logarithms on the zero-free contour domains

  1. theorem OAI.JointDickman.analyticAt_of_continuousAt_exp line 12
  2. theorem OAI.JointDickman.exists_analytic_log_on line 27
  3. theorem OAI.JointDickman.exists_normalized_analytic_log_on line 37
  4. theorem OAI.JointDickman.normalized_log_eq_principal_near line 48