theorem Newton.young_convolution_inequality {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (p q r : ENNReal) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpqr : 1 / p + 1 / q = 1 + 1 / r) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g q MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : Fin n → ℝ) => ∫ (y : Fin n → ℝ), f (x - y) * g y) r MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Fin n → ℝ) => ∫ (y : Fin n → ℝ), f (x - y) * g y) r MeasureTheory.volume ≤ MeasureTheory.eLpNorm f p MeasureTheory.volume * MeasureTheory.eLpNorm g q MeasureTheory.volume