OAI/Combinatorics/TreeEdit/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Binary edit-distance distortion
The nested finite-period and circle-tree constructions independently give the same
lower bound for every sufficiently large length cap, in the unrestricted real ℓ₁
space. The fixed-length conversion theorem applies to all words over any finite
alphabet within the cardinality bound, with width M ^ 2 and length M ^ 3.
This file declares nothing itself. It gathers the 3 imports below, so a file that imports it gets all of them.