Revision #2735 → #3218 · back to history
addedSobolev space7e6fc204741c
addedHausdorff measurea4e01ca44867
addedHausdorff dimension32965f392992
addedCayley graphdb1f8fee332c
modifiedLevenshtein distance6f2012bf2fef
| Field | From #2735 | To #3218 |
|---|
| note | No `Levenshtein`/edit-distance file exists in Mathlib (grep for `levenshtein`/`EditDistance` returns no matches). | No Levenshtein/edit-distance declaration exists in Mathlib; `decl_exists` and grep for `Levenshtein`/`EditDistance` return no matches. |
| provenance | ai | ai-moderated |
addedWasserstein distance1919edd8d76c
modifiedSnowflake of a metric1b57c218abe6
| Field | From #2735 | To #3218 |
|---|
| mathlib.decl | Metric.Snowflaking | — |
| mathlib.match_kind | special_case | — |
| mathlib.module | Mathlib.Topology.MetricSpace.Snowflaking | — |
| note | `Metric.Snowflaking X α` formalizes the power-of-d snowflake; the general concave-f version is not stated. | No general `Snowflaking` / concave-composition metric construction was located in Mathlib. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
addedNormed vector spacef118755fcb78
addedAngular distance on a sphere2d9dedb1828a
addedHyperbolic plane687110f68ccf