Revision #1593 → #2469 · back to history
modifiedStatistical significancecd6b209be778
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for 'significance' and 'hypothesis test' in Mathlib returned no relevant hits; statistical inference is not formalized. |
| status | — | not_formalized |
modifiedSignificance level3ae0699d8eaa
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No significance level / hypothesis testing infrastructure found in Mathlib. |
| status | — | not_formalized |
modifiedp-valuea6b19f949efc
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for pValue / p_value returned no statistical hits; p-values are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedStatistically significant result criterionb452677f51cd
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The p ≤ α decision rule requires unformalized hypothesis-testing machinery. |
| status | — | not_formalized |
modifiedSignificance level as false positive probability39bbd5f48b0a
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of α as type-I-error threshold in Mathlib. |
| status | — | not_formalized |
modifiedConfidence level97dd4f06dc86
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for 'confidence level' and 'confidence interval' returned no hits. |
| status | — | not_formalized |
modifiedNull hypothesis987a5aefaff2
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for 'null hypothesis' in Mathlib returned no files. |
| status | — | not_formalized |
modifiedp-value (hypothesis testing)fd4e1a3f7ce5
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Same result as the lead p-value entry; p-values are not defined in Mathlib. |
| status | — | not_formalized |
modified5% significance level allocation21d53722c3bf
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Type I error and its conditional-probability characterization are not in Mathlib. |
| status | — | not_formalized |
modifiedHiggs boson 5σ criterion6d7ecd0b7569
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Field-specific example of a significance threshold; not a Mathlib-formalizable statement. |
| status | — | not_formalized |
modifiedEffect size7f93b3dec243
| Field | From #1593 | To #2469 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for 'effect size' returned no hits in Mathlib. |
| status | — | not_formalized |
addedType I error (false positive)4cd36356b438
addedOne-tailed vs two-tailed test rejection region22efa5f60ef6
addedRejection region as fraction of sampling distributionf672230cbb7b
addedGenome-wide association study significance threshold9130f8767f7f
addedConfidence level formula γ = 1 − α3018a43b58f8