Theorems · Theorem · probability

ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv

∀ {r : ℝ},
  0 < r →
    ∀ (x : ℝ),
      ∫⁻ (y : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDF r y =
        ENNReal.ofReal (if 0 ≤ x then 1 - Real.exp (-(r * x)) else 0)

Defined in

Mathlib.Probability.Distributions.Exponential

Cited by

1 results in Mathlib

Foundations

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