integrable_cexp_quadratic' — Mathlib

English

For complex b with Re(b) < 0, the quadratic exponential integral is integrable for any c,d in C.

Русский

При Re(b) < 0 интеграл квадратичного экспоненциального вида интегрируем для любых комплексных c,d.

LaTeX

$$$$ \text{Integrable}\left(x \mapsto e^{b x^2 + c x + d} \right) \quad (\Re(b) < 0). $$$$

Lean4

theorem _root_.integrable_cexp_quadratic' (hb : b.re < 0) (c d : ℂ) :
    Integrable (fun (x : ℝ) ↦ cexp (b * x ^ 2 + c * x + d)) :=
  by
  have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
  by_contra H
  simpa [hb', pi_ne_zero, Complex.exp_ne_zero, integral_undef H] using integral_cexp_quadratic hb c d

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