lintegral_paretoPDF_of_le — Mathlib

English

If x ≤ t, then the integral of the Pareto pdf over the interval (−∞, x) is zero.

Русский

Если x ≤ t, то интеграл плотности Парето по промежутку (−∞, x) равен нулю.

LaTeX

$$$\\displaystyle \\int_{-\\infty}^{x} \\mathrm{paretoPDF}(t,r,y) \\, dy = 0 \\quad \\text{for } x \\le t$$$

Lean4

/-- The Lebesgue integral of the Pareto pdf over reals `≤ t` equals `0`. -/
theorem lintegral_paretoPDF_of_le (hx : x ≤ t) : ∫⁻ y in Iio x, paretoPDF t r y = 0 :=
  by
  rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
  · rw [lintegral_zero, ← ENNReal.ofReal_zero]
  · intro a (_ : a < _)
    simp only [paretoPDF_eq, ENNReal.ofReal_eq_zero]
    rw [if_neg (by linarith)]

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