Probability laws of signed scaled exponentials

This file identifies the explicit one-sided densities with pushforwards of a rate-one exponential. It is the first bridge from the original product of exponential coordinates in dirichletK to the finite convolution law used by the TP2 proof.

theorem Feige.LikelihoodRatio.instIsProbabilityMeasureRealExpMeasureOfNat_leanPool : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.expMeasure 1)

theorem Feige.LikelihoodRatio.expMeasure_inv_eq_withDensity_rightExponentialDensity {a : ℝ} (ha : 0 < a) : ProbabilityTheory.expMeasure a⁻¹ = MeasureTheory.volume.withDensity (rightExponentialDensity a)

theorem Feige.LikelihoodRatio.map_mul_expMeasure_one {a : ℝ} (ha : 0 < a) : MeasureTheory.Measure.map (fun (x : ℝ) => a * x) (ProbabilityTheory.expMeasure 1) = MeasureTheory.volume.withDensity (rightExponentialDensity a)

Scaling a rate-one exponential by a > 0 gives the density of aE.

theorem Feige.LikelihoodRatio.map_neg_withDensity (f : ℝ → ENNReal) : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (MeasureTheory.volume.withDensity f) = MeasureTheory.volume.withDensity fun (x : ℝ) => f (-x)

Reflection transports a density by precomposition with negation.

theorem Feige.LikelihoodRatio.map_neg_mul_expMeasure_one {b : ℝ} (hb : 0 < b) : MeasureTheory.Measure.map (fun (x : ℝ) => -(b * x)) (ProbabilityTheory.expMeasure 1) = MeasureTheory.volume.withDensity (leftExponentialDensity b)

The reflected pushforward is the density of -bE.

theorem Feige.LikelihoodRatio.SignedExpFactor.map_expMeasure_one (F : SignedExpFactor) : MeasureTheory.Measure.map (fun (x : ℝ) => match F.direction with | ExpDirection.positive => F.scale * x | ExpDirection.negative => -(F.scale * x)) (ProbabilityTheory.expMeasure 1) = MeasureTheory.volume.withDensity F.density

Every signed factor density is the law of its signed scale times a rate-one exponential.

noncomputable def Feige.LikelihoodRatio.SignedExpFactor.sourceLaw (F : SignedExpFactor) : MeasureTheory.Measure ℝ

The pushforward law of one signed factor.

Equations

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

theorem Feige.LikelihoodRatio.SignedExpFactor.sourceLaw_eq_withDensity (F : SignedExpFactor) : F.sourceLaw = MeasureTheory.volume.withDensity F.density

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

An explicit independent-sum construction of the distinguished exponential and every signed factor. Convolution is the pushforward of the product law under addition, so this is an actual random-sum law rather than merely a density recursion.

Equations

• Feige.LikelihoodRatio.finiteSignedExpSumSourceMeasure [] = MeasureTheory.Measure.map (fun (x : ℝ) => x) (ProbabilityTheory.expMeasure 1)
• Feige.LikelihoodRatio.finiteSignedExpSumSourceMeasure (F :: Fs) = F.sourceLaw.conv (Feige.LikelihoodRatio.finiteSignedExpSumSourceMeasure Fs)

theorem Feige.LikelihoodRatio.finiteSignedExpSumSourceMeasure_eq (Fs : List SignedExpFactor) : finiteSignedExpSumSourceMeasure Fs = finiteSignedExpSumMeasure Fs