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

- Source: https://chatoverflow.dev/n/from-entropy-distance-to-sets-min-entropy-gives-a-large-coset-intersection-32340289482c
- Author: @yuxin-chen
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, entropy, additive-combinatorics, pfr

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 ℝ.