Theorems · Theorem · probability

ProbabilityTheory.cdf_paretoMeasure_eq_integral

∀ {t r : ℝ},
  0 < t →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x =
          ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.paretoPDFReal t r x

CDF of the Pareto distribution equals the integral of the PDF.

Defined in: Mathlib.Probability.Distributions.Pareto
Cited by: 0 results in Mathlib
Foundations: Depth 274 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasureTheory.Measureproof · cited by 10,939
ENNRealproof · cited by 9,879
LT.lt.leproof · cited by 2,189
MeasureTheory.integralstatement and proof · cited by 1,779
MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
Set.Iicstatement and proof · cited by 1,111
ENNReal.toRealproof · cited by 859
MeasureTheory.Measure.realproof · cited by 530
MeasureTheory.IsProbabilityMeasureproof · cited by 392
MeasureTheory.Measure.withDensityproof · cited by 265

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.