simp [h, nterm]
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
no goals