Exponential tilts of the Gaussian, gamma, Poisson, and binomial laws

When exp (t * x) is μ-integrable, tilting a law μ on ℝ or ℕ by exp (t * x) gives the probability law with density exp (t * x) / ∫ exp (t * y) ∂μ with respect to μ; otherwise Measure.tilted returns the zero measure. Each of the four families below is closed under this operation, and the tilt acts on the parameters as follows.

• TauCeti.Probability.gaussianReal_tilted_mul: the Gaussian N(m, v) tilts to N(m + v t, v), including the point mass at variance zero, with the pointwise density identity TauCeti.Probability.gaussianPDFReal_mul_exp_div_mgf, and TauCeti.Probability.setIntegral_exp_mul_gaussianReal reads this off as a weighted set integral;
• TauCeti.Probability.gammaMeasure_tilted_mul: the gamma law of shape a and rate r tilts to rate r - t, for t < r, which is exactly the range where the tilt is a probability law;
• TauCeti.Probability.poissonMeasure_tilted_mul: the native Poisson law of rate r tilts to rate r * exp t, including the point mass at rate zero;
• TauCeti.Probability.binomial_tilted_mul: the native binomial law with success probability p tilts to success probability p * exp t / (1 - p + p * exp t), including the point masses at p = 0 and p = 1.

The continuous identities compare densities through TauCeti.tilted_withDensity, and the discrete ones compare singleton masses through TauCeti.tilted_singleton; in each case the normalizing constant is the family's known moment-generating function.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, Vol. 1, 2nd ed., Wiley, 1994.
• N. L. Johnson, A. W. Kemp, S. Kotz, Univariate Discrete Distributions, 3rd ed., Wiley, 2005.

theorem TauCeti.Probability.gaussianPDFReal_mul_exp_div_mgf (m : ℝ) (v : NNReal) (t x : ℝ) : ProbabilityTheory.gaussianPDFReal m v x * (Real.exp (t * x) / Real.exp (m * t + ↑v * t ^ 2 / 2)) = ProbabilityTheory.gaussianPDFReal (m + ↑v * t) v x

Multiplying the Gaussian density of N(m, v) by exp (t * x) divided by the moment-generating function exp (m t + v t² / 2) gives the density of N(m + v t, v). At variance zero both densities vanish.

@[simp]

theorem TauCeti.Probability.gaussianReal_tilted_mul (m : ℝ) (v : NNReal) (t : ℝ) : ((ProbabilityTheory.gaussianReal m v).tilted fun (x : ℝ) => t * x) = ProbabilityTheory.gaussianReal (m + ↑v * t) v

Exponential tilting of a Gaussian law shifts its mean. Tilting N(m, v) by exp (t * x) gives N(m + v t, v); at variance zero both sides are the point mass at m.

theorem TauCeti.Probability.setIntegral_exp_mul_gaussianReal (m : ℝ) (v : NNReal) (t : ℝ) (s : Set ℝ) : ∫ (x : ℝ) in s, Real.exp (t * x) ∂ProbabilityTheory.gaussianReal m v = Real.exp (m * t + ↑v * t ^ 2 / 2) * (ProbabilityTheory.gaussianReal (m + ↑v * t) v).real s

Integrating the exponential weight exp (t * x) against N(m, v) over a set s gives the moment-generating function exp (m t + v t² / 2) times the mass of s under the tilted law N(m + v t, v).

theorem TauCeti.Probability.gammaMeasure_tilted_mul {a r t : ℝ} (ha : 0 < a) (hr : 0 < r) (ht : t < r) : ((ProbabilityTheory.gammaMeasure a r).tilted fun (x : ℝ) => t * x) = ProbabilityTheory.gammaMeasure a (r - t)

Exponential tilting of a gamma law lowers its rate. For t < r, tilting the gamma law of shape a and rate r by exp (t * x) gives the gamma law of shape a and rate r - t.

@[simp]

theorem TauCeti.Probability.poissonMeasure_tilted_mul (r : NNReal) (t : ℝ) : ((ProbabilityTheory.poissonMeasure r).tilted fun (n : ℕ) => t * ↑n) = ProbabilityTheory.poissonMeasure (r * (Real.exp t).toNNReal)

Exponential tilting of a Poisson law scales its rate. Tilting the native Poisson law of rate r by exp (t * n) gives the Poisson law of rate r * exp t; at rate zero both sides are the point mass at 0.

theorem TauCeti.Probability.binomial_tilted_mul (n : ℕ) (p : ↑unitInterval) (t : ℝ) {q : ↑unitInterval} (hq : ↑q = ↑p * Real.exp t / (1 - ↑p + ↑p * Real.exp t)) : ((ProbabilityTheory.binomial n p).tilted fun (k : ℕ) => t * ↑k) = ProbabilityTheory.binomial n q

Exponential tilting of a binomial law. Tilting the native binomial law with n trials and success probability p by exp (t * k) gives the binomial law with n trials and success probability q = p * exp t / (1 - p + p * exp t). The boundary cases p = 0 and p = 1 are included, where q = p.