integral_exp_mul_Ioi — Mathlib

English

For a real a < 0 and real c, the integral ∫_{c}^{∞} e^{a x} dx equals -e^{a c}/a.

Русский

Пусть a < 0 и c ∈ ℝ. Тогда ∫_{c}^{∞} e^{a x} dx = -e^{a c}/a.

LaTeX

$$$\\int_{c}^{\\infty} e^{a x} \\, dx = -\\frac{e^{a c}}{a}$, $a < 0$$$

Lean4

theorem integral_exp_mul_Ioi {a : ℝ} (ha : a < 0) (c : ℝ) :
    ∫ x : ℝ in Set.Ioi c, Real.exp (a * x) = -Real.exp (a * c) / a :=
  by
  simp_rw [Real.exp, ← RCLike.re_to_complex, Complex.ofReal_mul]
  rw [integral_re, integral_exp_mul_complex_Ioi (by simpa using ha), RCLike.re_to_complex, RCLike.re_to_complex,
    Complex.div_ofReal_re, Complex.neg_re]
  exact integrableOn_exp_mul_complex_Ioi (by simpa using ha) _

Похожие утверждения