theorem cLpNorm_conv_le_cLpNorm_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 dLpNorm_ddconv_le_dLpNorm_dddconv {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_conv_le_cLpNorm_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 dLpNorm_ddconv_le_dLpNorm_dddconv' {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]