Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.logDeriv_centeredHadamardOrbitBlock

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:81 to 95

Mathematical statement

Exact Lean statement

theorem logDeriv_centeredHadamardOrbitBlock (w₀ α w : ℂ)
    (hden : α ^ 2 - w₀ ^ 2 ≠ 0) (hw : w ^ 2 ≠ α ^ 2) :
    logDeriv (fun z : ℂ => centeredHadamardOrbitBlock w₀ α z) w =
      2 * w / (w ^ 2 - α ^ 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDeriv_centeredHadamardOrbitBlock (w₀ α w : ℂ)    (hden : α ^ 2 - w₀ ^ 2 ≠ 0) (hw : w ^ 2 ≠ α ^ 2) :    logDeriv (fun z : ℂ => centeredHadamardOrbitBlock w₀ α z) w =      2 * w / (w ^ 2 - α ^ 2) := by  unfold centeredHadamardOrbitBlock  rw [logDeriv_apply]  have hderiv :      deriv (fun z : ℂ => (α ^ 2 - z ^ 2) / (α ^ 2 - w₀ ^ 2)) w =        (-2 * w) / (α ^ 2 - w₀ ^ 2) := by    simp  rw [hderiv]  have hden' : w ^ 2 - α ^ 2 ≠ 0 := sub_ne_zero.mpr hw  have hden'' : α ^ 2 - w ^ 2 ≠ 0 := sub_ne_zero.mpr hw.symm  field_simp [hden, hden', hden'']  ring