lintegral_exponentialPDF_of_nonpos

English

For x ≤ 0, the Lebesgue integral of exponentialPDF r over (-∞, x) is 0.

Русский

Для x ≤ 0 интеграл Лебега от экспоненциальной плотности по (-∞, x) равен 0.

LaTeX

$$$ x \le 0 \Rightarrow \int_{(-\infty, x)} \text{exponentialPDF}(r, y) \, dy = 0 $$$

Lean4

/-- The Lebesgue integral of the exponential pdf over nonpositive reals equals 0 -/
theorem lintegral_exponentialPDF_of_nonpos {x r : ℝ} (hx : x ≤ 0) : ∫⁻ y in Iio x, exponentialPDF r y = 0 :=
  lintegral_gammaPDF_of_nonpos hx

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