isProbabilityMeasureBeta — Mathlib

English

Let α, β > 0. The beta measure βMeasure(α, β) is a probability measure.

Русский

Пусть α, β > 0. Мера βMeasure(α, β) является вероятностной мерой.

LaTeX

$$$ (\alpha > 0 \land \beta > 0) \rightarrow \mathrm{IsProbabilityMeasure}(\betaMeasure(\alpha, \beta)) $$$

Lean4

theorem isProbabilityMeasureBeta {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : IsProbabilityMeasure (betaMeasure α β) where
  measure_univ := by simp [betaMeasure, lintegral_betaPDF_eq_one hα hβ]

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