The convolution characterisation of 3AP-free sets

theorem ThreeAPFree.wInner_one_mu_ddconv_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) : ⟪mu s ∗ᵈ mu s, mu (Finset.image (fun (x : G) => 2 • x) s)⟫_[ℝ] = (↑s.card ^ 2)⁻¹