WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Pareto distribution

Revision #1457 → #2107 · back to history

modifiedPareto (Type I) survival functione781440bdada
FieldFrom #1457To #2107
mathlib.decl—ProbabilityTheory.paretoMeasure
mathlib.match_kind——
mathlib.module—Mathlib.Probability.Distributions.Pareto
note—The Pareto measure is defined, so the survival function `1 - cdf` is derivable, but no explicit closed-form `(xm/x)^α` survival statement is present.
status—partial
modifiedScale and shape parameters876e9553f85e
FieldFrom #1457To #2107
mathlib.decl—ProbabilityTheory.paretoPDFReal
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Distributions.Pareto
note—`paretoPDFReal t r x` is parametrized by scale `t` and shape `r`, matching the Wikipedia parameters `x_m` and `α`.
status—formalized
modifiedCumulative distribution functione74a41da5d08
FieldFrom #1457To #2107
mathlib.decl—ProbabilityTheory.cdf_paretoMeasure_eq_integral
mathlib.match_kind—generalization
mathlib.module—Mathlib.Probability.Distributions.Pareto
note—Mathlib states the CDF as the integral of the PDF, but the closed-form `1 - (x_m/x)^α` for `x ≥ x_m` is not separately proved.
status—partial
modifiedProbability density function2ac0677375ef
FieldFrom #1457To #2107
mathlib.decl—ProbabilityTheory.paretoPDFReal
mathlib.match_kind—exact
mathlib.module—Mathlib.Probability.Distributions.Pareto
note—`paretoPDFReal t r x = r * t^r * x^(-(r+1))` for `t ≤ x` is exactly the Wikipedia PDF formula.
status—formalized
modifiedExpected value59a2a8c14307
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No expected-value / mean statement for `paretoMeasure` exists in Mathlib.
status—not_formalized
modifiedVariance357211fb9c8a
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No variance statement for the Pareto distribution exists in Mathlib.
status—not_formalized
modifiedRaw moments777923de858e
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No raw-moment formula for the Pareto distribution exists in Mathlib.
status—not_formalized
modifiedMoment generating functionc70c33b8b5ac
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Generic `mgf` exists in Mathlib's `Probability/Moments`, but no specialization to Pareto is proved.
status—not_formalized
modifiedCharacteristic function1e75ec77f54b
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Generic `charFun` exists, but no Pareto characteristic-function formula is proved in Mathlib.
status—not_formalized
modifiedConditional distribution of Pareto2ddb65d81b28
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No conditional-distribution statement for Pareto is present in Mathlib.
status—not_formalized
modifiedConditional expected value105bfda47f8b
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No conditional-expectation formula for Pareto is present in Mathlib.
status—not_formalized
modifiedCharacterization theorem4db9b4e2f1ba
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No characterization theorem (conditional-mean linear in threshold ⇒ Pareto) is present in Mathlib.
status—not_formalized
modifiedGeometric mean988c80e56b22
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No geometric-mean formula for Pareto is present in Mathlib.
status—not_formalized
modifiedHarmonic mean4b16b2008d88
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No harmonic-mean formula for Pareto is present in Mathlib.
status—not_formalized
modifiedLog-log linearity of PDF88463ad12708
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No statement about the log-log linearity of the Pareto PDF appears in Mathlib.
status—not_formalized
modifiedPareto hierarchyebe9308406d6
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Only the Type I Pareto distribution is in Mathlib; no Pareto hierarchy is defined.
status—not_formalized
modifiedPareto Types I–IV05b2a0ed6d4f
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Only the Type I Pareto distribution is in Mathlib; Types II–IV are absent.
status—not_formalized
modifiedLomax distribution0c1cef37b61f
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Lomax distribution is defined in Mathlib (grep returned no matches).
status—not_formalized
modifiedFeller–Pareto distributiond53a5489418e
FieldFrom #1457To #2107
anchor.snippetFellerdefines a Pareto variable by transformation
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Tightened snippet from the too-generic 'Feller' to a unique phrase from the same sentence.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedFeller–Pareto via Gamma variables29ee7a104667
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Feller–Pareto construction from Gamma variables is present in Mathlib.
status—not_formalized
modifiedInverse-Pareto / Power distributionb814b12d4dc7
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No inverse-Pareto / power distribution is defined in Mathlib.
status—not_formalized
modifiedPareto from exponential65fbe4b28ef0
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Both `paretoMeasure` and `exponentialPDF` exist, but no lemma relating them via `Y = x_m exp(X/α)` is present.
status—not_formalized
modifiedHierarchical exponential construction25edd92fcd2e
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No hierarchical/mixture construction of Pareto from exponentials is in Mathlib.
status—not_formalized
modifiedPareto–GPD equivalence71ce6d5f7583
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The generalized Pareto distribution is not in Mathlib, so the equivalence is unstated.
status—not_formalized
modifiedBounded Pareto distribution158e58d3257e
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No bounded/truncated Pareto distribution is defined in Mathlib.
status—not_formalized
modifiedBounded Pareto PDF9c956135f3d7
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No bounded-Pareto PDF formula is present in Mathlib.
status—not_formalized
modifiedInverse-transform for bounded Pareto2961894c3ec1
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No inverse-transform sampling formula for bounded Pareto is present in Mathlib.
status—not_formalized
modifiedSymmetric Pareto CDF8a8f3650637a
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No symmetric Pareto CDF is defined in Mathlib.
status—not_formalized
modifiedSymmetric Pareto PDF7609b8e7b63d
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No symmetric Pareto PDF is defined in Mathlib.
status—not_formalized
modifiedSymmetric Pareto variance9101f41272b5
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No variance statement for the symmetric Pareto distribution is in Mathlib.
status—not_formalized
modifiedZero Symmetric Pareto CDFffb97e24804d
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No zero-symmetric Pareto CDF is defined in Mathlib.
status—not_formalized
modifiedZero Symmetric Pareto PDF82536a86631f
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No zero-symmetric Pareto PDF is defined in Mathlib.
status—not_formalized
modifiedLikelihood function96111a5f9fab
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No likelihood function for the Pareto distribution is defined in Mathlib.
status—not_formalized
modifiedLog-likelihood functiond327e36ec6c7
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No log-likelihood for the Pareto distribution is defined in Mathlib.
status—not_formalized
modifiedMLE for α12774c549a9f
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No MLE for the Pareto shape parameter is proved in Mathlib.
status—not_formalized
modifiedMalik joint distributioneb2377cad27f
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No joint distribution of the Pareto MLEs is stated in Mathlib.
status—not_formalized
modifiedZipf from Paretofd8ec428c1e4
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Zipf's law is not present in Mathlib (no `Zipf` declarations found).
status—not_formalized
modified80/20 law equivalence6f7b6b21423a
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The 80/20 ⇔ α = log_4 5 equivalence is not formalized in Mathlib.
status—not_formalized
modifiedLorenz curvee8634262ee85
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Lorenz curve is not defined in Mathlib (no `Lorenz` declarations found).
status—not_formalized
modifiedLorenz curve for Pareto3a78476170d9
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Lorenz curve for the Pareto distribution is formalized in Mathlib.
status—not_formalized
modifiedGini coefficient for Paretobfbc66148180
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Gini coefficient is not defined in Mathlib, so its Pareto value is not formalized.
status—not_formalized
modifiedInverse transform sampling8b778d888d55
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No inverse-transform sampling lemma for Pareto is present in Mathlib.
status—not_formalized
modifiedOxfam wealth estimate7c60226a78c8
FieldFrom #1457To #2107
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This is an applied empirical example, not formalizable in Mathlib.
status—not_formalized
addedMLE for x_mac118fd52623
addedExpected statistical error of α̂5ed6677a5338
addedLindy effect (life expectancy ∝ age)c23428a97b49
addedPareto principle exponent log_4 576757f2522bf