Mathlib Map

Theorems · Definition · probability

ProbabilityTheory.beta

ℝ → ℝ → ℝ

The normalizing constant in the beta distribution.

Defined in
Mathlib.Probability.Distributions.Beta
Cited by
9 results in Mathlib
Foundations
Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ProbabilityTheory.betaPDFReal · cited by 4ProbabilityTheory.betaPDF…ProbabilityTheory.beta_pos · cited by 2ProbabilityTheory.beta_posProbabilityTheory.measurable_betaPDFReal · cited by 1ProbabilityTheory.measura…ProbabilityTheory.betaPDF_eq · cited by 1ProbabilityTheory.betaPDF…ProbabilityTheory.betaPDF_eq_zero_of_nonpos · cited by 1ProbabilityTheory.betaPDF…ProbabilityTheory.betaPDF_eq_zero_of_one_le · cited by 1ProbabilityTheory.betaPDF…ProbabilityTheory.betaPDF_of_pos_lt_one · cited by 1ProbabilityTheory.betaPDF…ProbabilityTheory.beta_eq_betaIntegralReal · cited by 1ProbabilityTheory.beta_eq…ProbabilityTheory.lintegral_betaPDF · cited by 1ProbabilityTheory.lintegr…ProbabilityTheory.lintegral_betaPDF_eq_one · cited by 1ProbabilityTheory.lintegr…Real · cited by 25697RealReal.Gamma · cited by 76Real.GammaProbabilityTheory.betaCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697
  • Real.Gammaproof · cited by 76

Cited by10

Results whose statement or proof uses this declaration.