theorem cLpNorm_cconv_le_cLpNorm_cdconv {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) : ‖f ∗ₙ f‖ₙ_[↑n] ≤ ‖f ○ₙ f‖ₙ_[↑n]

theorem dLpNorm_conv_le_dLpNorm_dconv {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) : ‖f ∗ f‖_[↑n] ≤ ‖f ○ f‖_[↑n]

theorem cLpNorm_cconv_le_cLpNorm_cdconv' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℝ) : ‖f ∗ₙ f‖ₙ_[↑n] ≤ ‖f ○ₙ f‖ₙ_[↑n]

theorem dLpNorm_conv_le_dLpNorm_dconv' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℝ) : ‖f ∗ f‖_[↑n] ≤ ‖f ○ f‖_[↑n]