English
The measure associated with the Pareto distribution is defined by volume with density paretoPDF.
Русский
Мера, соответствующая распределению Парето, задаётся как мера с плотностью paretoPDF.
LaTeX
$$$\\mathrm{paretoMeasure}(t,r)=\\mathrm{volume}.\\mathrm{withDensity}(\\mathrm{paretoPDF}(t,r))$$$
Lean4
/-- The pdf of the Pareto distribution integrates to `1`. -/
@[simp]
theorem lintegral_paretoPDF_eq_one (ht : 0 < t) (hr : 0 < r) : ∫⁻ x, paretoPDF t r x = 1 :=
by
have leftSide : ∫⁻ x in Iio t, paretoPDF t r x = 0 := lintegral_paretoPDF_of_le (le_refl t)
have rightSide : ∫⁻ x in Ici t, paretoPDF t r x = ∫⁻ x in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1))) :=
setLIntegral_congr_fun measurableSet_Ici (fun _ ↦ paretoPDF_of_le)
rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici, leftSide, rightSide, add_zero,
← integral_eq_lintegral_of_nonneg_ae]
· rw [integral_Ici_eq_integral_Ioi, integral_const_mul, integral_Ioi_rpow_of_lt _ ht]
· simp [field, ← rpow_add ht]
linarith
· rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
refine ae_of_all _ fun x (hx : t ≤ x) ↦ ?_
have := lt_of_lt_of_le ht hx
positivity
· apply (measurable_paretoPDFReal t r).aestronglyMeasurable.congr
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_
simp_rw [paretoPDFReal, eq_true_intro hx, ite_true]
