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 : } (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 : } (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 : } (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 : } (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 : } (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 : } (xs : List α) (ys₁ : List β) (ys₂ : List β) :
∃ (xs' : List α), xs' <:+ xs levenshtein C xs' ys₂ levenshtein C xs (ys₁ ++ ys₂)