cdf_gammaMeasure_eq_lintegral — Mathlib

English

For a > 0 and r > 0 and any x, the gamma measure CDF equals the real-to-real of the lintegral of gammaPDF.

Русский

Для a > 0 и r > 0 и произвольного x, CDF гамма-меры равна toReal(∫⁻ gammaPDF(a,r)) на отрезке Iic(x).

LaTeX

$$$cdf(\gammaMeasure(a,r))\, x = \operatorname{toReal}\left(\int^{-}_{t\in Iic(x)} \gammaPDF(a,r)(t)\right)$$$

Lean4

theorem cdf_gammaMeasure_eq_lintegral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
    cdf (gammaMeasure a r) x = ENNReal.toReal (∫⁻ x in Iic x, gammaPDF a r x) :=
  by
  have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasure_gammaMeasure ha hr
  simp only [gammaPDF, cdf_eq_real]
  simp [gammaMeasure, gammaPDF, measureReal_def]

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