Randomising by a function of dissociated support

This file proves that a function from a finite abelian group can be randomised by a function of dissociated support.

Precisely, for G a finite abelian group and two functions c : AddChar G ℂ → ℝ and d : AddChar G ℂ → ℝ such that {ψ | d ψ ≠ 0} is dissociated, the product of the c ψ over ψ is the same as the average over a of the product of the c ψ + Re (d ψ * ψ a).

theorem AddDissociated.randomisation {G : Type u_1} [Fintype G] [AddCommGroup G] (c : AddChar G ℂ → ℝ) (d : AddChar G ℂ → ℂ) (hcd : AddDissociated {ψ : AddChar G ℂ | d ψ ≠ 0}) : (Finset.univ.expect fun (a : G) => ∏ ψ : AddChar G ℂ, (c ψ + (d ψ * ψ a).re)) = ∏ ψ : AddChar G ℂ, c ψ

One can randomise by a function of dissociated support.