cLpNorm_conv_le_cLpNorm_dconv

lemma cLpNorm_conv_le_cLpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) :    ‖f ∗ f‖ₙ_[n] ≤ ‖f ○ f‖ₙ_[n] := by  refine le_of_pow_le_pow_left₀ hn₀ (by positivity) ?_  obtain ⟨k, rfl⟩ := hn.two_dvd  simp only [ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hn₀  refine Complex.le_of_eq_sum_of_eq_sum_norm (fun ψ : (Fin k → AddChar G ℂ) × (Fin k → AddChar G ℂ)    ↦ conj (∏ i, cft f (ψ.1 i) ^ 2) * (∏ i, cft f (ψ.2 i) ^ 2) * 𝔼 x, (∑ i, ψ.2 i - ∑ i, ψ.1 i) x)    univ (by norm_cast; positivity) ?_ ?_  · push_cast    rw [← cft_inversion' (f ∗ f), cLpNorm_two_mul_sum_pow hn₀]    simp_rw [cft_conv_apply, ← sq, Fintype.sum_prod_type, mul_expect, AddChar.sub_apply]    simp [mul_mul_mul_comm, mul_comm, map_neg_eq_conj, prod_mul_distrib]  · push_cast    rw [← cft_inversion' (f ○ f), cLpNorm_two_mul_sum_pow hn₀]    simp_rw [cft_dconv_apply, Complex.mul_conj', Fintype.sum_prod_type, mul_expect]    congr 1 with ψ    congr 1 with φ    simp only [Pi.smul_apply, smul_eq_mul, map_mul, map_pow, Complex.conj_ofReal, prod_mul_distrib,      mul_mul_mul_comm, ← mul_expect, map_prod, AddChar.sub_apply, AddChar.coe_sum,      Finset.prod_apply, norm_mul, norm_prod, norm_pow, RCLike.norm_conj, Complex.ofReal_mul,      Complex.ofReal_prod, Complex.ofReal_pow]    congr 1    calc      𝔼 x, (∏ i, conj (ψ i x)) * ∏ i, φ i x = 𝔼 x, (∑ i, φ i - ∑ i, ψ i) x := by        simp [map_neg_eq_conj, mul_comm, AddChar.sub_apply]      _ = ‖𝔼 x, (∑ i, φ i - ∑ i, ψ i) x‖ := by simp [expect_eq_ite, apply_ite]      _ = ‖𝔼 x, (∏ i, φ i x) * ∏ i, (ψ i) (-x)‖ := by simp [map_neg_eq_conj, AddChar.sub_apply]