Source indexedtheorem · leanprover/lean4:v4.32.0

CH2.B.continuousAt_ofReal_ne_zero

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1554 to 1561

Mathematical statement

Exact Lean statement

theorem B.continuousAt_ofReal_ne_zero (ε s : ℝ) (hs : s ≠ 0) :
    ContinuousAt (fun t : ℝ ↦ B ε (t : ℂ)) s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem B.continuousAt_ofReal_ne_zero (ε s : ℝ) (hs : s ≠ 0) :    ContinuousAt (fun t : ℝ ↦ B ε (t : ℂ)) s := by  have h_eq : (fun t : ℝ ↦ (t : ℂ) * (coth ((t : ℂ) / 2) + ε) / 2) =ᶠ[nhds s] (fun t : ℝ ↦ B ε (t : ℂ)) := by    filter_upwards [eventually_ne_nhds hs] with t ht    simp [B, ht]  refine ContinuousAt.congr ?_ h_eq  refine ContinuousAt.div_const (ContinuousAt.mul (by fun_prop) (ContinuousAt.add ?_ continuousAt_const)) 2  exact ContinuousAt.coth (by fun_prop) (by simpa using sinh_ofReal_half_ne_zero hs)