exponentialCDFReal — Mathlib

English

The CDF of the exponential distribution is defined as the cdf of the exponential measure: exponentialCDFReal(r) = cdf(expMeasure(r)).

Русский

CDF экспоненциального распределения определяется как CDF мере экспоненциального распределения: exponentialCDFReal(r) = cdf(expMeasure(r)).

LaTeX

$$$\text{exponentialCDFReal}(r) = \text{cdf}(\expMeasure(r))$$$

Lean4

/-- CDF of the exponential distribution -/
@[deprecated "Use `cdf (expMeasure r)` instead." (since := "2025-08-28")]
noncomputable def exponentialCDFReal (r : ℝ) : StieltjesFunction :=
  cdf (expMeasure r)

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