Theorems · Theorem · probability

ProbabilityTheory.lintegral_betaPDF

∀ {α β : ℝ},
  ∫⁻ (x : ℝ), ProbabilityTheory.betaPDF α β x =
    ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (1 / ProbabilityTheory.beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Defined in

Mathlib.Probability.Distributions.Beta

Cited by

1 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound