cdf_paretoMeasure_eq_lintegral — Mathlib

English

The CDF can also be expressed as the real-to-ENNReal conversion of the integral of the Pareto pdf up to x.

Русский

CDF может также выражаться через преобразование из ENNReal реального интеграла плотности Парето до x.

LaTeX

$$$\\mathrm{cdf}(\\mathrm{paretoMeasure}(t,r)).\\mathrm{toFun}(x) = \\mathrm{ENNReal.toReal}\\left(\\int_{-\\infty}^{x} \\mathrm{paretoPDFReal}(t,r,y) \\, dy\\right)$$$

Lean4

theorem cdf_paretoMeasure_eq_lintegral (ht : 0 < t) (hr : 0 < r) (x : ℝ) :
    cdf (paretoMeasure t r) x = ENNReal.toReal (∫⁻ x in Iic x, paretoPDF t r x) :=
  by
  have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
  rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

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