integrableOn_exp_mul_complex_Ioi — 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}) \\ (Ioi\ \\, c)$, when $\\operatorname{Re}(a) < 0$$$

Lean4

theorem integrableOn_exp_mul_complex_Ioi {a : ℂ} (ha : a.re < 0) (c : ℝ) :
    IntegrableOn (fun x : ℝ => Complex.exp (a * x)) (Ioi c) :=
  by
  refine (integrable_norm_iff ?_).mp ?_
  · apply Continuous.aestronglyMeasurable
    fun_prop
  ·
    simpa [Complex.norm_exp] using
      (integrableOn_Ioi_comp_mul_left_iff (fun x => exp (-x)) c (a := -a.re) (by simpa)).mpr <|
        integrableOn_exp_neg_Ioi _

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