Theorems · Theorem · probability

ProbabilityTheory.cdf_gammaMeasure_eq_lintegral

∀ {a r : ℝ},
  0 < a →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gammaMeasure a r)) x =
          (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.gammaPDF a r x).toReal

Defined in

Mathlib.Probability.Distributions.Gamma

Cited by

1 results in Mathlib

Foundations

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