Translation TP2 and convolution

This file proves the one-dimensional total-positivity statement behind preservation of log-concavity under convolution. It is adapted to the existing LikelihoodRatio.densityConvolution definition.

def Feige.LikelihoodRatio.TranslationTP2 (f : ℝ → ENNReal) : Prop

Total positivity of order two for the translation kernel of f.

Equations

• Feige.LikelihoodRatio.TranslationTP2 f = ∀ ⦃x₁ x₂ z₁ z₂ : ℝ⦄, x₁ ≤ x₂ → z₁ ≤ z₂ → f (x₁ - z₂) * f (x₂ - z₁) ≤ f (x₁ - z₁) * f (x₂ - z₂)

noncomputable def Feige.LikelihoodRatio.translationKernelComposition (f g : ℝ → ENNReal) (x y : ℝ) : ENNReal

Composition of two nonnegative translation kernels.

Equations

• Feige.LikelihoodRatio.translationKernelComposition f g x y = ∫⁻ (z : ℝ), f (x - z) * g (z - y)

theorem Feige.LikelihoodRatio.measurable_translationKernelComposition {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) : Measurable fun (p : ℝ × ℝ) => translationKernelComposition f g p.1 p.2

theorem Feige.LikelihoodRatio.TranslationTP2.kernelComposition {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) (hfFinite : ∀ (x : ℝ), f x ≠ ⊤) (hgFinite : ∀ (x : ℝ), g x ≠ ⊤) (hfTP2 : TranslationTP2 f) (hgTP2 : TranslationTP2 g) ⦃x₁ x₂ y₁ y₂ : ℝ⦄ : x₁ ≤ x₂ → y₁ ≤ y₂ → translationKernelComposition f g x₁ y₂ * translationKernelComposition f g x₂ y₁ ≤ translationKernelComposition f g x₁ y₁ * translationKernelComposition f g x₂ y₂

Composition of finite-valued measurable translation-TP2 kernels is again TP2.

theorem Feige.LikelihoodRatio.translationKernelComposition_eq_densityConvolution_sub (f g : ℝ → ENNReal) (x y : ℝ) : translationKernelComposition f g x y = densityConvolution g f (x - y)

theorem Feige.LikelihoodRatio.TranslationTP2.convolution {f g : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) (hfFinite : ∀ (x : ℝ), f x ≠ ⊤) (hgFinite : ∀ (x : ℝ), g x ≠ ⊤) (hfTP2 : TranslationTP2 f) (hgTP2 : TranslationTP2 g) : TranslationTP2 (densityConvolution f g)

The current project's density convolution preserves translation TP2.

theorem Feige.LikelihoodRatio.TranslationTP2.fourPointLogConcave {f : ℝ → ENNReal} (hf : TranslationTP2 f) : FourPointLogConcave f

Translation TP2 implies the existing general four-point log-concavity predicate.

theorem Feige.LikelihoodRatio.FourPointLogConcave.translationTP2 {f : ℝ → ENNReal} (hf : FourPointLogConcave f) : TranslationTP2 f

The existing four-point predicate is equivalent to translation TP2.