Likelihood-ratio comparison for exponential convolutions

This file formalizes the four-point and double-integral parts of the local exponential transfer step used in the proof of Theorem 2.1. We use an ℝ≥0∞-valued density so that Tonelli and monotone integration require no auxiliary integrability assumptions.

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

The one-dimensional four-point form of log-concavity.

For nonnegative functions on the line this is the exact multiplicative inequality needed below. Ordinary log-concave densities with convex support satisfy this property by concavity of log f.

Equations

• Feige.LikelihoodRatio.FourPointLogConcave f = ∀ ⦃r p q s : ℝ⦄, r ≤ p → p ≤ q → r ≤ s → s ≤ q → p + s = r + q → f r * f q ≤ f p * f s

theorem Feige.LikelihoodRatio.four_point_exponential_shifts {f : ℝ → ENNReal} (hf : FourPointLogConcave f) {a b x y s t : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hxy : y ≤ x) (hs : 0 ≤ s) (ht : 0 ≤ t) : f (x + b * t) * f (y - a * s) ≤ f (x - a * s) * f (y + b * t)

The geometric specialization of the four-point inequality used in the likelihood-ratio comparison.

noncomputable def Feige.LikelihoodRatio.expWeight (s : ℝ) : ENNReal

The exponential convolution weight.

Equations

• Feige.LikelihoodRatio.expWeight s = ENNReal.ofReal (Real.exp (-s))

theorem Feige.LikelihoodRatio.measurable_expWeight : Measurable expWeight

noncomputable def Feige.LikelihoodRatio.fPlus (f : ℝ → ENNReal) (a x : ℝ) : ENNReal

The positive-shift density f₊, expressed as a nonnegative integral.

Equations

• Feige.LikelihoodRatio.fPlus f a x = ∫⁻ (s : ℝ) in Set.Ici 0, f (x - a * s) * Feige.LikelihoodRatio.expWeight s

noncomputable def Feige.LikelihoodRatio.fMinus (f : ℝ → ENNReal) (b x : ℝ) : ENNReal

The negative-shift density f₋, expressed as a nonnegative integral.

Equations

• Feige.LikelihoodRatio.fMinus f b x = ∫⁻ (t : ℝ) in Set.Ici 0, f (x + b * t) * Feige.LikelihoodRatio.expWeight t

theorem Feige.LikelihoodRatio.fPlus_mul_fMinus_mono {f : ℝ → ENNReal} (hfmeas : Measurable f) (hflc : FourPointLogConcave f) {a b x y : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hxy : y ≤ x) : fMinus f b x * fPlus f a y ≤ fPlus f a x * fMinus f b y

Monotone likelihood-ratio inequality for the two shift densities.

The proof expands both products as double nonnegative integrals and applies the four-point inequality pointwise. Because all functions are ℝ≥0∞-valued, Tonelli is unconditional.

theorem Feige.LikelihoodRatio.measurable_fPlus {f : ℝ → ENNReal} (hf : Measurable f) (a : ℝ) : Measurable (fPlus f a)

Measurability of the positive exponential convolution.

theorem Feige.LikelihoodRatio.measurable_fMinus {f : ℝ → ENNReal} (hf : Measurable f) (b : ℝ) : Measurable (fMinus f b)

Measurability of the negative exponential convolution.

noncomputable def Feige.LikelihoodRatio.uIntegral (g : ℝ → ENNReal) (d : ℝ) : ENNReal

The lower-tail transfer functional u for a nonnegative density g.

Equations

• Feige.LikelihoodRatio.uIntegral g d = ∫⁻ (x : ℝ) in Set.Ici 0, g x * ENNReal.ofReal (Real.exp (-x / d))

noncomputable def Feige.LikelihoodRatio.vIntegral (g : ℝ → ENNReal) (c : ℝ) : ENNReal

The upper-tail transfer functional v for a nonnegative density g.

Equations

• Feige.LikelihoodRatio.vIntegral g c = ∫⁻ (y : ℝ) in Set.Iio 0, g y * ENNReal.ofReal (Real.exp (y / c))

theorem Feige.LikelihoodRatio.uMinus_mul_vPlus_le {f : ℝ → ENNReal} (hfmeas : Measurable f) (hflc : FourPointLogConcave f) {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : uIntegral (fMinus f b) d * vIntegral (fPlus f a) c ≤ uIntegral (fPlus f a) d * vIntegral (fMinus f b) c

Integrating the likelihood-ratio comparison against the two exponential weights gives u₋ v₊ ≤ u₊ v₋.

theorem Feige.LikelihoodRatio.theta_le_theta_of_cross {uPlus uMinus vPlus vMinus : ℝ} (hwPlus : 0 < uPlus + vPlus) (hwMinus : 0 < uMinus + vMinus) (hcross : uMinus * vPlus ≤ uPlus * vMinus) : uMinus / (uMinus + vMinus) ≤ uPlus / (uPlus + vPlus)

Algebraic bridge from the cross-product comparison to monotonicity of θ = u / (u + v). This real-valued form is convenient after converting finite probability integrals from ℝ≥0∞.