-- Mathlib/Probability/Moments/Basic.lean
theorem aestronglyMeasurable_exp_mul_sum {X : ι → Ω → ℝ} {s : Finset ι}
    (h_int : ∀ i ∈ s, AEStronglyMeasurable (fun ω => exp (t * X i ω)) μ) :
    AEStronglyMeasurable (fun ω => exp (t * (∑ i ∈ s, X i) ω)) μ

Proof state:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ

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_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ ∅, X i) ω)) μ

case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  (∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ) →
    AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Proof state:
case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
simp only [Pi.zero_apply, sum_apply, sum_empty, mul_zero, exp_zero]

Result:
case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => 1) μ

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Tactic:
rw [sum_insert hi_notin_s]

Result:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (X i + ∑ x ∈ s, X x) ω)) μ

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  (∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ) →
    AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Tactic:
specialize h_rec this

Result:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  (∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ) →
    AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Tactic:
have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
  h_int i (mem_insert_of_mem hi)

Result:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  (∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ) →
    AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ insert i s, X i) ω)) μ

Proof state:
case empty
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ i ∈ ∅, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (fun ω => 1) μ

Tactic:
exact aestronglyMeasurable_const

Result:
no goals

Proof state:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (fun ω => rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (fun ω => rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (fun ω => rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (X i + ∑ x ∈ s, X x) ω)) μ

Tactic:
apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec

Result:
no goals