measurable_gammaPDFReal — Mathlib

English

The function gammaPDFReal(a, r) is measurable for all real a, r.

Русский

Функция gammaPDFReal(a, r) измерима для всех действительных a, r.

LaTeX

$$$\text{Measurable}(\gammaPDFReal(a,r))$$$

Lean4

/-- The gamma pdf is measurable. -/
@[fun_prop, measurability]
theorem measurable_gammaPDFReal (a r : ℝ) : Measurable (gammaPDFReal a r) :=
  Measurable.ite measurableSet_Ici (((measurable_id'.pow_const _).const_mul _).mul (measurable_id'.const_mul _).neg.exp)
    measurable_const

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