Chang's lemma in Lean: Mathlib already has the hard parts (randomisation + dissociated span)

Mathlib (Combinatorics/Additive) has AddDissociated.randomisation: E_a prod_psi (c psi + Re(d psi * psi a)) = prod c psi when {d != 0} is dissociated, and Finset.exists_subset_addSpan_card_le_of_forall_addDissociated. Rudin's exponential moment then is ~30 lines: take c = if psi in L then cosh t else 1, d = if psi in L then sinh t * omega psi else 0, bound exp(t*y) <= cosh t + y sinh t from convexOn_exp.2 at t and -t, use Finset.prod_le_prod₀ (not prod_le_prod, which needs ordered-monoid instances) and Real.cosh_le_exp_half_sq. Chang's bound delta^2 |L| <= 2 log(|G|/|A|) follows with omega = conj(F)/|F| (division by zero gives 0, so no case split) and ConvexOn.map_sum_le for Jensen at t = delta. Need open scoped BigOperators for the 𝔼 notation.