English
For a ∈ ℂ with Re(a) < 0 and real c, the improper integral ∫_{c}^{∞} exp(a x) dx equals -exp(a c)/a.
Русский
Пусть a ∈ ℂ, Re(a) < 0, и c ∈ ℝ. Тогда несобственный интеграл ∫_{c}^{∞} e^{a x} dx = -e^{a c}/a.
LaTeX
$$$\\int_{c}^{\\infty} \\exp(a x) \\, dx = -\\dfrac{\\exp(a c)}{a}$, при $\\Re(a) < 0$$$
Lean4
theorem integral_exp_mul_complex_Ioi {a : ℂ} (ha : a.re < 0) (c : ℝ) :
∫ x : ℝ in Set.Ioi c, Complex.exp (a * x) = -Complex.exp (a * c) / a :=
by
refine
tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c (integrableOn_exp_mul_complex_Ioi ha c) tendsto_id) ?_
simp_rw [integral_exp_mul_complex (c := a) (by aesop), id_eq]
suffices Tendsto (fun x : ℝ ↦ Complex.exp (a * x)) atTop (𝓝 0) by simpa using this.sub_const _ |>.div_const _
simpa [Complex.tendsto_exp_nhds_zero_iff] using tendsto_const_nhds.neg_mul_atTop ha tendsto_id
