dLpNorm_ddconv_le_dLpNorm_dddconv

lemma dLpNorm_ddconv_le_dLpNorm_dddconv (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) ?_  have h := pow_le_pow_left₀ (by positivity) (cLpNorm_conv_le_cLpNorm_dconv hn₀ hn f) n  rw [conv_eq_smul_ddconv, dconv_eq_smul_dddconv] at h  have h' : (Fintype.card G : ℝ)⁻¹ * (Fintype.card G : ℝ)⁻¹ ^ n * ‖f ∗ᵈ f‖_[n] ^ n ≤      (Fintype.card G : ℝ)⁻¹ * (Fintype.card G : ℝ)⁻¹ ^ n * ‖f ○ᵈ f‖_[n] ^ n := by    simpa [cLpNorm_pow_eq_card_inv_mul_dLpNorm_pow hn₀, dLpNorm_nnqsmul, mul_pow,      mul_assoc, mul_left_comm, mul_comm] using h  have hpos : 0 < (Fintype.card G : ℝ)⁻¹ * (Fintype.card G : ℝ)⁻¹ ^ n := by positivity  nlinarith