WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Student's t-distribution

Revision #1602 → #1804 · back to history

modifiedStudent's t distribution77f264fe7787
FieldFrom #1602To #1804
noteMathlib has Gaussian, Cauchy, Gamma and Beta distributions but no Student's t-distribution.No Student's t-distribution declaration is present in Mathlib (no StudentT/tDistribution under Mathlib/Probability/Distributions).
modifiedCauchy and normal limiting cases68e14c7266f6
FieldFrom #1602To #1804
noteBoth endpoint distributions (Cauchy and Gaussian) are formalized, but the limiting relationship of the t-distribution to them is not.Cauchy and Gaussian endpoint distributions are defined, but the limiting relationship to the (undefined) t-distribution is not formalized.
modifiedLocation-scale form generalizes normal / Bayesian compound9d82edbf1a4a
FieldFrom #1602To #1804
noteNo location-scale t-distribution or compound-distribution-as-t result exists in Mathlib.Mathlib has no location-scale t-distribution or normal/inverse-gamma compound result.
modifiedProbability density functionb19af0767db7
FieldFrom #1602To #1804
anchors[{"section":"Probability density function","snippet":"Student's t distribution has the probability density function (PDF) given by"},{"type":"math_alttext","value":"{\\displaystyle f(t)={\\frac {\\Gamma {\\left({\\frac {\\nu +1}{2}}\\right)}}{{\\sqrt {\\pi \\nu }}\\,\\Gamma {\\left({\\frac {\\nu }{2}}\\right)}}}\\left(1+{\\frac {t^{2}}{\\nu }}\\right)^{-(\\nu +1)/2},}"},{"type":"math_alttext","value":"{\\displaystyle f(t)={\\frac {1}{{\\sqrt {\\nu }}\\,\\mathrm {B} {\\left({\\frac {1}{2}},{\\frac {\\nu }{2}}\\right)}}}\\left(1+{\\frac {t^{2}}{\\nu }}\\right)^{-(\\nu +1)/2},}"}]—
noteThere is no t-distribution PDF in Mathlib (only Cauchy/Gaussian/Beta/Gamma PDFs).No t-distribution PDF appears in Mathlib (only Cauchy/Gaussian/Beta/Gamma PDFs).
modifiedPDF is symmetric and bell-shapedffcbab120f63
FieldFrom #1602To #1804
noteNo t-distribution PDF or symmetry result is present in Mathlib.No t-distribution PDF (or its symmetry) is formalized in Mathlib.
modifiedt distribution approaches normal as df grows00e1c421c5d0
FieldFrom #1602To #1804
noteThe convergence of the t-distribution to the normal is not formalized since the t-distribution is undefined in Mathlib.Convergence of t to normal is not formalized; the t-distribution itself is absent from Mathlib.
modifiedCumulative distribution functioned88bdfed12b
FieldFrom #1602To #1804
noteMathlib has the complete Beta function (Complex.betaIntegral) but no regularized incomplete beta function nor the t-distribution CDF.Mathlib has the complete Beta integral but no regularized incomplete beta function nor a t-distribution CDF.
modifiedAlternative CDF formula via hypergeometric function02fff9fbe6b9
FieldFrom #1602To #1804
noteAn ordinary hypergeometric function exists in Mathlib, but the t-distribution CDF formula is not formalized.An ordinary hypergeometric function exists in Mathlib but no t-distribution CDF formula in terms of it.
modifiedRaw moments of the t distributiondebc8c434880
FieldFrom #1602To #1804
noteNo t-distribution or its moments are defined in Mathlib.Neither the t-distribution nor its raw moments are defined in Mathlib.
modifiedMoments of order ν or higher do not existc137c5ba0783
FieldFrom #1602To #1804
noteNo statement about non-existence of high-order t-distribution moments is in Mathlib.No statement about non-existence of high-order t-distribution moments is present in Mathlib.
modifiedSimplified even-order moments4ab7eb7f5b0f
FieldFrom #1602To #1804
noteReal.Gamma exists but no even-order t-distribution moment simplification is formalized.Real.Gamma is formalized but no even-order t-distribution moment simplification exists in Mathlib.
modifiedt distribution as distribution of test statistic T22712cb6fe84
FieldFrom #1602To #1804
noteThe ratio-of-normal-to-chi construction defining the t-distribution is not in Mathlib (chi-squared distribution is absent).The ratio-of-normal-to-chi construction is absent; Mathlib lacks the chi-squared distribution.
modifiedNoncentral t-distributionc6a958851dec
FieldFrom #1602To #1804
anchors[{"section":"As the distribution of a test statistic","snippet":"This random variable has a noncentral t -distribution with noncentrality parameter μ ."},{"type":"math_alttext","value":"{\\displaystyle (Z+\\mu ){\\sqrt {\\frac {\\nu }{V}}}.}"}]—
noteNo noncentral t-distribution exists in Mathlib.No noncentral t-distribution is defined in Mathlib.
modifiedStandardized sample mean is standard normal9035cf1d4822
FieldFrom #1602To #1804
noteMathlib proves sums and scalar multiples of Gaussian variables are Gaussian, but the standardized sample mean being exactly N(0,1) is not assembled.Mathlib proves sums and scalar multiples of Gaussian variables are Gaussian (HasGaussianLaw.sum/smul), but the standardized sample mean as exactly N(0,1) is not assembled.
modifiedT depends on ν but not μ or σ988761b74b03
FieldFrom #1602To #1804
noteNo formalization of the parameter-independence (pivotal) property of the t-statistic is in Mathlib.No pivotal-quantity parameter-independence result for the t-statistic is in Mathlib.
modifiedt statistic is a pivotal quantity9fd2263e8ec3
FieldFrom #1602To #1804
noteMathlib has no notion of pivotal quantities or the t-statistic.Mathlib has no notion of pivotal quantity or the t-statistic.
modifiedMLE-based statistic is location-scale t distributedb85e9a7aa6a4
FieldFrom #1602To #1804
anchors[{"section":"Sampling distribution of t-statistic","snippet":"This is distributed according to the location-scale t distribution:"},{"type":"math_alttext","value":"{\\displaystyle \\ s_{\\mathsf {ML}}^{2}={\\frac {\\ 1\\ }{n}}\\ \\sum _{i=1}^{n}(x_{i}-{\\bar {x}})^{2}\\ }"},{"type":"math_alttext","value":"{\\displaystyle \\ t_{\\mathsf {ML}}={\\frac {{\\bar {x}}-\\mu }{\\sqrt {s_{\\mathsf {ML}}^{2}/n\\ }}}={\\sqrt {{\\frac {n}{n-1}}\\ }}\\ t~.}"},{"type":"math_alttext","value":"{\\displaystyle t_{\\mathsf {ML}}\\sim \\operatorname {\\ell st} (0,\\ \\tau ^{2}=n/(n-1),\\ n-1)~.}"}]—
noteNo location-scale t-distribution or MLE-statistic distribution result is in Mathlib.No location-scale t-distribution or MLE-based statistic distribution result is in Mathlib.
modifiedCompound of normal with inverse gamma over variance51c47ddcc231
FieldFrom #1602To #1804
noteThe inverse-gamma distribution and the normal/inverse-gamma compounding yielding t are not in Mathlib.Neither the inverse-gamma distribution nor the normal/inverse-gamma compounding result is in Mathlib.
modifiedEquivalent compound with scaled-inverse-chi-squared4e011d61768f
FieldFrom #1602To #1804
noteThe scaled-inverse-chi-squared distribution and this compounding result are absent from Mathlib.Mathlib has no scaled-inverse-chi-squared distribution or this compounding equivalence.
modifiedt distribution as maximum entropy distributioncf79281a39f9
FieldFrom #1602To #1804
noteMathlib has no maximum-entropy characterization machinery nor the t-distribution.Mathlib has no maximum-entropy characterization for the t-distribution.
modifiedNoncentral t distribution5836b216f4b8
FieldFrom #1602To #1804
noteNo noncentral t-distribution exists in Mathlib.No noncentral t-distribution is defined in Mathlib.
modifiedDiscrete Student's t distribution008c8d732ccf
FieldFrom #1602To #1804
anchors[{"section":"In general","snippet":"The discrete Student's t distribution is defined by its probability mass function at r being proportional to:"},{"type":"math_alttext","value":"{\\displaystyle \\prod _{j=1}^{k}{\\frac {1}{(r+j+a)^{2}+b^{2}}}\\quad \\quad r=\\ldots ,-1,0,1,\\ldots ~.}"}]—
noteNo discrete Student's t-distribution exists in Mathlib.No discrete Student's t-distribution is defined in Mathlib.
modifiedSampling via ratio of normal and chi-squared roota6240cccec2c
FieldFrom #1602To #1804
noteThe chi-squared distribution and this ratio-sampling characterization are not in Mathlib.The chi-squared distribution and this ratio-sampling characterization are absent from Mathlib.
modifiedLocation-scale t distribution04c9e361e4a7
FieldFrom #1602To #1804
anchors[{"section":"Location-scale transformation","snippet":"Student's t distribution generalizes to the three parameter location-scale t distribution"},{"type":"math_alttext","value":"{\\displaystyle \\ T\\sim t_{\\nu }\\ }"},{"type":"math_alttext","value":"{\\displaystyle \\ X=\\mu +\\tau \\ T\\ }"},{"type":"math_alttext","value":"{\\displaystyle X\\sim \\operatorname {\\ell st} (\\mu ,\\ \\tau ^{2},\\ \\nu )~.}"}]—
noteThe three-parameter location-scale t-distribution is not in Mathlib.The three-parameter location-scale t-distribution is absent from Mathlib.
modifiedLocation-scale t normal limitc01824b71e04
FieldFrom #1602To #1804
noteThe normal limit of the location-scale t-distribution is not formalized in Mathlib.The normal limit of the location-scale t-distribution is not formalized.
modifiedLocation-scale t with ν=1 is Cauchy2858ee9036d6
FieldFrom #1602To #1804
noteThe Cauchy distribution is formalized, but its identification with the ν=1 location-scale t-distribution is not (the t-distribution is undefined).Cauchy is formalized but its identification with the ν=1 location-scale t-distribution is not (t-distribution undefined).
modifiedStudent's t process588f4f389146
FieldFrom #1602To #1804
noteThe analogous Gaussian process is formalized, but the Student's t process is not (the t-distribution is undefined).The analogous IsGaussianProcess is formalized, but no Student's t process exists in Mathlib.