English
The vertical integral tends to 0 as the height goes to infinity, for nonzero real parts.
Русский
Вертикальный интеграл стремится к нулю при стремлении высоты к бесконечности.
LaTeX
$$$$ \lim_{T \to \infty} \mathrm{verticalIntegral}(b,c,T) = 0 \quad (\Re(b) > 0). $$$$
Lean4
theorem tendsto_verticalIntegral (hb : 0 < b.re) (c : ℝ) : Tendsto (verticalIntegral b c) atTop (𝓝 0) := by
-- complete proof using squeeze theorem:
rw [tendsto_zero_iff_norm_tendsto_zero]
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ?_ (Eventually.of_forall fun _ => norm_nonneg _)
((eventually_ge_atTop (0 : ℝ)).mp (Eventually.of_forall fun T hT => verticalIntegral_norm_le hb c hT))
rw [(by ring : 0 = 2 * |c| * 0)]
refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _
apply tendsto_atTop_add_const_right
simp_rw [sq, ← mul_assoc, ← sub_mul]
refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id
exact (tendsto_const_mul_atTop_of_pos hb).mpr tendsto_id
