stronglyMeasurable_gammaPDFReal

Mathlib.Probability.Distributions.Gamma

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.stronglyMeasurable_gammaPDFReal

← MathLib Explorer

English

The gamma pdf is strongly measurable for all real a, r.

Русский

Гамма-плотность сильно измерима для любых a, r.

LaTeX

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

Lean4

/-- The gamma pdf is strongly measurable -/
@[fun_prop, measurability]
theorem stronglyMeasurable_gammaPDFReal (a r : ℝ) : StronglyMeasurable (gammaPDFReal a r) :=
  (measurable_gammaPDFReal a r).stronglyMeasurable

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru