Young's Lᵖ inequality for a probability kernel

This file collects the reusable convolution machinery feeding the weak-gradient Morrey embedding. The headline result eLpNorm_convolution_le is a specialised Young inequality: convolving an Lᵖ function against a non-negative kernel of unit mass does not increase its Lᵖ seminorm. The classical proof uses the (currently absent) Minkowski integral inequality; we instead derive the pointwise bound directly from Hölder's inequality in ℝ≥0∞ and close with Tonelli, so no Minkowski inequality is required.

The mollifier kernel φ.normed volume is the intended instance (non-negative by ContDiffBump.nonneg_normed, unit mass by ContDiffBump.integral_normed), and the restricted corollary eLpNorm_convolution_restrict_le is the form consumed downstream.

The second result tendsto_eLpNorm_convolution_sub records the Lᵖ convergence of the mollifications h ⋆ ρ_ε to h as the bump radii shrink. It is proved by a density 3ε argument: approximate h in Lᵖ by a smooth compactly supported w (MeasureTheory.MemLp.exist_eLpNorm_sub_le), control the tail (h - w) ⋆ ρ_ε by the Young bound above, and drive the middle term w ⋆ ρ_ε - w to zero using the uniform convergence supplied by ContDiffBump.dist_normed_convolution_le on the fixed compact support. No Lᵖ-continuity of translation is required, and the argument is valid along an arbitrary filter.

theorem EllipticPdes.Embedding.eLpNorm_convolution_le {d : ℕ} {p : ℝ} (hp : 1 ≤ p) {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρ0 : 0 ≤ ρ) (hρm : MeasureTheory.AEStronglyMeasurable ρ MeasureTheory.volume) (hρ1 : ∫ (y : EuclideanSpace ℝ (Fin d)), ρ y = 1) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal p) MeasureTheory.volume) : MeasureTheory.eLpNorm (MeasureTheory.convolution h ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) (ENNReal.ofReal p) MeasureTheory.volume ≤ MeasureTheory.eLpNorm h (ENNReal.ofReal p) MeasureTheory.volume

Young's Lᵖ inequality for a probability kernel. For 1 ≤ p, a non-negative kernel ρ with unit mass ∫ ρ = 1, and h ∈ Lᵖ, the convolution against ρ does not increase the Lᵖ seminorm: ‖h ⋆ ρ‖_{Lᵖ} ≤ ‖h‖_{Lᵖ}. Proved by the pointwise Hölder bound |(h ⋆ ρ)(x)|^p ≤ ∫ |h(t)|^p ρ(x - t) together with Tonelli and unit mass; no Minkowski integral inequality is required.

theorem EllipticPdes.Embedding.eLpNorm_convolution_restrict_le {d : ℕ} {p : ℝ} (hp : 1 ≤ p) {ρ : EuclideanSpace ℝ (Fin d) → ℝ} (hρ0 : 0 ≤ ρ) (hρm : MeasureTheory.AEStronglyMeasurable ρ MeasureTheory.volume) (hρ1 : ∫ (y : EuclideanSpace ℝ (Fin d)), ρ y = 1) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal p) MeasureTheory.volume) (s : Set (EuclideanSpace ℝ (Fin d))) : MeasureTheory.eLpNorm (MeasureTheory.convolution h ρ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) (ENNReal.ofReal p) (MeasureTheory.volume.restrict s) ≤ MeasureTheory.eLpNorm h (ENNReal.ofReal p) MeasureTheory.volume

Young bound restricted to a set s on the left, upper-bounded by the full Lᵖ norm.

theorem EllipticPdes.Embedding.tendsto_eLpNorm_convolution_sub {d : ℕ} {p : ℝ} (hp : 1 ≤ p) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal p) MeasureTheory.volume) {ι : Type u_1} {l : Filter ι} {φ : ι → ContDiffBump 0} {K : ℝ} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (_hK : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (MeasureTheory.convolution h ((φ i).normed MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume - h) (ENNReal.ofReal p) MeasureTheory.volume) l (nhds 0)

Lᵖ convergence of mollifications. For 1 ≤ p, an Lᵖ function h, and a family of normalised bumps whose outer radii tend to 0 (with a bounded inner/outer ratio), the mollifications h ⋆ ρ_ε converge to h in Lᵖ. Proved by a density 3ε argument: approximate h in Lᵖ by a smooth compactly supported w (MeasureTheory.MemLp.exist_eLpNorm_sub_le), bound the tail (h - w) ⋆ ρ_ε by eLpNorm_convolution_le, and send w ⋆ ρ_ε - w to zero with tendsto_eLpNorm_bump_convolution_sub. No Lᵖ-continuity of translation is used.