Finite signed exponential sums

The common part of a genuine insertion edge is a distinguished rate-one exponential together with finitely many positive or negative scaled rate-one exponentials. This file gives that law an explicit normalized density and derives its four-point log-concavity from translation TP2 closure under convolution.

theorem Feige.LikelihoodRatio.rightExponentialDensity_eq_exponentialPDF {a : ℝ} (ha : 0 < a) : rightExponentialDensity a = ProbabilityTheory.exponentialPDF a⁻¹

theorem Feige.LikelihoodRatio.lintegral_rightExponentialDensity {a : ℝ} (ha : 0 < a) : ∫⁻ (x : ℝ), rightExponentialDensity a x = 1

theorem Feige.LikelihoodRatio.lintegral_leftExponentialDensity {b : ℝ} (hb : 0 < b) : ∫⁻ (x : ℝ), leftExponentialDensity b x = 1

theorem Feige.LikelihoodRatio.rightExponentialDensity_ne_top (a x : ℝ) : rightExponentialDensity a x ≠ ⊤

theorem Feige.LikelihoodRatio.leftExponentialDensity_ne_top (b x : ℝ) : leftExponentialDensity b x ≠ ⊤

theorem Feige.LikelihoodRatio.rightExponentialDensity_le_rate {a : ℝ} (ha : 0 < a) (x : ℝ) : rightExponentialDensity a x ≤ ENNReal.ofReal a⁻¹

theorem Feige.LikelihoodRatio.leftExponentialDensity_le_rate {b : ℝ} (hb : 0 < b) (x : ℝ) : leftExponentialDensity b x ≤ ENNReal.ofReal b⁻¹

inductive Feige.LikelihoodRatio.ExpDirection : Type

The sign of one nondegenerate scaled exponential summand.

• positive : ExpDirection
• negative : ExpDirection

@[instance_reducible]

instance Feige.LikelihoodRatio.instDecidableEqExpDirection : DecidableEq ExpDirection

Equations

• Feige.LikelihoodRatio.instDecidableEqExpDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Feige.LikelihoodRatio.SignedExpFactor : Type

One positive or negative scaled rate-one exponential summand.

• direction : ExpDirection

  Whether the exponential summand is positive or negative.

• scale : ℝ

  The positive scale of the summand.

• scale_pos : 0 < self.scale

noncomputable def Feige.LikelihoodRatio.SignedExpFactor.density (F : SignedExpFactor) : ℝ → ENNReal

The one-sided exponential density associated with a signed factor.

Equations

• One or more equations did not get rendered due to their size.

theorem Feige.LikelihoodRatio.SignedExpFactor.measurable_density (F : SignedExpFactor) : Measurable F.density

theorem Feige.LikelihoodRatio.SignedExpFactor.density_ne_top (F : SignedExpFactor) (x : ℝ) : F.density x ≠ ⊤

theorem Feige.LikelihoodRatio.SignedExpFactor.lintegral_density (F : SignedExpFactor) : ∫⁻ (x : ℝ), F.density x = 1

theorem Feige.LikelihoodRatio.SignedExpFactor.density_le_rate (F : SignedExpFactor) (x : ℝ) : F.density x ≤ ENNReal.ofReal F.scale⁻¹

theorem Feige.LikelihoodRatio.SignedExpFactor.translationTP2_density (F : SignedExpFactor) : TranslationTP2 F.density

def Feige.LikelihoodRatio.finiteSignedExpSumDensity : List SignedExpFactor → ℝ → ENNReal

Density of a distinguished rate-one exponential convolved with finitely many signed scaled exponentials.

Equations

• Feige.LikelihoodRatio.finiteSignedExpSumDensity [] = Feige.LikelihoodRatio.rightExponentialDensity 1
• Feige.LikelihoodRatio.finiteSignedExpSumDensity (F :: Fs) = Feige.LikelihoodRatio.densityConvolution F.density (Feige.LikelihoodRatio.finiteSignedExpSumDensity Fs)

theorem Feige.LikelihoodRatio.measurable_finiteSignedExpSumDensity (Fs : List SignedExpFactor) : Measurable (finiteSignedExpSumDensity Fs)

theorem Feige.LikelihoodRatio.lintegral_finiteSignedExpSumDensity (Fs : List SignedExpFactor) : ∫⁻ (x : ℝ), finiteSignedExpSumDensity Fs x = 1

theorem Feige.LikelihoodRatio.densityConvolution_le_of_left_bound {f g : ℝ → ENNReal} (hg : Measurable g) {C : ENNReal} (hfC : ∀ (x : ℝ), f x ≤ C) (hgInt : ∫⁻ (x : ℝ), g x = 1) (x : ℝ) : densityConvolution f g x ≤ C

theorem Feige.LikelihoodRatio.finiteSignedExpSumDensity_ne_top (Fs : List SignedExpFactor) (x : ℝ) : finiteSignedExpSumDensity Fs x ≠ ⊤

theorem Feige.LikelihoodRatio.translationTP2_finiteSignedExpSumDensity (Fs : List SignedExpFactor) : TranslationTP2 (finiteSignedExpSumDensity Fs)

Finite signed exponential convolution remains translation TP2.

theorem Feige.LikelihoodRatio.fourPointLogConcave_finiteSignedExpSumDensity (Fs : List SignedExpFactor) : FourPointLogConcave (finiteSignedExpSumDensity Fs)

The explicit four-point log-concavity needed by the local exponential transfer step.

instance Feige.LikelihoodRatio.instIsProbabilityMeasureWithDensityFiniteSignedExpSum (Fs : List SignedExpFactor) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.volume.withDensity (finiteSignedExpSumDensity Fs))

def Feige.LikelihoodRatio.finiteSignedExpSumMeasure : List SignedExpFactor → MeasureTheory.Measure ℝ

The same finite signed-exponential law constructed directly by successive convolution of its absolutely continuous factor laws.

Equations

• Feige.LikelihoodRatio.finiteSignedExpSumMeasure [] = MeasureTheory.volume.withDensity (Feige.LikelihoodRatio.rightExponentialDensity 1)
• Feige.LikelihoodRatio.finiteSignedExpSumMeasure (F :: Fs) = (MeasureTheory.volume.withDensity F.density).conv (Feige.LikelihoodRatio.finiteSignedExpSumMeasure Fs)

theorem Feige.LikelihoodRatio.finiteSignedExpSumMeasure_eq_withDensity (Fs : List SignedExpFactor) : finiteSignedExpSumMeasure Fs = MeasureTheory.volume.withDensity (finiteSignedExpSumDensity Fs)

The recursively convolved law has exactly the explicit TP2 density.

instance Feige.LikelihoodRatio.instIsProbabilityMeasureFiniteSignedExpSumMeasure (Fs : List SignedExpFactor) : MeasureTheory.IsProbabilityMeasure (finiteSignedExpSumMeasure Fs)