integrable_cexp_neg_mul_sq_add_real_mul_I

English

The function x ↦ exp(−b_red x^2) with a linear shift is integrable on R for Re(b)>0.

Русский

Функция x ↦ exp(−b_re x^2) с линейным сдвигом интегрируема на R при Re(b)>0.

LaTeX

$$$$ \int_{-\infty}^{\infty} |\mathrm{cexp}(-b (x + c I)^2)| dx < \infty. $$$$

Lean4

theorem integrable_cexp_neg_mul_sq_add_real_mul_I (hb : 0 < b.re) (c : ℝ) :
    Integrable fun x : ℝ => cexp (-b * (x + c * I) ^ 2) :=
  by
  refine
    ⟨(Complex.continuous_exp.comp
          (continuous_const.mul ((continuous_ofReal.add continuous_const).pow 2))).aestronglyMeasurable,
      ?_⟩
  rw [← hasFiniteIntegral_norm_iff]
  simp_rw [norm_cexp_neg_mul_sq_add_mul_I' hb.ne', neg_sub _ (c ^ 2 * _), sub_eq_add_neg _ (b.re * _), Real.exp_add]
  suffices Integrable fun x : ℝ => exp (-(b.re * x ^ 2)) by
    exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _
  simp_rw [← neg_mul]
  apply integrable_exp_neg_mul_sq hb

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