Revision #1971 → #2387 · back to history
modifiedStandard deviation as square root of variance19781b484b3e
| Field | From #1971 | To #2387 |
|---|
| note | No `stdDev`/`standardDeviation` declaration exists in Mathlib; only `ProbabilityTheory.variance` is defined (loogle for `"stdDev"` returned zero hits). | No `stdDev`/`standardDeviation` declaration exists in Mathlib; only `ProbabilityTheory.variance` is defined. |
addedVariance as average of squared deviations from the mean9e1c4df53173
addedStandard error of the mean equals σ/√Nc9a8f3f07079
addedPareto distribution has mean but no SD198fd5d379a7
modifiedCauchy distribution has no SD4dd8f30fbad9
| Field | From #1971 | To #2387 |
|---|
| note | Mathlib has no Cauchy distribution definition (loogle for `cauchy`+`Distribution` returned zero hits) and no statement about non-existence of its moments. | Mathlib has no Cauchy distribution definition and no statement about non-existence of its moments. |
modifiedSD of the log-normal distribution8961951a176c
| Field | From #1971 | To #2387 |
|---|
| note | Log-normal distribution is not defined in Mathlib (loogle for `logNormal` returned zero hits). | Log-normal distribution is not defined in Mathlib. |
modifiedSampling distribution is scaled chi7e9a42e89709
| Field | From #1971 | To #2387 |
|---|
| note | The chi and chi-square distributions are not defined in Mathlib (loogle for `chiSquared` returned zero hits). | The chi and chi-square distributions are not defined in Mathlib. |
modifiedConfidence interval for sampled SDbe4046e104d9
| Field | From #1971 | To #2387 |
|---|
| anchor.snippet | where [MATH] is the p -th quantile of the chi-square distribution | is the p -th quantile of the chi-square distribution with k degrees of freedom |
| 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). | — |
modifiedMean absolute deviation (alternative)67d20b55eaf3
| Field | From #1971 | To #2387 |
|---|
| note | No `meanAbsoluteDeviation` declaration is present in Mathlib (loogle returned zero hits). | No `meanAbsoluteDeviation` declaration is present in Mathlib. |
modifiedCentral limit theorem45e5eaedb4a9
| Field | From #1971 | To #2387 |
|---|
| note | No central limit theorem declaration was found in Mathlib (loogle for `centralLimit` returned zero hits). | No central limit theorem declaration was found in Mathlib. |
addedNormal cumulative distribution function58ccf51c3d9d
modifiedCoefficient of variation2248a67f138e
| Field | From #1971 | To #2387 |
|---|
| note | No `coefficientOfVariation` definition exists in Mathlib (loogle returned zero hits). | No `coefficientOfVariation` definition exists in Mathlib. |
modifiedWeighted running calculation12c77fe8fd0d
| Field | From #1971 | To #2387 |
|---|
| anchor.snippet | When the values [MATH] are weighted with unequal weights | the power sums s 0 , s 1 , s 2 are each computed as |
| 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. | — |
modifiedAverage absolute deviation (alternative to SD)bc1f170a2795
| Field | From #1971 | To #2387 |
|---|
| note | The average/mean absolute deviation is not defined in Mathlib (loogle returned zero hits). | The average/mean absolute deviation is not defined in Mathlib. |