expander_mixing_lemma_tight