Revision #2847 → #3974 · back to history
modifiedAkaike information criterion (AIC)330eb289b0a4
| Field | From #2847 | To #3974 |
|---|
| note | No AIC or model-selection-criterion definition exists in Mathlib (grep for 'Akaike'/'AIC' returns nothing in Mathlib/). | Grep for 'Akaike'/'AIC' returns no hits in Mathlib/. |
modifiedAIC value of a model8b59c06c3b74
| Field | From #2847 | To #3974 |
|---|
| note | The formula AIC = 2k - 2 ln L̂ is absent from Mathlib; Mathlib has KL divergence and log-likelihood-ratio infra but no AIC formula. | The formula AIC = 2k − 2 ln L̂ is absent from Mathlib; no likelihood-based model-selection API exists. |
addedKullback–Leibler divergencefdc117f5c521
modifiedRelative likelihood of model i2ea9586eee15
| Field | From #2847 | To #3974 |
|---|
| note | The relative-likelihood transform exp((AICmin - AICi)/2) has no Mathlib counterpart. | The relative-likelihood transform exp((AICmin − AICi)/2) has no Mathlib counterpart. |
modifiedProbability interpretation of relative likelihood469c7a9ff834
| Field | From #2847 | To #3974 |
|---|
| note | Not formalized; depends on AIC and the underlying decision-theoretic interpretation absent from Mathlib. | Depends on AIC and a decision-theoretic interpretation, none of which is in Mathlib. |
modifiedThree candidate models example731538361acb
| Field | From #2847 | To #3974 |
|---|
| note | Numerical AIC worked example with no formal statistics counterpart in Mathlib. | Numerical AIC worked example with no formal counterpart in Mathlib. |
addedLog-normal distribution (transformed density)b5db940aee3f
modifiedBIC penalty vs AIC penalty72a3b9b6ed9e
| Field | From #2847 | To #3974 |
|---|
| note | Neither AIC nor BIC (Bayesian Information Criterion) is defined in Mathlib. | Neither AIC nor BIC is defined in Mathlib. |
modifiedAsymptotic equivalence of AIC and Cpf0d7eb576c32
| Field | From #2847 | To #3974 |
|---|
| note | Mallows's Cp statistic is not defined in Mathlib (grep for 'Mallows' returns no results). | Grep for 'Mallows' in Mathlib returns no hits, so Cp and this equivalence are not formalized. |