English
If X ≤μ-a.e. Y and t ≤ 0, with exp(t·X) integrable, then mgf(Y; μ; t) ≤ mgf(X; μ; t).
Русский
Если X ≤μ-a.e. Y и t ≤ 0, и exp(t·X) интегрируема, то mgf(Y; μ; t) ≤ mgf(X; μ; t).
LaTeX
$$$X \le_{\mu}^{\mathrm{ae}} Y\;\wedge\; t \le 0\;\wedge\; \mathrm{Integrable}(\lambda \omega. e^{t X(\omega)})\,\mu\Rightarrow\; \mathrm{mgf}(Y, \mu, t) \le \mathrm{mgf}(X, \mu, t).$$$
Lean4
/-- The moment-generating function is antitone in the random variable for `t ≤ 0`. -/
theorem mgf_anti_of_nonpos {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : t ≤ 0) (htX : Integrable (fun ω ↦ exp (t * X ω)) μ) :
mgf Y μ t ≤ mgf X μ t := by
by_cases htY : Integrable (fun ω ↦ exp (t * Y ω)) μ
· refine integral_mono_ae htY htX ?_
filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht
· rw [mgf_undef htY]
exact mgf_nonneg
