Jensen's inequality for convolution with a probability kernel

Let ρ be a probability kernel on a measurable additive group with a right-invariant measure μ, that is ρ ≥ 0 almost everywhere and ∫ ρ = 1. Convolution with ρ averages the translates of a function, so a convex integrand of the norm cannot increase. Precisely, let Φ : ℝ → ℝ be convex and monotone on [0, ∞). Then at every point

Φ(‖(ρ ⋆ g)(x)‖) ≤ ∫ ρ(t) Φ(‖g(x - t)‖) dt

(ConvexOn.ofReal_map_norm_convolution_le_lintegral), and integrating in x,

∫ Φ(‖ρ ⋆ g‖) ≤ ∫ Φ(‖g‖)

(ConvexOn.lintegral_ofReal_map_norm_convolution_le). Both sides are extended nonnegative integrals of ENNReal.ofReal ∘ Φ, so no integrability of g or of Φ(‖g‖) is assumed and the bound is informative exactly when its right side is finite. For a mollifier ρ and the weak gradient g = ∇u of a Sobolev function this is the bound ∫ Φ(‖∇(ρ ⋆ u)‖) ≤ ∫ Φ(‖∇u‖) that makes mollification compatible with de la Vallée Poussin's criterion (MeasureTheory.Integrable.exists_convexOn_superlinear_integrable).

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, Chapter 4 (mollification of Sobolev functions).

theorem ConvexOn.ofReal_map_norm_convolution_le_lintegral {G : Type u_1} {F : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] {Φ : ℝ → ℝ} {ρ : G → ℝ} (hΦ : ConvexOn ℝ (Set.Ici 0) Φ) (hΦm : MonotoneOn Φ (Set.Ici 0)) (hρ0 : 0 ≤ᵐ[μ] ρ) (hρ1 : ∫ (t : G), ρ t ∂μ = 1) {g : G → F} (hg : MeasureTheory.AEStronglyMeasurable g μ) (x : G) : ENNReal.ofReal (Φ ‖MeasureTheory.convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖) ≤ ∫⁻ (t : G), ENNReal.ofReal (ρ t) * ENNReal.ofReal (Φ ‖g (x - t)‖) ∂μ

Jensen's inequality for convolution. If Φ is convex and monotone on [0, ∞) and ρ is a probability kernel, then at every point Φ(‖(ρ ⋆ g)(x)‖) ≤ ∫ ρ(t) Φ(‖g(x - t)‖) dt, in extended nonnegative form.

theorem ConvexOn.lintegral_ofReal_map_norm_convolution_le {G : Type u_1} {F : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] {Φ : ℝ → ℝ} {ρ : G → ℝ} (hΦ : ConvexOn ℝ (Set.Ici 0) Φ) (hΦm : MonotoneOn Φ (Set.Ici 0)) (hρ0 : 0 ≤ᵐ[μ] ρ) (hρ1 : ∫ (t : G), ρ t ∂μ = 1) {g : G → F} (hg : MeasureTheory.AEStronglyMeasurable g μ) : ∫⁻ (x : G), ENNReal.ofReal (Φ ‖MeasureTheory.convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖) ∂μ ≤ ∫⁻ (x : G), ENNReal.ofReal (Φ ‖g x‖) ∂μ

Convolution with a probability kernel does not increase a convex integral of the norm. If Φ is convex and monotone on [0, ∞) and ρ is a probability kernel, then ∫ Φ(‖ρ ⋆ g‖) ≤ ∫ Φ(‖g‖), in extended nonnegative form.