integrableOn_exp_mul_complex_Iic — Mathlib

English

If Re(a) > 0, then exp(a x) is integrable on (-∞, c] for every real c.

Русский

Если Re(a) > 0, то e^{a x} интегрируема на (−∞, c] для любого c.

LaTeX

$$$\\text{IntegrableOn} (x \\mapsto e^{a x}) (Iic\\ c)$, $\\operatorname{Re}(a) > 0$$$

Lean4

theorem integrableOn_exp_mul_complex_Iic {a : ℂ} (ha : 0 < a.re) (c : ℝ) :
    IntegrableOn (fun x : ℝ => Complex.exp (a * x)) (Iic c) := by
  simpa using
    Iff.mpr integrableOn_Iic_iff_integrableOn_Iio
      (integrableOn_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)).comp_neg_Iio

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