Local finite-disk zero factorization

This module replaces a global Hadamard product by the divisor on one bounded complex disk. The resulting factorization and logarithmic-derivative formula are obtained from analyticity and isolated zeros; no explicit-formula equality is supplied as a hypothesis.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.localFiniteDisk_zeroFactorization (f : ℂ → ℂ) (hf : Differentiable ℂ f) {z₀ : ℂ} (hz₀ : f z₀ ≠ 0) (c : ℂ) {R : ℝ} (hR : 0 < R) : ∃ (D : ℂ → ℤ) (S : Finset ℂ) (g : ℂ → ℂ), (∀ (z : ℂ), 0 ≤ D z) ∧ ↑S = Function.support D ∧ (∀ (z : ℂ), z ∈ S ↔ z ∈ Metric.ball c R ∧ f z = 0) ∧ AnalyticOnNhd ℂ g (Metric.ball c R) ∧ (∀ z ∈ Metric.ball c R, g z ≠ 0) ∧ ∀ z ∈ Metric.ball c R, f z = (∏ ρ ∈ S, (z - ρ) ^ (D ρ).toNat) * g z

An entire nonzero complex function has, on every positive-radius disk, a finite zero divisor and a factorization by that divisor times a nonvanishing analytic function. Multiplicities are the integer values of D; they are nonnegative and S is exactly their finite support.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.localFiniteDisk_explicitFormula (f : ℂ → ℂ) (hf : Differentiable ℂ f) {z₀ : ℂ} (hz₀ : f z₀ ≠ 0) (c : ℂ) {R : ℝ} (hR : 0 < R) : ∃ (D : ℂ → ℤ) (S : Finset ℂ) (g : ℂ → ℂ), (∀ (z : ℂ), 0 ≤ D z) ∧ (∀ (z : ℂ), z ∈ S ↔ z ∈ Metric.ball c R ∧ f z = 0) ∧ AnalyticOnNhd ℂ g (Metric.ball c R) ∧ (∀ z ∈ Metric.ball c R, g z ≠ 0) ∧ ∀ s ∈ Metric.ball c R, f s ≠ 0 → logDeriv f s = ∑ ρ ∈ S, ↑(D ρ).toNat / (s - ρ) + logDeriv g s

The local finite-zero explicit formula attached to the factorization above. At every nonzero point of the disk, the logarithmic derivative is the finite sum of reciprocal zero distances (with multiplicity), plus the analytic nonvanishing remainder g'/g.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.norm_logDeriv_le_of_circleBounds (g : ℂ → ℂ) (s : ℂ) {r M m : ℝ} (hr : 0 < r) (hM : 0 ≤ M) (hm : 0 < m) (hg : DiffContOnCl ℂ g (Metric.ball s r)) (hcircle : ∀ z ∈ Metric.sphere s r, ‖g z‖ ≤ M) (hlower : m ≤ ‖g s‖) : ‖logDeriv g s‖ ≤ M / r / m

Cauchy control of the nonvanishing remainder from one circle value bound and one interior lower bound. This is the local replacement for the usual global Hadamard remainder estimate.

theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.symmetricCompletedLFunction_localFiniteDisk_explicitFormula {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (c : ℂ) {R : ℝ} (hR : 0 < R) : ∃ (D : ℂ → ℤ) (S : Finset ℂ) (g : ℂ → ℂ), (∀ (z : ℂ), 0 ≤ D z) ∧ (∀ (z : ℂ), z ∈ S ↔ z ∈ Metric.ball c R ∧ symmetricCompletedLFunction χ z = 0) ∧ AnalyticOnNhd ℂ g (Metric.ball c R) ∧ (∀ z ∈ Metric.ball c R, g z ≠ 0) ∧ ∀ s ∈ Metric.ball c R, symmetricCompletedLFunction χ s ≠ 0 → logDeriv (symmetricCompletedLFunction χ) s = ∑ ρ ∈ S, ↑(D ρ).toNat / (s - ρ) + logDeriv g s

Character-specific specialization for the actual symmetrically completed Dirichlet L-function. Nontriviality is proved at s = 2 from the standard nonvanishing theorem for L(s,χ) and the nonzero gamma factor.