integrableOn_exp_mul_Iic — Mathlib

English

For real a with a > 0, the function x ↦ e^{a x} is integrable on Iic c for any c.

Русский

Для действительного a с a > 0 функция x ↦ e^{a x} интегрируема на Iic c.

LaTeX

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

Lean4

theorem integrableOn_exp_mul_Iic {a : ℝ} (ha : 0 < a) (c : ℝ) : IntegrableOn (fun x : ℝ => Real.exp (a * x)) (Iic c) :=
  by
  have := Integrable.norm <| integrableOn_exp_mul_complex_Iic (a := a) (by simpa using ha) c
  simpa [Complex.norm_exp] using this

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