lintegral_gammaPDF_of_nonpos — Mathlib

English

For any a, r ∈ ℝ and x ∈ ℝ with x ≤ 0 (i.e., hx: x ≤ 0), the Lebesgue integral of gammaPDF(a, r, y) over y ∈ (−∞, x) is zero.

Русский

Пусть a, r ∈ ℝ и x ∈ ℝ с условием x ≤ 0. Тогда линейный интеграл по y ∈ (−∞, x) от gammaPDF(a, r, y) равен 0.

LaTeX

$$$\int^{-}_{y \in Iio(x)} \gammaPDF(a,r,y) \, dy = 0 \quad\text{when } x \le 0$$$

Lean4

/-- The Lebesgue integral of the gamma pdf over nonpositive reals equals 0 -/
theorem lintegral_gammaPDF_of_nonpos {x a r : ℝ} (hx : x ≤ 0) : ∫⁻ y in Iio x, gammaPDF a r y = 0 :=
  by
  rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
  · rw [lintegral_zero, ← ENNReal.ofReal_zero]
  · intro a (_ : a < _)
    simp only [gammaPDF_eq, ENNReal.ofReal_eq_zero]
    rw [if_neg (by linarith)]

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