theorem Newton.integral_norm_eq_toReal_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} (hf : MeasureTheory.Integrable f μ) : ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Relate the integral of the norm of an integrable function with the corresponding lintegral.

theorem Newton.minkowski_integral_inequality {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {E : Type u_3} [NormedAddCommGroup E] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [NormedSpace ℝ E] (p : ENNReal) (hp : 1 ≤ p) (hp_ne_top : p ≠ ⊤) (F : α → β → E) (hF : MeasureTheory.AEStronglyMeasurable (Function.uncurry F) (μ.prod ν)) (hF_prod : MeasureTheory.Integrable (Function.uncurry F) (μ.prod ν)) (hF_int : ∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun (x : α) => F x y) μ) (hF_memLp : ∀ᵐ (y : β) ∂ν, MeasureTheory.MemLp (fun (x : α) => F x y) p μ) (hF_norm : MeasureTheory.Integrable (fun (y : β) => (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal) ν) : MeasureTheory.eLpNorm (fun (x : α) => ∫ (y : β), F x y ∂ν) p μ ≤ ENNReal.ofReal (∫ (y : β), (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal ∂ν)

Minkowski's integral inequality (general form with eLpNorm).

For 1 ≤ p < ∞ and measurable F : α × β → E, ‖∫ F(·, y) dν(y)‖{L^p(μ)} ≤ ∫ ‖F(·, y)‖{L^p(μ)} dν(y)

This is the key inequality for proving Young's inequality for convolution.

theorem Newton.convolution_kernel_aestronglyMeasurable {G : Type u_4} [NormedAddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] (f g : G → ℂ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (q : G × G) => f (q.1 - q.2) * g q.2) (μ.prod μ)

Almost everywhere measurability of the convolution kernel produced from L^p data. This lemma packages the hypotheses needed to apply Minkowski's integral inequality in the Young inequality arguments.

theorem Newton.convolution_kernel_integrable {G : Type u_4} [NormedAddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] (f g : G → ℂ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : MeasureTheory.Integrable (fun (q : G × G) => f (q.1 - q.2) * g q.2) (μ.prod μ)

Integrability of the convolution kernel assuming the factors themselves are integrable. This is the basic input needed for the convolution estimates below.