norm_complexMGF_le_mgf — Mathlib

English

For any complex z, the modulus of the complex MGF is bounded above by the real MGF evaluated at the real part of z: ||complexMGF X μ z|| ≤ mgf X μ (Re z).

Русский

Пусть z — комплексное число. Модуль комплексной MGФ не превышает MGФ на действительной оси в точке Re(z): ||complexMGF X μ z|| ≤ mgf X μ (Re z).

LaTeX

$$$\|complexMGF(X,\mu; z)\| \le mgf(X,\mu; \operatorname{Re}(z))$$$

Lean4

theorem norm_complexMGF_le_mgf : ‖complexMGF X μ z‖ ≤ mgf X μ z.re :=
  by
  rw [complexMGF, ← re_add_im z]
  simp_rw [add_mul, Complex.exp_add, re_add_im]
  calc
    ‖∫ ω, cexp (z.re * X ω) * cexp (z.im * I * X ω) ∂μ‖
    _ ≤ ∫ ω, ‖cexp (z.re * X ω) * cexp (z.im * I * X ω)‖ ∂μ := (norm_integral_le_integral_norm _)
    _ = ∫ ω, rexp (z.re * X ω) ∂μ := by simp [Complex.norm_exp]

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