English
For real b > 0 and s ∈ (-1, ∞), the integrand x^s e^{-b x^2} is integrable on the real line, reflecting the balance between polynomial growth and Gaussian decay.
Русский
При b > 0 и s > -1 интегрируемость x^s e^{-b x^2} на всей оси сохраняется.
LaTeX
$$$$\\int_{-\\\\infty}^{\\\\infty} x^s e^{-b x^2} \\, dx < \\infty \\quad (b>0, s>-1).$$$$
Lean4
theorem integrable_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
Integrable fun x : ℝ => x ^ s * exp (-b * x ^ 2) :=
by
rw [← integrableOn_univ, ← @Iio_union_Ici _ _ (0 : ℝ), integrableOn_union, integrableOn_Ici_iff_integrableOn_Ioi]
refine ⟨?_, integrableOn_rpow_mul_exp_neg_mul_sq hb hs⟩
rw [←
(Measure.measurePreserving_neg (volume : Measure ℝ)).integrableOn_comp_preimage
(Homeomorph.neg ℝ).measurableEmbedding]
simp only [Function.comp_def, neg_sq, neg_preimage, neg_Iio, neg_zero]
apply Integrable.mono' (integrableOn_rpow_mul_exp_neg_mul_sq hb hs)
· apply Measurable.aestronglyMeasurable
exact (measurable_id'.neg.pow measurable_const).mul ((measurable_id'.pow measurable_const).const_mul (-b)).exp
· have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
filter_upwards [ae_restrict_mem this] with x hx
have h'x : 0 ≤ x := le_of_lt hx
rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (exp_pos _).le]
apply mul_le_mul_of_nonneg_right _ (exp_pos _).le
simpa [abs_of_nonneg h'x] using abs_rpow_le_abs_rpow (-x) s
