Revision #2476 → #3112 · back to history
modifiedSimpson's paradoxe742635090e7
| Field | From #2476 | To #3112 |
|---|
| note | No definition of Simpson's paradox appears in Mathlib; grep for `Simpson` returns only unrelated references to Alex Simpson in topology. | Grep for `Simpson` in Mathlib returns only Alex Simpson's convenient-topology work; no definition of Simpson's paradox exists. |
modifiedUC Berkeley gender bias298b311e8142
| Field | From #2476 | To #3112 |
|---|
| note | Real-world dataset examples are not in scope for Mathlib and no formalization exists. | Real-world dataset examples are out of scope for Mathlib; no formalization exists. |
addedParallelogram rule for combined success-rate vectorsb800cd71be34
modifiedCorrelation reversal from lurking confounderd38bc44058c4
| Field | From #2476 | To #3112 |
|---|
| note | Grep for `confounder`/`confounding` returns no hits; no formalization of correlation reversal exists. | Grep for `confound` returns no hits in Mathlib; correlation reversal from a lurking variable is not formalized. |
modifiedQualified Savage sure-thing principle60ab7b3e8ac4
| Field | From #2476 | To #3112 |
|---|
| note | Savage's sure-thing principle is not stated or proved in Mathlib. | Savage's sure-thing principle is not stated or proved in Mathlib (only unrelated `do calculus` comment in manifold docs). |
modifiedBack-door criterion614f6e9b70b6
| Field | From #2476 | To #3112 |
|---|
| kind | theorem | definition |
| note | Grep for `back.?door` returns no hits; Pearl's back-door criterion is not formalized in Mathlib. | Grep for `back.?door` returns no hits in Mathlib; Pearl's back-door criterion is not formalized. |
| provenance | ai | ai-moderated |
modifiedNoncollapsibility87fb07d91003
| Field | From #2476 | To #3112 |
|---|
| note | Noncollapsibility of association measures across strata is not defined in Mathlib. | Grep for `noncollapsib` returns no hits; noncollapsibility of association measures is not defined in Mathlib. |