Log-concavity of scaled one-sided exponential densities

The common part in each insertion edge is a convolution of positive and negative scaled exponentials. This file verifies the four-point log-concavity condition for each individual one-sided exponential factor.

noncomputable def Feige.LikelihoodRatio.rightExponentialDensity (a x : ℝ) : ENNReal

Density of aE, up to the canonical Lebesgue interpretation.

Equations

• Feige.LikelihoodRatio.rightExponentialDensity a x = if 0 ≤ x then ENNReal.ofReal (Real.exp (-x / a) / a) else 0

theorem Feige.LikelihoodRatio.measurable_rightExponentialDensity (a : ℝ) : Measurable (rightExponentialDensity a)

theorem Feige.LikelihoodRatio.fourPointLogConcave_rightExponentialDensity {a : ℝ} (ha : 0 < a) : FourPointLogConcave (rightExponentialDensity a)

A positive scaled exponential density satisfies the multiplicative four-point form of log-concavity, including its zero extension outside its half-line support.

theorem Feige.LikelihoodRatio.FourPointLogConcave.reflect {f : ℝ → ENNReal} (hf : FourPointLogConcave f) : FourPointLogConcave fun (x : ℝ) => f (-x)

Reflection of a four-point log-concave function is again four-point log-concave.

noncomputable def Feige.LikelihoodRatio.leftExponentialDensity (b x : ℝ) : ENNReal

Density of -bE.

Equations

• Feige.LikelihoodRatio.leftExponentialDensity b x = Feige.LikelihoodRatio.rightExponentialDensity b (-x)

theorem Feige.LikelihoodRatio.measurable_leftExponentialDensity (b : ℝ) : Measurable (leftExponentialDensity b)

theorem Feige.LikelihoodRatio.fourPointLogConcave_leftExponentialDensity {b : ℝ} (hb : 0 < b) : FourPointLogConcave (leftExponentialDensity b)