cdf_expMeasure_eq_lintegral — Mathlib

English

For hr>0 and x, the CDF of the exponential measure equals the real value of the lintegral of the pdf over (-∞, x], i.e., cdf(expMeasure(r))(x) = toReal(∫⁻ y in Iic x, exponentialPDFReal(r, y)).

Русский

CDF(expMeasure(r))(x) равно вещественному значению линтеграла плотности над (-∞, x].

LaTeX

$$$ \mathrm{cdf}(\expMeasure(r))(x) = \mathrm{toReal}\left(\int_{(-\infty, x]} \text{exponentialPDFReal}(r, y) \, dy\right) $$$

Lean4

theorem cdf_expMeasure_eq_lintegral {r : ℝ} (hr : 0 < r) (x : ℝ) :
    cdf (expMeasure r) x = ENNReal.toReal (∫⁻ x in Iic x, exponentialPDF r x) :=
  cdf_gammaMeasure_eq_lintegral zero_lt_one hr x

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