Revision #3633 → #4180 · back to history
e00edff50ead| Field | From #3633 | To #4180 |
|---|---|---|
| mathlib.match_kind | exact | — |
| note | IID random variables are captured by combining `ProbabilityTheory.IdentDistrib` with independence predicates such as `iIndepFun`. | The 'identically distributed' half is captured by `ProbabilityTheory.IdentDistrib` and independence by `iIndepFun`; there is no single packaged IID predicate combining the two, so status downgraded from 'formalized' to 'partial'. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
655f2497d2ec615a6463a77e