Revision #3167 → #3711 · back to history
modifiedExponential distributionde6012bcb6ed
| Field | From #3167 | To #3711 |
|---|
| note | `expMeasure r` is the exponential measure on ℝ with rate `r`, defined as `gammaMeasure 1 r`. | Verified: `expMeasure r := gammaMeasure 1 r` in `Mathlib/Probability/Distributions/Exponential.lean`. |
modifiedPDF of exponential distribution30f3851d9099
| Field | From #3167 | To #3711 |
|---|
| note | `exponentialPDFReal r x = r * exp (-(r*x))` for `0 ≤ x` and `0` otherwise (via `exponentialPDF_eq`). | Verified: `exponentialPDF_eq` gives `r * exp (-(r*x))` on `0 ≤ x` and `0` else. |
modifiedRate parametercd06ab3ae3eb
| Field | From #3167 | To #3711 |
|---|
| note | The rate parameter is the `r : ℝ` argument of `exponentialPDFReal`/`expMeasure`, with positivity assumed via `hr : 0 < r`. | Verified: the `r : ℝ` argument of `exponentialPDFReal`/`expMeasure` is the rate, with `0 < r` used throughout (e.g. `isProbabilityMeasure_expMeasure`). |
modifiedInfinite divisibilitya91cdfd1e705
| Field | From #3167 | To #3711 |
|---|
| note | No notion of infinite divisibility or its instance for the exponential distribution was found in Mathlib. | Verified: no `InfinitelyDivisible`/`infinitelyDivisible` definition exists anywhere in `Mathlib/`. |
modifiedCDF of exponential distributionf961d8618864
| Field | From #3167 | To #3711 |
|---|
| note | `cdf_expMeasure_eq` proves `cdf (expMeasure r) x = 1 - exp (-(r*x))` for `0 ≤ x` and `0` else. | Verified: `cdf_expMeasure_eq` states `cdf (expMeasure r) x = if 0 ≤ x then 1 - exp (-(r*x)) else 0`. |
modifiedScale parameter parametrization61fa8bf9eebf
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Alternative parametrization","snippet":"The exponential distribution is sometimes parametrized in terms of the scale parameter"},{"type":"math_alttext","value":"{\\displaystyle f(x;\\beta )={\\begin{cases}{\\frac {1}{\\beta }}e^{-x/\\beta }&x\\geq 0,\\\\0&x<0.\\end{cases}}\\qquad \\qquad F(x;\\beta )={\\begin{cases}1-e^{-x/\\beta }&x\\geq 0,\\\\0&x<0.\\end{cases}}}"}] | — |
| note | Mathlib only provides the rate-parameter form; no scale-parameter alternative parametrization is defined. | Verified: `Mathlib/Probability/Distributions/Exponential.lean` only exposes the rate-parameter form. |
modifiedMean of exponential distributiond29b511f1e69
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Mean, variance, moments, and median","snippet":"The mean or expected value of an exponentially distributed random variable"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {E} [X]={\\frac {1}{\\lambda }}.}"}] | — |
| note | No computation of `∫ x ∂(expMeasure r) = 1/r` is present in `Mathlib/Probability/Distributions/Exponential.lean`. | Verified: no expectation lemma for `expMeasure` appears in `Mathlib/Probability/Distributions/Exponential.lean`. |
modifiedVariance of exponential distributione2a71e7f5ebd
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Mean, variance, moments, and median","snippet":"The variance of X is given by"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Var} [X]={\\frac {1}{\\lambda ^{2}}},}"}] | — |
| note | No variance formula for `expMeasure` was found. | Verified: no `variance` lemma for `expMeasure` is present in Mathlib. |
modifiedMoments of exponential distribution4bf9e98b92f1
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Mean, variance, moments, and median","snippet":"The moments of X , for"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {E} \\left[X^{n}\\right]={\\frac {n!}{\\lambda ^{n}}}.}"}] | — |
| note | No general moment formula `E[X^n] = n!/λ^n` for the exponential distribution was found. | Verified: no general moment formula for the exponential distribution appears in Mathlib. |
modifiedCentral moments of exponential distributionbf312bfa8d33
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Mean, variance, moments, and median","snippet":"The central moments of X , for"},{"type":"math_alttext","value":"{\\displaystyle \\mu _{n}={\\frac {!n}{\\lambda ^{n}}}={\\frac {n!}{\\lambda ^{n}}}\\sum _{k=0}^{n}{\\frac {(-1)^{k}}{k!}}.}"}] | — |
| note | No central moment formula for the exponential distribution was found. | Verified: no central-moment formula for the exponential distribution is present in Mathlib. |
modifiedMedian of exponential distributionb478f7eefab1
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Mean, variance, moments, and median","snippet":"The median of X is given by"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {m} [X]={\\frac {\\ln(2)}{\\lambda }}<\\operatorname {E} [X],}"},{"type":"math_alttext","value":"{\\displaystyle \\left|\\operatorname {E} \\left[X\\right]-\\operatorname {m} \\left[X\\right]\\right|={\\frac {1-\\ln(2)}{\\lambda }}<{\\frac {1}{\\lambda }}=\\operatorname {\\sigma } [X],}"}] | — |
| note | No general notion of `median` of a measure was found in `Mathlib/Probability`. | Verified: no median-of-measure definition (nor an exponential instance) is present in `Mathlib/Probability`. |
modifiedMemorylessness relation08f2c75d5713
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Memorylessness property of exponential random variable","snippet":"An exponentially distributed random variable T obeys the relation"},{"type":"math_alttext","value":"{\\displaystyle \\Pr \\left(T>s+t\\mid T>s\\right)=\\Pr(T>t),\\qquad \\forall s,t\\geq 0.}"}] | — |
| note | No `memoryless` predicate or proof for the exponential distribution was found in Mathlib. | Verified: no `memoryless`/`Memoryless` occurrences anywhere under `Mathlib/`. |
modifiedCharacterization of memoryless distributions1862554a2142
| Field | From #3167 | To #3711 |
|---|
| note | Memorylessness is not formalized, so no such characterization exists in Mathlib. | Verified: memorylessness is not formalized, so no such characterization exists. |
modifiedConstant failure rate characterization8905409f2985
| Field | From #3167 | To #3711 |
|---|
| note | No notion of hazard/failure rate or its characterization is present in Mathlib. | Verified: no hazard/failure-rate notion appears in Mathlib. |
modifiedQuantile functionef5e68f29055
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Quantiles","snippet":"The quantile function (inverse cumulative distribution function) for Exp"},{"type":"math_alttext","value":"{\\displaystyle F^{-1}(p;\\lambda )={\\frac {-\\ln(1-p)}{\\lambda }},\\qquad 0\\leq p<1}"}] | — |
| note | No quantile-function formula for the exponential distribution was found. | Verified: no exponential-specific quantile function lemma is present. |
modifiedQuartiles of exponential distributionc46e137a752e
| Field | From #3167 | To #3711 |
|---|
| note | No quartile computation for the exponential distribution was found. | Verified: no quartile computation for the exponential distribution exists in Mathlib. |
modifiedInterquartile rangea1e58a756063
| Field | From #3167 | To #3711 |
|---|
| note | No interquartile range result for the exponential distribution was found. | Verified: no interquartile-range lemma for the exponential distribution exists. |
modifiedConditional Value at Riske1065989b18d
| Field | From #3167 | To #3711 |
|---|
| note | No CVaR/expected-shortfall definitions appear anywhere in Mathlib. | Verified: no `CVaR`/`ExpectedShortfall` occurrences in `Mathlib/`. |
modifiedBuffered Probability of Exceedanceff518bd1b1fa
| Field | From #3167 | To #3711 |
|---|
| note | No buffered probability of exceedance is defined in Mathlib. | Verified: no buffered probability of exceedance is defined anywhere in Mathlib. |
modifiedKullback–Leibler divergence of exponentials744860057fcc
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Kullback–Leibler divergence","snippet":"The directed Kullback–Leibler divergence in nats of"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\Delta (\\lambda _{0}\\parallel \\lambda )&=\\mathbb {E} _{\\lambda _{0}}\\left(\\log {\\frac {p_{\\lambda _{0}}(x)}{p_{\\lambda }(x)}}\\right)\\\\&=\\mathbb {E} _{\\lambda _{0}}\\left(\\log {\\frac {\\lambda _{0}e^{\\lambda _{0}x}}{\\lambda e^{\\lambda x}}}\\right)\\\\&=\\log(\\lambda _{0})-\\log(\\lambda )-(\\lambda _{0}-\\lambda )E_{\\lambda _{0}}(x)\\\\&=\\log(\\lambda _{0})-\\log(\\lambda )+{\\frac {\\lambda }{\\lambda _{0}}}-1.\\end{aligned}}}"}] | — |
| note | General KL divergence is formalized but the closed-form formula `λ₀/λ₁ − 1 − log(λ₀/λ₁)` for two exponentials is not. | Verified: `InformationTheory.klDiv` is defined in general, but no closed-form for two exponentials is present. |
modifiedMaximum entropy distribution298a1bac26ce
| Field | From #3167 | To #3711 |
|---|
| note | No maximum-entropy characterization is found for the exponential distribution in Mathlib. | Verified: no maximum-entropy characterization of the exponential distribution appears in Mathlib. |
modifiedMinimum of independent exponentials1374609f084b
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Distribution of the minimum of exponential random variables","snippet":"Let X 1 , ..., X n be independent exponentially distributed random variables with rate parameters"},{"type":"math_alttext","value":"{\\displaystyle \\min \\left\\{X_{1},\\dotsc ,X_{n}\\right\\}}"},{"type":"math_alttext","value":"{\\displaystyle \\lambda =\\lambda _{1}+\\dotsb +\\lambda _{n}.}"}] | — |
| note | No theorem that `min Xᵢ ∼ Exp(∑ λᵢ)` was found. | Verified: no theorem that the minimum of independent exponentials is exponential appears in Mathlib. |
modifiedIndex of minimum is categorical14110add1c72
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Distribution of the minimum of exponential random variables","snippet":"The index of the variable which achieves the minimum is distributed according to the categorical distribution"},{"type":"math_alttext","value":"{\\displaystyle \\Pr \\left(X_{k}=\\min\\{X_{1},\\dotsc ,X_{n}\\}\\right)={\\frac {\\lambda _{k}}{\\lambda _{1}+\\dotsb +\\lambda _{n}}}.}"}] | — |
| note | Neither the categorical distribution nor this index theorem is formalized. | Verified: neither a categorical distribution nor this index theorem appears in Mathlib. |
modifiedDifference not exponentialea6d2726d18d
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Distribution of the minimum of exponential random variables","snippet":"is not exponentially distributed, if X 1 , ..., X n do not all have parameter 0"},{"type":"math_alttext","value":"{\\displaystyle \\max\\{X_{1},\\dotsc ,X_{n}\\}}"}] | — |
| note | No negative result on the distribution of differences of exponentials was found. | Verified: no such negative-result lemma appears in Mathlib. |
modifiedJoint moments of order statistics1fde4179f694
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Joint moments of i.i.d. exponential order statistics","snippet":"the joint moment"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\operatorname {E} \\left[X_{(i)}X_{(j)}\\right]&=\\sum _{k=0}^{j-1}{\\frac {1}{(n-k)\\lambda }}\\operatorname {E} \\left[X_{(i)}\\right]+\\operatorname {E} \\left[X_{(i)}^{2}\\right]\\\\&=\\sum _{k=0}^{j-1}{\\frac {1}{(n-k)\\lambda }}\\sum _{k=0}^{i-1}{\\frac {1}{(n-k)\\lambda }}+\\sum _{k=0}^{i-1}{\\frac {1}{((n-k)\\lambda )^{2}}}+\\left(\\sum _{k=0}^{i-1}{\\frac {1}{(n-k)\\lambda }}\\right)^{2}.\\end{aligned}}}"}] | — |
| note | No order-statistic theory for exponential samples was found. | Verified: no order-statistic theory for exponential samples appears in Mathlib. |
modifiedSum of two independent exponentials density06ce66fe3a4e
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Sum of two independent exponential random variables","snippet":"are independent exponential random variables with respective rate parameters"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}f_{Z}(z)&=\\int _{-\\infty }^{\\infty }f_{X_{1}}(x_{1})f_{X_{2}}(z-x_{1})\\,dx_{1}\\\\&=\\int _{0}^{z}\\lambda _{1}e^{-\\lambda _{1}x_{1}}\\lambda _{2}e^{-\\lambda _{2}(z-x_{1})}\\,dx_{1}\\\\&=\\lambda _{1}\\lambda _{2}e^{-\\lambda _{2}z}\\int _{0}^{z}e^{(\\lambda _{2}-\\lambda _{1})x_{1}}\\,dx_{1}\\\\&={\\begin{cases}{\\dfrac {\\lambda _{1}\\lambda _{2}}{\\lambda _{2}-\\lambda _{1}}}\\left(e^{-\\lambda _{1}z}-e^{-\\lambda _{2}z}\\right)&{\\text{ if }}\\lambda _{1}\\neq \\lambda _{2}\\\\[4pt]\\lambda ^{2}ze^{-\\lambda z}&{\\text{ if }}\\lambda _{1}=\\lambda _{2}=\\lambda .\\end{cases}}\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}H(Z)&=1+\\gamma +\\ln \\left({\\frac {\\lambda _{1}-\\lambda _{2}}{\\lambda _{1}\\lambda _{2}}}\\right)+\\psi \\left({\\frac {\\lambda _{1}}{\\lambda _{1}-\\lambda _{2}}}\\right),\\end{aligned}}"}] | — |
| note | No convolution formula for two exponentials with different rates was found. | Verified: no convolution formula for two exponentials appears in Mathlib. |
modifiedEqual rate parameters yield Erlang8d865bc98913
| Field | From #3167 | To #3711 |
|---|
| mathlib.module_note | — | — |
| note | The Gamma distribution (which subsumes Erlang) is defined, but no theorem connects the sum of two exponentials to it. | Verified: `gammaMeasure` (which subsumes Erlang for integer shape) is defined, but no sum-of-two-exponentials identification exists. |
modifiedSum of n i.i.d. exponentialsf14ac443b6cd
| Field | From #3167 | To #3711 |
|---|
| note | The Gamma target distribution exists in Mathlib, but the convolution identity sum of n iid Exp(λ) = Gamma(n,λ) is not proven. | Verified: `gammaMeasure` is defined in Mathlib but the convolution identity `∑ Exp(λ) = Gamma(n,λ)` is not proven. |
modifiedLaplace absolute value6d1b04d50645
| Field | From #3167 | To #3711 |
|---|
| note | The Laplace distribution is not defined in Mathlib (no matching files found). | Verified: no Laplace distribution file exists in `Mathlib/Probability/Distributions/`. |
modifiedUniform to exponential1e1ae3758307
| Field | From #3167 | To #3711 |
|---|
| note | No theorem stating that `-log U/λ ∼ Exp(λ)` for uniform `U` was found. | Verified: no `-log U / λ ∼ Exp(λ)` transformation lemma is present in Mathlib. |
modifiedLog of Paretoa10af8e4bc88
| Field | From #3167 | To #3711 |
|---|
| note | The Pareto distribution is formalized but no transformation result linking it to the exponential is present. | Verified: `paretoMeasure` is defined, but no transformation result linking it to the exponential. |
modifiedLimit of scaled beta57dfb101d902
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Related distributions","snippet":"The exponential distribution is a limit of a scaled beta distribution"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }n\\operatorname {Beta} (1,n)=\\operatorname {Exp} (1).}"}] | — |
| note | Beta distribution exists in Mathlib but no convergence-to-exponential limit theorem was found. | Verified: `betaPDF`/`betaPDFReal` are defined, but no convergence-to-exponential limit theorem is present. |
modifiedSpecial case of Pearson type 342846ec8eec2
| Field | From #3167 | To #3711 |
|---|
| note | Pearson distributions are not present in Mathlib. | Verified: Pearson distributions do not appear in Mathlib. |
modifiedSpecial case of Gamma60ff11574395
| Field | From #3167 | To #3711 |
|---|
| mathlib.decl | ProbabilityTheory.exponentialPDFReal | ProbabilityTheory.expMeasure |
| note | By definition `exponentialPDFReal r x = gammaPDFReal 1 r x` and `expMeasure r = gammaMeasure 1 r`. | Verified: `expMeasure r := gammaMeasure 1 r` and `exponentialPDFReal r x := gammaPDFReal 1 r x` realise this identification definitionally. |
modifiedClosure under scaling57ba18470672
| Field | From #3167 | To #3711 |
|---|
| note | No theorem stating that `kX ∼ Exp(λ/k)` for `X ∼ Exp(λ)` was found. | Verified: no `k · X ∼ Exp(λ/k)` closure lemma appears in Mathlib. |
modifiedBenktander Weibull relationcff87145cd17
| Field | From #3167 | To #3711 |
|---|
| note | The Benktander–Weibull distribution is not defined in Mathlib. | Verified: no Benktander–Weibull distribution appears in Mathlib. |
modifiedExponential of exponential is Paretobf88b8fcacd2
| Field | From #3167 | To #3711 |
|---|
| note | No transformation theorem relating `k·e^X` of an exponential to Pareto was found. | Verified: no `k · e^X ∼ Pareto` transformation lemma is present. |
modifiede to minus lambda X uniform5d5959add503
| Field | From #3167 | To #3711 |
|---|
| note | No such transformation theorem from exponential to uniform was found. | Verified: no `e^{-λX} ∼ U(0,1)` transformation lemma appears in Mathlib. |
modifiede to minus X is Betab32cf6361b98
| Field | From #3167 | To #3711 |
|---|
| note | No `e^{-X} ∼ Beta` transformation result was found in Mathlib. | Verified: no `e^{-X} ∼ Beta` transformation result appears in Mathlib. |
modifiedPower law relation1c0f120a2345
| Field | From #3167 | To #3711 |
|---|
| note | Power-law distributions are not separately formalized. | Verified: no separate power-law distribution appears in Mathlib. |
modifiedGumbel relationa630ed67a185
| Field | From #3167 | To #3711 |
|---|
| note | Gumbel distribution is not present in Mathlib. | Verified: no Gumbel distribution appears in Mathlib. |
modifiedLaplace from difference69dbf2a1f418
| Field | From #3167 | To #3711 |
|---|
| note | Laplace distribution is absent from Mathlib. | Verified: no Laplace distribution exists in Mathlib. |
modifiedMinimum of exponentials relatedb92589c91864
| Field | From #3167 | To #3711 |
|---|
| note | No min-of-exponentials theorem is present in Mathlib. | Verified: no min-of-exponentials theorem appears in Mathlib. |
modifiedDifference of exponentials Laplace0b6a1f7e3c9e
| Field | From #3167 | To #3711 |
|---|
| note | Laplace distribution and this transformation result are not in Mathlib. | Verified: no Laplace distribution nor this transformation appears in Mathlib. |
modifiedChi-squared relationa09861734fbc
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Related distributions","snippet":"X has a chi-squared distribution with 2 degrees of freedom"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Exp} (\\lambda )={\\frac {1}{2\\lambda }}\\operatorname {Exp} \\left({\\frac {1}{2}}\\right)\\sim {\\frac {1}{2\\lambda }}\\chi _{2}^{2}\\Rightarrow \\sum _{i=1}^{n}\\operatorname {Exp} (\\lambda )\\sim {\\frac {1}{2\\lambda }}\\chi _{2n}^{2}}"}] | — |
| note | Chi-squared distribution is not present in Mathlib. | Verified: no chi-squared distribution appears in Mathlib. |
modifiedHoyt from exponential and arcsine051cd51d1160
| Field | From #3167 | To #3711 |
|---|
| note | Neither Hoyt nor arcsine distributions appear in Mathlib's probability distributions. | Verified: neither Hoyt nor arcsine distributions appear in Mathlib's probability distributions. |
modifiedLimit of kappa-exponentialfd0971a40d89
| Field | From #3167 | To #3711 |
|---|
| note | Kappa-exponential distribution is not present in Mathlib. | Verified: no κ-exponential distribution appears in Mathlib. |
modifiedLimit of kappa-Generalized Gamma20e79a064da8
| Field | From #3167 | To #3711 |
|---|
| note | Kappa-generalized Gamma is not present in Mathlib. | Verified: no κ-generalized Gamma distribution appears in Mathlib. |
modifiedLikelihood function22165a563e84
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Parameter estimation","snippet":"The likelihood function for λ, given an independent and identically distributed sample"},{"type":"math_alttext","value":"{\\displaystyle L(\\lambda )=\\prod _{i=1}^{n}\\lambda \\exp(-\\lambda x_{i})=\\lambda ^{n}\\exp \\left(-\\lambda \\sum _{i=1}^{n}x_{i}\\right)=\\lambda ^{n}\\exp \\left(-\\lambda n{\\overline {x}}\\right),}"}] | — |
| note | A general log-likelihood-ratio is formalized but no exponential-distribution-specific likelihood function is. | Verified: general log-likelihood-ratio `llr` exists, but no exponential-specific likelihood function. |
modifiedMaximum likelihood estimator024deeb8b113
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Parameter estimation","snippet":"the maximum likelihood estimate for the rate parameter is"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {\\lambda }}_{\\text{mle}}={\\frac {1}{\\overline {x}}}={\\frac {n}{\\sum _{i}x_{i}}}}"}] | — |
| note | No MLE for the exponential rate parameter is formalized. | Verified: no MLE for the exponential rate parameter is formalized. |
modifiedMLE bias91f882e572b8
| Field | From #3167 | To #3711 |
|---|
| note | Statistical bias of the MLE is not discussed in Mathlib. | Verified: statistical bias of estimators is not developed in Mathlib. |
modifiedBias-corrected MLEd2ff4213560e
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Parameter estimation","snippet":"which yields the bias-corrected maximum likelihood estimator"},{"type":"math_alttext","value":"{\\displaystyle B\\equiv \\operatorname {E} \\left[\\left({\\widehat {\\lambda }}_{\\text{mle}}-\\lambda \\right)\\right]={\\frac {\\lambda }{n-1}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {\\lambda }}_{\\text{mle}}^{*}={\\widehat {\\lambda }}_{\\text{mle}}-B.}"}] | — |
| note | Bias-correction of estimators is not in Mathlib. | Verified: no bias-corrected estimator appears in Mathlib. |
modifiedMSE-minimizing correctionf2908f862897
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Parameter estimation","snippet":"An approximate minimizer of mean squared error"},{"type":"math_alttext","value":"{\\displaystyle {\\widehat {\\lambda }}=\\left({\\frac {n-2}{n}}\\right)\\left({\\frac {1}{\\bar {x}}}\\right)={\\frac {n-2}{\\sum _{i}x_{i}}}}"}] | — |
| note | MSE-minimizing estimator corrections are not in Mathlib. | Verified: no MSE-minimizing correction appears in Mathlib. |
modifiedFisher information756cbc8d527e
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Fisher information","snippet":"The Fisher information , denoted"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {I}}(\\lambda )=\\operatorname {E} \\left[\\left.\\left({\\frac {\\partial }{\\partial \\lambda }}\\log f(x;\\lambda )\\right)^{2}\\right|\\lambda \\right]=\\int \\left({\\frac {\\partial }{\\partial \\lambda }}\\log f(x;\\lambda )\\right)^{2}f(x;\\lambda )\\,dx}"}] | — |
| note | No Fisher information definition is found in Mathlib. | Verified: no `FisherInformation`/`fisherInformation` occurrences under `Mathlib/`. |
modifiedExact confidence interval6ed0948e3c77
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Confidence intervals","snippet":"An exact 100(1 − α)% confidence interval for the rate parameter of an exponential distribution is given by"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {2n}{{\\widehat {\\lambda }}_{\\textrm {mle}}\\chi _{{\\frac {\\alpha }{2}},2n}^{2}}}<{\\frac {1}{\\lambda }}<{\\frac {2n}{{\\widehat {\\lambda }}_{\\textrm {mle}}\\chi _{1-{\\frac {\\alpha }{2}},2n}^{2}}}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {2n{\\overline {x}}}{\\chi _{{\\frac {\\alpha }{2}},2n}^{2}}}<{\\frac {1}{\\lambda }}<{\\frac {2n{\\overline {x}}}{\\chi _{1-{\\frac {\\alpha }{2}},2n}^{2}}}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\lambda _{\\text{lower}}&={\\widehat {\\lambda }}\\left(1-{\\frac {1.96}{\\sqrt {n}}}\\right)\\\\\\lambda _{\\text{upper}}&={\\widehat {\\lambda }}\\left(1+{\\frac {1.96}{\\sqrt {n}}}\\right)\\end{aligned}}"}] | — |
| note | Confidence intervals are not formalized in Mathlib. | Verified: confidence intervals are not developed in Mathlib. |
modifiedNormal approximation CI9399517d4046
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Confidence intervals","snippet":"A simple approximation to the exact interval endpoints can be derived using a normal approximation"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {2n}{{\\widehat {\\lambda }}_{\\textrm {mle}}\\chi _{{\\frac {\\alpha }{2}},2n}^{2}}}<{\\frac {1}{\\lambda }}<{\\frac {2n}{{\\widehat {\\lambda }}_{\\textrm {mle}}\\chi _{1-{\\frac {\\alpha }{2}},2n}^{2}}}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {2n{\\overline {x}}}{\\chi _{{\\frac {\\alpha }{2}},2n}^{2}}}<{\\frac {1}{\\lambda }}<{\\frac {2n{\\overline {x}}}{\\chi _{1-{\\frac {\\alpha }{2}},2n}^{2}}}\\,,"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\lambda _{\\text{lower}}&={\\widehat {\\lambda }}\\left(1-{\\frac {1.96}{\\sqrt {n}}}\\right)\\\\\\lambda _{\\text{upper}}&={\\widehat {\\lambda }}\\left(1+{\\frac {1.96}{\\sqrt {n}}}\\right)\\end{aligned}}}"}] | — |
| note | Normal-approximation CIs are not formalized in Mathlib. | Verified: normal-approximation CIs are not formalized in Mathlib. |
modifiedConjugate gamma prior612992b74981
| Field | From #3167 | To #3711 |
|---|
| note | Bayesian conjugate-prior theory is not present in Mathlib. | Verified: Bayesian conjugate-prior theory is absent from Mathlib. |
modifiedPosterior distribution800d6f5e3e0a
| Field | From #3167 | To #3711 |
|---|
| note | No posterior-distribution derivation appears in Mathlib. | Verified: no posterior-distribution derivation appears in Mathlib. |
modifiedPosterior meanbe9899f59852
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Bayesian inference with a conjugate prior","snippet":"The posterior mean here is"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\alpha +n}{\\beta +n{\\overline {x}}}}.}"}] | — |
| note | No posterior-mean computation for the exponential model exists in Mathlib. | Verified: no posterior-mean computation for the exponential model exists. |
modifiedHaar measure for exponential08cda9873eda
| Field | From #3167 | To #3711 |
|---|
| note | Although Haar measure exists in Mathlib generally, the Bayesian Haar prior for the exponential distribution is not formalized. | Verified: general Haar measure exists in Mathlib, but no exponential-specific Bayesian Haar prior is defined. |
modifiedBayesian prediction with Haar priorebd3336a5ca5
| Field | From #3167 | To #3711 |
|---|
| note | Bayesian predictive distributions are not present in Mathlib. | Verified: Bayesian predictive distributions are not developed in Mathlib. |
modifiedInter-arrival times in Poisson process4b9d023ff5d7
| Field | From #3167 | To #3711 |
|---|
| note | Poisson point process theory and inter-arrival theorems are not in Mathlib. | Verified: only the Poisson PMF (`Mathlib/Probability/Distributions/Poisson/…`) is present — no Poisson point process nor inter-arrival theorem. |
modifiedContinuous counterpart of geometric6546cdfc272d
| Field | From #3167 | To #3711 |
|---|
| note | Both distributions exist (`geometricPMFReal`, `expMeasure`) but no result connects them as continuous/discrete analogues. | Verified: `geometricMeasure` and `expMeasure` exist, but no formal analogy result connects them. |
modifiedPhone calls and radioactive decayf8308b390dc0
| Field | From #3167 | To #3711 |
|---|
| note | Applied examples like phone calls and radioactive decay are not formalized in Mathlib. | Verified: applied physical examples are not formalized in Mathlib. |
modifiedConstant probability per unit lengthb3f94a144949
| Field | From #3167 | To #3711 |
|---|
| note | Applied modelling examples are not formalized in Mathlib. | Verified: applied modelling examples are not formalized in Mathlib. |
modifiedQueuing theory service times92e5e4abe302
| Field | From #3167 | To #3711 |
|---|
| note | Queueing-theory applications are not formalized in Mathlib. | Verified: queueing-theory applications are not formalized in Mathlib. |
modifiedReliability theory bathtub curveb2197829121a
| Field | From #3167 | To #3711 |
|---|
| note | Reliability theory is not formalized in Mathlib. | Verified: reliability theory is not formalized in Mathlib. |
modifiedBarometric formula19be4d2713ae
| Field | From #3167 | To #3711 |
|---|
| note | Barometric/physics examples are not formalized in Mathlib. | Verified: physical/barometric examples are not formalized in Mathlib. |
modifiedHydrology extreme values44065f3a8c08
| Field | From #3167 | To #3711 |
|---|
| note | Hydrology/extreme-value applications are not formalized in Mathlib. | Verified: hydrology/extreme-value applications are not formalized in Mathlib. |
modifiedSurgery duration0002aedabbaa
| Field | From #3167 | To #3711 |
|---|
| note | Operations-research applications are not formalized in Mathlib. | Verified: operations-research applications are not formalized in Mathlib. |
modifiedPlug-in predictive distributionca6310c6baa3
| Field | From #3167 | To #3711 |
|---|
| anchors | [{"section":"Prediction","snippet":"the so-called plug-in distribution, formed by plugging a suitable estimate for the rate parameter"},{"type":"math_alttext","value":"{\\displaystyle p_{\\rm {ML}}(x_{n+1}\\mid x_{1},\\ldots ,x_{n})=\\left({\\frac {1}{\\overline {x}}}\\right)\\exp \\left(-{\\frac {x_{n+1}}{\\overline {x}}}\\right).}"}] | — |
| note | Plug-in predictive distributions are not formalized in Mathlib. | Verified: plug-in predictive distributions are not formalized in Mathlib. |
modifiedCNML predictive superiority1bf2a796fdca
| Field | From #3167 | To #3711 |
|---|
| note | CNML and predictive comparison theorems are not formalized in Mathlib. | Verified: CNML and predictive comparison theorems are not in Mathlib. |
modifiedInverse transform sampling8000ddfd89f9
| Field | From #3167 | To #3711 |
|---|
| note | Inverse transform sampling is not formalized for the exponential distribution in Mathlib. | Verified: no inverse-transform-sampling result for the exponential distribution is in Mathlib. |
modifiedUniform symmetry trickde4b2118ce0f
| Field | From #3167 | To #3711 |
|---|
| note | No theorem stating `1 − U` is uniform on `(0,1)` for uniform `U` was found in `Mathlib/Probability/Distributions/Uniform.lean`. | Verified: no `1 − U` symmetry lemma appears in `Mathlib/Probability/Distributions/Uniform.lean`. |
modifiedStandard deviation equals mean4c284ac1cf16
| Field | From #3167 | To #3711 |
|---|
| note | Direct consequence of Var[X] = 1/λ², but no formalization of variance/standard deviation for `expMeasure` exists. | Verified: neither variance nor standard deviation is computed for `expMeasure` in Mathlib. |
modifiedMemorylessness via complementary CDF8319da320da7
| Field | From #3167 | To #3711 |
|---|
| note | No proof of the memoryless property via the survival function is formalized for `expMeasure`. | Verified: no memoryless-via-survival-function proof is present for `expMeasure`. |
modifiedMinimum via complementary CDF572b663d127f
| Field | From #3167 | To #3711 |
|---|
| note | The complementary-CDF argument for the distribution of the minimum of independent exponentials is not formalized. | Verified: the complementary-CDF argument for the min-of-exponentials theorem is not formalized in Mathlib. |
modifiedMedian-mean inequality for exponential9f0a9caf4e27
| Field | From #3167 | To #3711 |
|---|
| note | Neither the general median-mean inequality nor its exponential-distribution instance is in Mathlib. | Verified: neither the general median-mean inequality nor its exponential instance is in Mathlib. |
modifiedLog-likelihood derivative0dfbacaa05c4
| Field | From #3167 | To #3711 |
|---|
| note | Score function computations for the exponential family are not formalized in Mathlib. | Verified: score-function computations for the exponential family are not formalized in Mathlib. |
modifiedFisher information of rate parameter27f27cce8653
| Field | From #3167 | To #3711 |
|---|
| note | The specific Fisher information I(λ) = 1/λ² for the exponential distribution is not in Mathlib (Fisher information itself is not defined). | Verified: Fisher information itself is not defined in Mathlib, so `I(λ) = 1/λ²` is likewise absent. |
addedSupport on non-negative reals71426712b673
addedSum of n i.i.d. exponentials is Erlang6c130cfe6853