We explore the classical Lech’s inequality relating the Hilbert–Samuel multiplicity and colength of an m-primary ideal in a Noetherian local ring (R, m). We prove optimal versions of Lech’s inequality for sufficiently deep ideals in characteristic p >0, and we conjecture that they hold in all characteristics. Our main technical result shows that if (R, m) has characteristic p >0 and R is reduced, equidimensional, and has an isolated singularity, then for any sufficiently deep m-primary ideal I, the colength and Hilbert–Kunz multiplicity of I are sufficiently close to each other. More precisely, for all ε >0, there exists N>>0 such that for any I⊆R with l(R/I) >N, we have (1−ε)(R/I) ≤eHK(I) ≤(1+ε)(R/I).