-- Mathlib/Probability/Moments/Basic.lean
theorem iIndepFun.mgf_sum {X : ι → Ω → ℝ}
    (h_indep : iIndepFun (fun _ => inferInstance) X μ) (h_meas : ∀ i, Measurable (X i))
    (s : Finset ι) : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Proof state:
case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t

Tactic:
simp only [sum_empty, mgf_zero_fun, measure_univ, ENNReal.one_toReal, prod_empty]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure

Result:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
induction' s using Finset.induction_on with i s hi_notin_s h_rec h_int

Result:
case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t

case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Tactic:
have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
  ((h_meas i).const_mul t).exp.aestronglyMeasurable

Result:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (fun x => inferInstance) X μ
h_meas : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Tactic:
rw [sum_insert hi_notin_s,
  IndepFun.mgf_add (h_indep.indepFun_finset_sum_of_not_mem h_meas hi_notin_s).symm (h_int' i)
    (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
  h_rec, prod_insert hi_notin_s]

Result:
no goals