OAI/Combinatorics/EditApproximation/BasicResults.lean

Almost-linear approximation of edit distance

A uniform binary randomized approximation scheme attains success probability at least two thirds, returns zero on equal strings, uses almost-linear expected work for each fixed binary accuracy, and has polynomial space on every outcome. Finite Bernstein concentration discharges the hypotheses of its conditional accuracy and work bounds.