Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.hadamardGenusOneFactor_pair_cancellation

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:24 to 41

Source documentation

Pairing the genus-one factors at opposite zeros cancels the exponential corrections.

Exact Lean statement

theorem hadamardGenusOneFactor_pair_cancellation (α w : ℂ) (hα : α ≠ 0) :
    hadamardGenusOneFactor (w / α) * hadamardGenusOneFactor (w / (-α)) = 1 - w ^ 2 / α ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hadamardGenusOneFactor_pair_cancellation (α w : ℂ) (hα : α ≠ 0) :    hadamardGenusOneFactor (w / α) * hadamardGenusOneFactor (w / (-α)) = 1 - w ^ 2 / α ^ 2 := by  unfold hadamardGenusOneFactor  have hsum : w / α + w / (-α) = 0 := by    field_simp [hα]    ring  have hexp : Complex.exp (w / α) * Complex.exp (w / (-α)) = 1 := by    rw [← Complex.exp_add, hsum, Complex.exp_zero]  calc    (1 - w / α) * Complex.exp (w / α) *        ((1 - w / (-α)) * Complex.exp (w / (-α)))        = ((1 - w / α) * (1 - w / (-α))) *            (Complex.exp (w / α) * Complex.exp (w / (-α))) := by          ring    _ = 1 - w ^ 2 / α ^ 2 := by      rw [hexp]      field_simp [hα]      ring