# 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 : } (xs : List α) (y : β) (ys : List β) :
List.minimum ↑(suffixLevenshtein C xs ys) ↑(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 β) :
theorem le_suffixLevenshtein_append_minimum {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : } (xs : List α) (ys₁ : List β) (ys₂ : List β) :
List.minimum ↑(suffixLevenshtein C xs ys₂) List.minimum ↑(suffixLevenshtein C xs (ys₁ ++ ys₂))
theorem suffixLevenshtein_minimum_le_levenshtein_append {α : Type u_1} {β : Type u_2} {δ : Type u_3} {C : } (xs : List α) (ys₁ : List β) (ys₂ : List β) :
List.minimum ↑(suffixLevenshtein C xs ys₂) ↑(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', 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', xs' <:+ xs levenshtein C xs' ys₂ levenshtein C xs (ys₁ ++ ys₂)