cdf_expMeasure_eq — Mathlib

English

For all r>0 and all x, 0 ≤ exponentialPDFReal(r,x).

Русский

Для всех r>0 и всех x, 0 ≤ exponentialPDFReal(r,x).

LaTeX

$$$ (r>0) \Rightarrow \forall x, 0 \le \text{exponentialPDFReal}(r, x) $$$

Lean4

/-- The CDF of the exponential distribution equals ``1 - exp (-(r * x))`` -/
theorem cdf_expMeasure_eq {r : ℝ} (hr : 0 < r) (x : ℝ) :
    cdf (expMeasure r) x = if 0 ≤ x then 1 - exp (-(r * x)) else 0 :=
  by
  rw [cdf_expMeasure_eq_lintegral hr, lintegral_exponentialPDF_eq_antiDeriv hr x, ENNReal.toReal_ofReal_eq_iff]
  split_ifs with h
  · simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff]
    exact mul_nonneg hr.le h
  · exact le_rfl

Похожие утверждения