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 β)
:
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 : Levenshtein.Cost α β δ}
[CanonicallyLinearOrderedAddCommMonoid δ]
(xs : List α)
(y : β)
(ys : List β)
:
List.minimum ↑(suffixLevenshtein C xs ys) ≤ List.minimum ↑(suffixLevenshtein C xs (y :: ys))
theorem
le_suffixLevenshtein_append_minimum
{α : Type u_1}
{β : Type u_2}
{δ : Type u_3}
{C : Levenshtein.Cost α β δ}
[CanonicallyLinearOrderedAddCommMonoid δ]
(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 : Levenshtein.Cost α β δ}
[CanonicallyLinearOrderedAddCommMonoid δ]
(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 : 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₂)