cdf_gammaMeasure_eq_integral — Mathlib

English

For a > 0 and r > 0 and any x ∈ ℝ, cdf(gammaMeasure(a, r))(x) equals ∫_{(-∞, x]} gammaPDFReal(a, r)(t) dt.

Русский

Для a > 0 и r > 0 и для любого x ∈ ℝ, cdf(gammaMeasure(a, r))(x) равно ∫_{(-∞, x]} gammaPDFReal(a, r)(t) dt.

LaTeX

$$$cdf(\gammaMeasure(a,r))\, x = \int_{(-\infty, x]} \gammaPDFReal(a,r)(t)\,dt$$$

Lean4

theorem cdf_gammaMeasure_eq_integral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
    cdf (gammaMeasure a r) x = ∫ x in Iic x, gammaPDFReal a r x :=
  by
  have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasure_gammaMeasure ha hr
  rw [cdf_eq_real, gammaMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
  refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
  · exact ae_of_all _ fun b ↦ by simp [gammaPDFReal_nonneg ha hr]
  · fun_prop

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