cgf_sum — Mathlib

English

If X and Y are a.e.-measurable, then exp(t(X+Y)) is aestronglyMeasurable.

Русский

Если X и Y а.е.-измеримы, то exp(t(X+Y)) является aestronglyMeasurable.

LaTeX

$$$\mathrm{AEStronglyMeasurable}\big(\omega \mapsto e^{t(X(\omega)+Y(\omega))}\big)\mu$$

Lean4

theorem cgf_sum {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ i, Measurable (X i)) {s : Finset ι}
    (h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) : cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t :=
  by
  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  simp_rw [cgf]
  rw [← log_prod _ _ fun j hj => ?_]
  · rw [h_indep.mgf_sum h_meas]
  · exact (mgf_pos (h_int j hj)).ne'

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