exp_neg_integrableOn_Ioc — Mathlib

English

The exponential pdf Real is strongly measurable for every r.

Русский

Плотность экспоненциального распределения сильно измерима для каждого r.

LaTeX

$$$ \\text{stronglyMeasurable\_exponentialPDFReal}(r) := \\text{StronglyMeasurable}(\\text{exponentialPDFReal}(r)) $$$

Lean4

/-- A negative exponential function is integrable on intervals in `R≥0` -/
theorem exp_neg_integrableOn_Ioc {b x : ℝ} (hb : 0 < b) : IntegrableOn (fun x ↦ rexp (-(b * x))) (Ioc 0 x) :=
  by
  simp only [neg_mul_eq_neg_mul]
  exact (exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self

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