mgf_mono_of_nonneg — Mathlib

English

If X and Y have IdentDistrib with μ and μ', then mgf X μ = mgf Y μ'.

Русский

Если X и Y имеют IdentDistrib относительно μ и μ', то mgf X μ = mgf Y μ'.

LaTeX

$$$\mathrm{mgf}(X; μ) = \mathrm{mgf}(Y; μ')$$$

Lean4

/-- The moment-generating function is monotone in the random variable for `t ≥ 0`. -/
theorem mgf_mono_of_nonneg {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : 0 ≤ t) (htY : Integrable (fun ω ↦ exp (t * Y ω)) μ) :
    mgf X μ t ≤ mgf Y μ t := by
  by_cases htX : Integrable (fun ω ↦ exp (t * X ω)) μ
  · refine integral_mono_ae htX htY ?_
    filter_upwards [hXY] with ω hω using by gcongr
  · rw [mgf_undef htX]
    exact mgf_nonneg

Похожие утверждения