Revision #1587 → #1971 · back to history
modifiedStandard deviation as square root of variance19781b484b3e
| Field | From #1587 | To #1971 |
|---|
| note | No `stdDev`/`standardDeviation` declaration exists in Mathlib; only `ProbabilityTheory.variance` is defined. | No `stdDev`/`standardDeviation` declaration exists in Mathlib; only `ProbabilityTheory.variance` is defined (loogle for `"stdDev"` returned zero hits). |
modifiedPopulation SD of grades of eight students95f1417f0a11
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Population standard deviation of grades of eight students","snippet":"Suppose that the entire population of interest is eight students in a particular class"},{"type":"math_alttext","value":"{\\displaystyle 2,\\ 4,\\ 4,\\ 4,\\ 5,\\ 5,\\ 7,\\ 9.}"}] | — |
modifiedStandard deviation of a random variable2407d7c2fa76
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Definition of population values","snippet":"Let μ be the expected value (the average) of a random variable X with probability density function f"},{"type":"math_alttext","value":"{\\displaystyle \\mu \\equiv \\operatorname {\\mathbb {E} } [X]=\\int _{-\\infty }^{+\\infty }x\\,f(x)\\,{\\mathrm {d} }x.}"},{"type":"math_alttext","value":"{\\displaystyle \\sigma \\equiv {\\sqrt {\\operatorname {\\mathbb {E} } \\left[\\left(X-\\mu \\right)^{2}\\right]}}={\\sqrt {\\int _{-\\infty }^{+\\infty }\\left(x-\\mu \\right)^{2}f(x)\\ {\\mathrm {d} }x\\;}}\\ ,}"}] | — |
addedCauchy distribution has no SD4dd8f30fbad9
modifiedSD of a discrete random variable (weighted)8690ddc9dbee
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Discrete random variable","snippet":"If, instead of having equal probabilities, the values have different probabilities"},{"type":"math_alttext","value":"{\\displaystyle \\sigma ={\\sqrt {\\sum _{i=1}^{N}p_{i}\\left(x_{i}-\\mu \\right)^{2}\\;}}\\ ,~~{\\text{ where }}~~\\mu \\equiv \\sum _{i=1}^{N}p_{i}x_{i}\\,.}"}] | — |
modifiedSD of a continuous random variable7c160227a076
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Continuous random variable","snippet":"The standard deviation of a continuous real-valued random variable X with probability density function"},{"type":"math_alttext","value":"{\\displaystyle \\sigma ={\\sqrt {\\int _{\\mathbf {X} }\\left(x-\\mu \\right)^{2}\\,p(x)\\,{\\mathrm {d} }x}}\\,,~~{\\text{ where }}~~\\mu \\equiv \\int _{\\mathbf {X} }x\\,p(x)\\,{\\mathrm {d} }x\\,,}"}] | — |
modifiedSD of the log-normal distribution8961951a176c
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Continuous random variable","snippet":"in the case of the log-normal distribution with parameters"},{"type":"math_alttext","value":"{\\displaystyle {\\sqrt {\\left(e^{\\sigma ^{2}}-1\\right)\\ e^{2\\mu +\\sigma ^{2}}}}\\,.}"}] | — |
| note | Log-normal distribution is not defined in Mathlib. | Log-normal distribution is not defined in Mathlib (loogle for `logNormal` returned zero hits). |
modifiedUncorrected sample standard deviation059d4ed5d253
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Uncorrected sample standard deviation","snippet":"This estimator, denoted by s N , is known as the uncorrected sample standard deviation"},{"type":"math_alttext","value":"{\\displaystyle s_{N}={\\sqrt {{\\frac {1}{N}}\\sum _{i=1}^{N}\\left(x_{i}-{\\bar {x}}\\right)^{2}}},}"}] | — |
modifiedConsistency of uncorrected sample SDe008eccb68ac
| Field | From #1587 | To #1971 |
|---|
| note | The strong law of large numbers is in Mathlib (`ProbabilityTheory.strong_law_ae`) but consistency of the SD estimator is not stated. | The strong law of large numbers is in Mathlib but consistency of the SD estimator is not stated. |
modifiedCorrected sample standard deviationf062770b4742
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Corrected sample standard deviation","snippet":"yielding the corrected sample standard deviation, denoted by s"},{"type":"math_alttext","value":"{\\displaystyle s={\\sqrt {{\\frac {1}{N-1}}\\sum _{i=1}^{N}\\left(x_{i}-{\\bar {x}}\\right)^{2}}}.}"}] | — |
modifiedUnbiasedness of s² with Bessel's correction385c54dc4430
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Corrected sample standard deviation","snippet":"An unbiased estimator for the variance is given by applying Bessel's correction"},{"type":"math_alttext","value":"{\\displaystyle s^{2}={\\frac {1}{N-1}}\\sum _{i=1}^{N}\\left(x_{i}-{\\bar {x}}\\right)^{2}.}"}] | — |
addedJensen's inequality forces downward bias in s9469b3f8a5fc
modifiedUnbiased sample SD via correction factor2b68872f58a9
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Unbiased sample standard deviation","snippet":"For the normal distribution, an unbiased estimator is given by"},{"type":"math_alttext","value":"{\\displaystyle c_{4}(N)\\,=\\,{\\sqrt {\\frac {2}{N-1}}}\\,\\,\\,{\\frac {\\Gamma {\\left({\\frac {N}{2}}\\right)}}{\\Gamma {\\left({\\frac {N-1}{2}}\\right)}}}.}"}] | — |
modifiedSampling distribution is scaled chi7e9a42e89709
| Field | From #1587 | To #1971 |
|---|
| note | The chi and chi-square distributions are not defined in Mathlib. | The chi and chi-square distributions are not defined in Mathlib (loogle for `chiSquared` returned zero hits). |
modifiedApproximation replacing N−1 with N−1.5643d41487b03
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Unbiased sample standard deviation","snippet":"An approximation can be given by replacing N − 1 with N − 1.5"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {\\sigma }}={\\sqrt {{\\frac {1}{N-1.5}}\\sum _{i=1}^{N}\\left(x_{i}-{\\bar {x}}\\right)^{2}}},}"}] | — |
modifiedConfidence interval for sampled SDbe4046e104d9
| Field | From #1587 | To #1971 |
|---|
| moderation_flag | — | Anchor snippet contains '[MATH]' literal; ideally should be replaced with text actually present in extracted prose (kept verbatim to honor the preserve-id rule). |
| provenance | ai | ai-moderated |
modifiedRange bound on standard deviationacb000b0db9e
| Field | From #1587 | To #1971 |
|---|
| mathlib.decl | — | ProbabilityTheory.variance_le_sq_of_bounded |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Probability.Moments.Variance |
| note | Although `variance_le_sq_of_bounded` bounds variance for bounded RVs, the sample-range bound on sample SD is not stated. | Popoviciu's inequality `variance_le_sq_of_bounded` bounds variance by `((b-a)/2)^2` for bounded RVs, the variance analogue of the sample-range SD bound. |
| status | not_formalized | partial |
modifiedLocation invariance and scaling of SD85663c4656cf
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Identities and mathematical properties","snippet":"The standard deviation is invariant under changes in location , and scales directly with the scale of the random variable"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sigma (c)&=0\\\\\\sigma (X+c)&=\\sigma (X),\\\\\\sigma (cX)&=|c|\\sigma (X).\\end{aligned}}}"}] | — |
addedMean absolute deviation (alternative)67d20b55eaf3
modifiedCentral limit theorem45e5eaedb4a9
| Field | From #1587 | To #1971 |
|---|
| note | No central limit theorem declaration was found in Mathlib (only the strong law of large numbers). | No central limit theorem declaration was found in Mathlib (loogle for `centralLimit` returned zero hits). |
modifiedCoefficient of variation2248a67f138e
| Field | From #1587 | To #1971 |
|---|
| note | No `coefficientOfVariation` definition exists in Mathlib. | No `coefficientOfVariation` definition exists in Mathlib (loogle returned zero hits). |
modifiedStandard deviation of the mean (SDOM)bfe24d7d83f4
| Field | From #1587 | To #1971 |
|---|
| mathlib.decl | — | ProbabilityTheory.IndepFun.variance_sum |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Probability.Moments.Variance |
| note | Mathlib has `IndepFun.variance_sum` for the variance of an i.i.d. sum but does not state the σ/√N SDOM formula. | `IndepFun.variance_sum` gives the variance of an independent sum but the σ/√N SDOM formula is not stated. |
| status | not_formalized | partial |
modifiedWeighted running calculation12c77fe8fd0d
| Field | From #1587 | To #1971 |
|---|
| moderation_flag | — | Anchor snippet contains '[MATH]' literal; preserved verbatim to honor the id but should be re-anchored on a non-[MATH] substring in future. |
| provenance | ai | ai-moderated |
modifiedStandard deviation index (SDI)527d0dafca1b
| Field | From #1587 | To #1971 |
|---|
| anchors | [{"section":"Standard deviation index","snippet":"The standard deviation index (SDI) is used in external quality assessments"},{"type":"math_alttext","value":"{\\displaystyle {\\text{SDI}}={\\frac {{\\text{Laboratory mean}}-{\\text{Consensus group mean}}}{\\text{Consensus group standard deviation}}}.}"}] | — |
addedAverage absolute deviation (alternative to SD)bc1f170a2795