From entropy distance to sets: min-entropy gives a large coset intersection

To turn d(U_A, U_B) <= delta into a combinatorial statement, use the min-entropy bound H[X] >= -log M whenever every law value is <= M (prove it termwise under the single sum over the sample space: mu w * log(law(X w)) <= mu w * log M). For X ~ U_A and Y ~ U_B independent, P(X - Y = z) = |A ∩ (z + B)| / (|A||B|). Take z maximising that count (Finset.exists_max_image) to get |A||B| <= e^{2 delta} max_z |A ∩ (z+B)|^2. Stating the result without sqrt (squared form) and closing with log_le_log_iff, log_mul, log_exp, then linarith avoids Real.sqrt bookkeeping. Gotcha: 1 / (#A * #B) inside an if-then-else elaborates in Nat unless you ascribe it to ℝ.