Nonnegative density convolution

The closure of log-concavity under convolution is the one-dimensional case of the Prékopa theorem. Mathlib does not currently provide that theorem. This file establishes its measure-theoretic convolution layer; the required one-dimensional closure is proved by the TP2/Cauchy--Binet argument in Feige.TranslationTP2 and instantiated for the insertion common laws in Feige.FiniteSignedExp.

noncomputable def Feige.LikelihoodRatio.densityConvolution (f g : ℝ → ENNReal) : ℝ → ENNReal

Lebesgue convolution of two nonnegative densities on the line.

Equations

• Feige.LikelihoodRatio.densityConvolution f g = MeasureTheory.lconvolution f g MeasureTheory.volume

theorem Feige.LikelihoodRatio.densityConvolution_apply (f g : ℝ → ENNReal) (x : ℝ) : densityConvolution f g x = ∫⁻ (y : ℝ), f y * g (x - y)

theorem Feige.LikelihoodRatio.measurable_densityConvolution {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) : Measurable (densityConvolution f g)

theorem Feige.LikelihoodRatio.densityConvolution_assoc {f g h : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) : densityConvolution (densityConvolution f g) h = densityConvolution f (densityConvolution g h)

theorem Feige.LikelihoodRatio.lintegral_densityConvolution {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : ℝ), densityConvolution f g x = (∫⁻ (x : ℝ), f x) * ∫⁻ (x : ℝ), g x

The integral of a nonnegative convolution is the product of the two integrals. No finiteness assumptions are needed.

theorem Feige.LikelihoodRatio.lintegral_densityConvolution_eq_one {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) (hf_one : ∫⁻ (x : ℝ), f x = 1) (hg_one : ∫⁻ (x : ℝ), g x = 1) : ∫⁻ (x : ℝ), densityConvolution f g x = 1

Convolution preserves normalization of nonnegative densities.

theorem Feige.LikelihoodRatio.conv_withDensity_eq_withDensity_densityConvolution {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) : (MeasureTheory.volume.withDensity f).conv (MeasureTheory.volume.withDensity g) = MeasureTheory.volume.withDensity (densityConvolution f g)

Convolving densities agrees with convolving their absolutely continuous measures.