Events

theorem mgf_of_iid
{Y : ℕ → Ω → ℝ}
{Z : ℕ → Ω → ℝ}
(h_meas : ∀ (i : ℕ), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (i : ℕ) => inferInstance) Y μ)
(hident : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (Y i) (Y j) μ μ)
(Z_def : ∀ n : ℕ, Z n = (Real.sqrt n)⁻¹ • (∑ i ∈ Finset.range n, Y i)) :
  ∀ n : ℕ, n > 0 →
    ∀ t : ℝ, mgf (Z n) μ t = (mgf (Y 0) μ ((√n)⁻¹ * t)) ^ n := by
  intro n hn t
  rw [Z_def]
  rw [ProbabilityTheory.mgf_smul_left]