Theorems · Theorem · probability
ProbabilityTheory.measurable_betaPDFReal
∀ (α β : ℝ), Measurable (ProbabilityTheory.betaPDFReal α β)
The beta pdf is measurable.
- Defined in
- Mathlib.Probability.Distributions.Beta
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Measurablestatement · cited by 1,499
- measurable_constproof · cited by 156
- measurable_id'proof · cited by 145
- measurableSet_Iooproof · cited by 42
- Measurable.fun_mulproof · cited by 30
- Measurable.pow_constproof · cited by 26
- Measurable.const_mulproof · cited by 19
- Measurable.const_subproof · cited by 14
- ProbabilityTheory.betaproof · cited by 9
- Measurable.iteproof · cited by 8
- ProbabilityTheory.betaPDFRealstatement · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- ProbabilityTheory.stronglyMeasurable_betaPDFRealproof · cited by 0