WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Student's t-distribution

Revision #2313 → #2962 · back to history

modifiedStandardized sample mean is standard normal9035cf1d4822
FieldFrom #2313To #2962
mathlib.declProbabilityTheory.HasGaussianLaw.sumProbabilityTheory.iIndepFun.hasGaussianLaw_sum
mathlib.moduleMathlib.Probability.Distributions.Gaussian.HasGaussianLaw.BasicMathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
noteMathlib 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.Mathlib proves that a finite sum of independent Gaussian variables has a Gaussian law (iIndepFun.hasGaussianLaw_sum), but the standardization to exactly N(0,1) as a sampling-distribution statement is not assembled.
addedV has chi-squared distribution with ν degrees of freedome71fae17ca01
addedZ and V are independentd3d9085c502d
addedPDF via beta function representationdbd0a698a565
addedInfinite ν limit is normal distribution67bb8e8d4d04
addedBox–Muller extension for sampling teb0f87027cd4
addedt distribution as Pearson type IVf4e418afeab4