Documentation

Mathlib.Data.List.EditDistance.Bounds

Lower bounds for Levenshtein distances #

We show that there is some suffix L' of L such that the Levenshtein distance from L' to M gives a lower bound for the Levenshtein distance from L to m :: M.

This allows us to use the intermediate steps of a Levenshtein distance calculation to produce lower bounds on the final result.

theorem suffixLevenshtein_minimum_le_levenshtein_cons {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (y : β) (ys : List β) :
(↑(suffixLevenshtein C xs ys)).minimum (levenshtein C xs (y :: ys))
theorem le_suffixLevenshtein_cons_minimum {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (y : β) (ys : List β) :
(↑(suffixLevenshtein C xs ys)).minimum (↑(suffixLevenshtein C xs (y :: ys))).minimum
theorem le_suffixLevenshtein_append_minimum {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (ys₁ : List β) (ys₂ : List β) :
(↑(suffixLevenshtein C xs ys₂)).minimum (↑(suffixLevenshtein C xs (ys₁ ++ ys₂))).minimum
theorem suffixLevenshtein_minimum_le_levenshtein_append {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (ys₁ : List β) (ys₂ : List β) :
(↑(suffixLevenshtein C xs ys₂)).minimum (levenshtein C xs (ys₁ ++ ys₂))
theorem le_levenshtein_cons {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (y : β) (ys : List β) :
∃ (xs' : List α), xs' <:+ xs levenshtein C xs' ys levenshtein C xs (y :: ys)
theorem le_levenshtein_append {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : Levenshtein.Cost α β δ} [CanonicallyLinearOrderedAddCommMonoid δ] (xs : List α) (ys₁ : List β) (ys₂ : List β) :
∃ (xs' : List α), xs' <:+ xs levenshtein C xs' ys₂ levenshtein C xs (ys₁ ++ ys₂)