AddDissociated.boringEnergy_le

lemma AddDissociated.boringEnergy_le [MeasurableSpace G] [DiscreteMeasurableSpace G] [DecidableEq G]    [Finite G] {s : Finset G} (hs : AddDissociated (s : Set G)) (n : ℕ) :    boringEnergy n s ≤ changConst ^ n * n ^ n * #s ^ n := by  cases nonempty_fintype G  obtain rfl | hn := eq_or_ne n 0  · simp  calc    _ = (‖dft 𝟭_[(s : Set G)]‖ₙ_[↑(2 * n)] ^ (2 * n) : ℝ) := by rw [cLpNorm_dft_indicator_one_pow]    _ ≤ (4 * rexp 2⁻¹ * sqrt ↑(2 * n) * ‖dft 𝟭_[(s : Set G)]‖ₙ_[2]) ^ (2 * n) := by        gcongr        refine rudin_ineq (le_mul_of_one_le_right zero_le_two <| Nat.one_le_iff_ne_zero.2 hn)          (dft 𝟭_[(s : Set G), ℂ]) ?_        rwa [cft_dft, support_comp_eq_preimage, Set.support_indicator_one, Set.preimage_comp,          Set.neg_preimage, addDissociated_neg, AddEquiv.addDissociated_preimage]    _ = _ := by        simp_rw [mul_pow, pow_mul, cL2Norm_dft_indicator_one]        rw [← exp_nsmul, sq_sqrt (by positivity), sq_sqrt (by positivity)]        simp_rw [← mul_pow]        simp [changConst]        ring_nf