Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.Phi_circ.analyticAt_of_not_pole

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2096 to 2104

Source documentation

Phi_circ is analytic whenever we are away from the poles.

Exact Lean statement

theorem Phi_circ.analyticAt_of_not_pole (ν ε : ℝ) (z : ℂ) (h_not_pole : ∀ n : ℤ, z ≠ n - I * ν / (2 * π)) :
    AnalyticAt ℂ (Phi_circ ν ε) z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Phi_circ.analyticAt_of_not_pole (ν ε : ℝ) (z : ℂ) (h_not_pole : ∀ n : ℤ, z ≠ n - I * ν / (2 * π)) :    AnalyticAt ℂ (Phi_circ ν ε) z := by  set w : ℂ := -2 * π * I * z + ν  have h_an : AnalyticAt ℂ (fun s : ℂ ↦ coth (s / 2)) w := by    have heq : (fun s : ℂ ↦ coth (s / 2)) =ᶠ[nhds w] (fun s ↦ Complex.cosh (s / 2) / Complex.sinh (s / 2)) :=      Filter.Eventually.of_forall (fun s ↦ by unfold coth; simp [Complex.tanh_eq_sinh_div_cosh])    apply (analyticAt_congr heq).mpr    fun_prop (disch := exact sinh_ne_zero_of_not_pole h_not_pole)  unfold Phi_circ; fun_prop (disch := exact [h_an.comp (by fun_prop), by simp [w]; fun_prop])