English
The CDF of the Pareto distribution with parameters t>0, r>0 at x is the integral of the Pareto pdf up to x.
Русский
CDF распределения Парето с параметрами t>0, r>0 в точке x равен интегралу плотности Парето по (-∞, x].
LaTeX
$$$\\mathrm{cdf}(\\mathrm{paretoMeasure}(t,r),x)=\\int_{-\\infty}^{x} \\mathrm{paretoPDFReal}(t,r,u) \\, du$$$
Lean4
/-- CDF of the Pareto distribution equals the integral of the PDF. -/
theorem cdf_paretoMeasure_eq_integral (ht : 0 < t) (hr : 0 < r) (x : ℝ) :
cdf (paretoMeasure t r) x = ∫ x in Iic x, paretoPDFReal t r x :=
by
have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
· exact ae_of_all _ fun _ ↦ by simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]
· fun_prop
