Revision #2951 → #3417 · back to history
8eca45c66486| Field | From #2951 | To #3417 |
|---|---|---|
| mathlib.match_kind | exact | close |
| note | The (log-)likelihood ratio is defined in Mathlib via Radon–Nikodym derivatives. | Mathlib defines the log-likelihood ratio `llr` via Radon–Nikodym derivatives; the (non-log) likelihood ratio is `rnDeriv` itself. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
a35920b98d9e5a504fefc93a