Revision #1165 → #2558 · back to history
modifiedStatistical distances2042463802ec
| Field | From #1165 | To #2558 |
|---|
| mathlib.decl | klDiv | InformationTheory.klDiv |
| provenance | ai | ai-moderated |
modifiedRelative entropy (Kullback–Leibler divergence)f91329c9caaf
| Field | From #1165 | To #2558 |
|---|
| mathlib.decl | klDiv | InformationTheory.klDiv |
| provenance | ai | ai-moderated |
modifiedHausdorff distance is a metric on compact subsets22bae2a93f11
| Field | From #1165 | To #2558 |
|---|
| mathlib.decl | TopologicalSpace.NonemptyCompacts.instMetricSpace | Metric.NonemptyCompacts.instMetricSpace |
| provenance | ai | ai-moderated |