simp [Complex.log_im, arg_eq_zero_iff, div_nonneg (Nat.cast_nonneg _) X_pos.le]
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
ht : ∀ (t : ℝ), -(2 + ↑t * I) = -1 * (2 + ↑t * I)
hn : ∀ (n : ℂ), (n / ↑X) ^ (-1) = ↑X / n
n : ℕ
⊢ ((↑n / ↑X).log * -1).im = 0
no goals