theorem Newton.inner_integral_bound {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (p q r : ENNReal) (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hp_ne_top : p ≠ ⊤) (hq_ne_top : q ≠ ⊤) (hr_ne_top : r ≠ ⊤) (hpqr : 1 / p + 1 / q = 1 + 1 / r) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g q MeasureTheory.volume) (x : Fin n → ℝ) : ∫⁻ (y : Fin n → ℝ), ↑‖f y‖₊ * ↑‖g (x - y)‖₊ ≤ (∫⁻ (y : Fin n → ℝ), ↑‖f y‖₊ ^ p.toReal * ↑‖g (x - y)‖₊ ^ q.toReal) ^ (1 / r.toReal) * MeasureTheory.eLpNorm f p MeasureTheory.volume ^ (1 - p / r).toReal * MeasureTheory.eLpNorm g q MeasureTheory.volume ^ (1 - q / r).toReal

Inner integral bound for fixed x

theorem Newton.young_convolution_r_ne_top {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (p q r : ENNReal) (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hp_ne_top : p ≠ ⊤) (hq_ne_top : q ≠ ⊤) (hr_ne_top : r ≠ ⊤) (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