Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.logDeriv_finiteCenteredHadamardOrbitProduct

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:123 to 136

Source documentation

Finite Hadamard-orbit calculation before any infinite product limit is needed.

Exact Lean statement

theorem logDeriv_finiteCenteredHadamardOrbitProduct (w₀ w : ℂ) (A : Finset ℂ)
    (hden : ∀ α ∈ A, α ^ 2 - w₀ ^ 2 ≠ 0)
    (hw : ∀ α ∈ A, w ^ 2 ≠ α ^ 2) :
    logDeriv (fun z : ℂ => finiteCenteredHadamardOrbitProduct w₀ A z) w =
      finiteCenteredHadamardOrbitLogDerivSum A w

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDeriv_finiteCenteredHadamardOrbitProduct (w₀ w : ℂ) (A : Finset ℂ)    (hden : ∀ α ∈ A, α ^ 2 - w₀ ^ 2 ≠ 0)    (hw : ∀ α ∈ A, w ^ 2 ≠ α ^ 2) :    logDeriv (fun z : ℂ => finiteCenteredHadamardOrbitProduct w₀ A z) w =      finiteCenteredHadamardOrbitLogDerivSum A w := by  classical  unfold finiteCenteredHadamardOrbitProduct finiteCenteredHadamardOrbitLogDerivSum  rw [logDeriv_prod]  · exact Finset.sum_congr rfl fun α hα =>      logDeriv_centeredHadamardOrbitBlock w₀ α w (hden α hα) (hw α hα)  · exact fun α hα => centeredHadamardOrbitBlock_ne_zero (hden α hα) (hw α hα)  · intro α hα    unfold centeredHadamardOrbitBlock    fun_prop