The convolution characterisation of 3AP-free sets

theorem ThreeAPFree.wInner_one_mu_conv_mu_mu_two_smul_mu {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] {s : Finset G} (hG : Odd (Fintype.card G)) (hs : ThreeAPFree ↑s) : RCLike.wInner 1 (mu s ∗ mu s) (mu (Finset.image (fun (x : G) => 2 • x) s)) = (↑s.card ^ 2)⁻¹