English
For a nonzero complex number c, ∫_a^b exp(c x) dx equals (exp(c b) − exp(c a)) / c.
Русский
Пусть c ≠ 0, комплексное число; тогда ∫_a^b exp(c x) dx = (exp(c b) − exp(c a)) / c.
LaTeX
$$$\forall a,b \in \mathbb{R},\ \forall c \in \mathbb{C},\ c \neq 0 \Rightarrow \displaystyle \int_a^b e^{c x} \, dx = \frac{e^{c b} - e^{c a}}{c}$$$
Lean4
theorem integral_exp_mul_complex {c : ℂ} (hc : c ≠ 0) :
(∫ x in a..b, Complex.exp (c * x)) = (Complex.exp (c * b) - Complex.exp (c * a)) / c :=
by
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x :=
by
intro x
conv => congr
rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
· ring
· fun_prop
