Documentation Verification Report

Pareto

📁 Source: Mathlib/Probability/Distributions/Pareto.lean

Statistics

Metric	Count
Definitions `paretoMeasure`, `paretoPDF`, `paretoPDFReal`	3
Theorems `cdf_paretoMeasure_eq_integral`, `cdf_paretoMeasure_eq_lintegral`, `isProbabilityMeasure_paretoMeasure`, `lintegral_paretoPDF_eq_one`, `lintegral_paretoPDF_of_le`, `measurable_paretoPDFReal`, `paretoCDFReal_eq_integral`, `paretoCDFReal_eq_lintegral`, `paretoPDFReal_nonneg`, `paretoPDFReal_pos`, `paretoPDF_eq`, `paretoPDF_of_le`, `paretoPDF_of_lt`, `stronglyMeasurable_paretoPDFReal`	14
Total	17

ProbabilityTheory

Definitions

Name	Category	Theorems
`paretoMeasure` 📖	CompOp	5 math math: `paretoCDFReal_eq_lintegral`, `isProbabilityMeasure_paretoMeasure`, `cdf_paretoMeasure_eq_integral`, `paretoCDFReal_eq_integral`, `cdf_paretoMeasure_eq_lintegral`
`paretoPDF` 📖	CompOp	7 math math: `paretoCDFReal_eq_lintegral`, `paretoPDF_of_le`, `lintegral_paretoPDF_of_le`, `lintegral_paretoPDF_eq_one`, `paretoPDF_eq`, `paretoPDF_of_lt`, `cdf_paretoMeasure_eq_lintegral`
`paretoPDFReal` 📖	CompOp	6 math math: `paretoPDFReal_pos`, `cdf_paretoMeasure_eq_integral`, `measurable_paretoPDFReal`, `paretoCDFReal_eq_integral`, `paretoPDFReal_nonneg`, `stronglyMeasurable_paretoPDFReal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cdf_paretoMeasure_eq_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `paretoMeasure` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `paretoPDFReal`	—	`isProbabilityMeasure_paretoMeasure` `cdf_eq_real` `paretoMeasure.eq_1` `MeasureTheory.measureReal_def` `MeasureTheory.withDensity_apply` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `paretoPDFReal_nonneg` `LT.lt.le` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `stronglyMeasurable_paretoPDFReal`
`cdf_paretoMeasure_eq_lintegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `paretoMeasure` `ENNReal.toReal` `MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `paretoPDF`	—	`isProbabilityMeasure_paretoMeasure` `cdf_eq_real` `paretoMeasure.eq_1` `MeasureTheory.measureReal_def` `MeasureTheory.withDensity_apply` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`isProbabilityMeasure_paretoMeasure` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.IsProbabilityMeasure` `Real.measurableSpace` `paretoMeasure`	—	`MeasureTheory.withDensity_apply` `MeasureTheory.Measure.restrict_univ` `lintegral_paretoPDF_eq_one`
`lintegral_paretoPDF_eq_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `paretoPDF` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`lintegral_paretoPDF_of_le` `le_refl` `MeasureTheory.setLIntegral_congr_fun` `measurableSet_Ici` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `paretoPDF_of_le` `ENNReal.toReal_eq_one_iff` `MeasureTheory.lintegral_add_compl` `Set.compl_Ici` `add_zero` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyLE.eq_1` `MeasureTheory.ae_restrict_iff'` `Filter.univ_mem'` `lt_of_lt_of_le` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.rpow_pos_of_pos` `MeasureTheory.AEStronglyMeasurable.congr` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `measurable_paretoPDFReal` `MeasureTheory.ae_of_all` `eq_true_intro` `MeasureTheory.integral_Ici_eq_integral_Ioi` `Real.noAtoms_volume` `MeasureTheory.integral_const_mul` `integral_Ioi_rpow_of_lt` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `neg_add_rev` `neg_add_cancel_comm` `neg_div_neg_eq` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Real.rpow_add` `add_neg_cancel` `Real.rpow_zero`
`lintegral_paretoPDF_of_le` 📖	mathematical	`Real` `Real.instLE`	`MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iio` `Real.instPreorder` `paretoPDF` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.setLIntegral_congr_fun` `measurableSet_Iio` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `le_refl` `MeasureTheory.lintegral_zero` `ENNReal.ofReal_zero`
`measurable_paretoPDFReal` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `paretoPDFReal`	—	`Measurable.ite` `measurableSet_Ici` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.const_mul` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measurable.pow_const` `Real.hasMeasurablePow` `measurable_id` `measurable_const`
`paretoCDFReal_eq_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `paretoMeasure` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `paretoPDFReal`	—	`cdf_paretoMeasure_eq_integral`
`paretoCDFReal_eq_lintegral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `paretoMeasure` `ENNReal.toReal` `MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Iic` `Real.instPreorder` `paretoPDF`	—	`cdf_paretoMeasure_eq_lintegral`
`paretoPDFReal_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`paretoPDFReal`	—	`le_iff_eq_or_lt` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Real.rpow_nonneg` `lt_of_lt_of_le` `le_of_lt` `Real.rpow_pos_of_pos` `Mathlib.Meta.Positivity.nonneg_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero`
`paretoPDFReal_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE`	`paretoPDFReal`	—	`paretoPDFReal.eq_1` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_pos_of_pos`
`paretoPDF_eq` 📖	mathematical	—	`paretoPDF` `ENNReal.ofReal` `Real` `Real.instLE` `Real.decidableLE` `Real.instMul` `Real.instPow` `Real.instNeg` `Real.instAdd` `Real.instOne` `Real.instZero`	—	—
`paretoPDF_of_le` 📖	mathematical	`Real` `Real.instLE`	`paretoPDF` `ENNReal.ofReal` `Real.instMul` `Real.instPow` `Real.instNeg` `Real.instAdd` `Real.instOne`	—	—
`paretoPDF_of_lt` 📖	mathematical	`Real` `Real.instLT`	`paretoPDF` `ENNReal` `instZeroENNReal`	—	`not_le` `ENNReal.ofReal_zero`
`stronglyMeasurable_paretoPDFReal` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.measurableSpace` `paretoPDFReal`	—	`Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `measurable_paretoPDFReal`

---

← Back to Index