Holomorphic logarithms of the character-specific local factor

The logarithm in this file is not an additional hypothesis. It is constructed from a primitive of g'/g on the (convex, hence simply connected) disk and is normalised at the centre. The exponential identity is then proved by showing that exp h / g has zero derivative on the disk.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.exists_holomorphicLog_on_ball (g : ℂ → ℂ) (c : ℂ) {R : ℝ} (hR : 0 < R) (hg : DifferentiableOn ℂ g (Metric.ball c R)) (hg0 : ∀ z ∈ Metric.ball c R, g z ≠ 0) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h (Metric.ball c R) ∧ Set.EqOn (fun (z : ℂ) => Complex.exp (h z)) g (Metric.ball c R)

A nonvanishing holomorphic function on a disk has a holomorphic logarithm on that disk. This is the disk-specialised, differentiable version of the continuous lifting theorem for the exponential covering map.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.exists_holomorphicLog {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} {c : ℂ} {R : ℝ} (d : CharacterLocalDiskData χ c R) (hR : 0 < R) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h (Metric.ball c R) ∧ Set.EqOn (fun (z : ℂ) => Complex.exp (h z)) d.g (Metric.ball c R)

The local factor selected by the actual character finite-disk factorisation has a genuinely constructed holomorphic logarithm.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.CharacterLocalDiskData.exists_holomorphicLog_deriv_eq_logDeriv {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} {c : ℂ} {R : ℝ} (d : CharacterLocalDiskData χ c R) (hR : 0 < R) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h (Metric.ball c R) ∧ Set.EqOn (fun (z : ℂ) => Complex.exp (h z)) d.g (Metric.ball c R) ∧ ∀ z ∈ Metric.ball c R, deriv h z = logDeriv d.g z

For the logarithm just constructed, its derivative is literally the character-specific finite-disk remainder g'/g at every point of the disk.