English
If exp(t X_i) are aestronglyMeasurable for each i in a finite set s, then exp(t (∑_{i∈s} X_i)) is aestronglyMeasurable.
Русский
Если для каждого i в конечном множестве s функции exp(t X_i) являются aestronglyMeasurable, то exp(t ∑_{i∈s} X_i) тоже является aestronglyMeasurable.
LaTeX
$$$\mathrm{AEStronglyMeasurable}\big(\omega \mapsto e^{t \sum_{i\in s} X_i(\omega)}\big)\mu$$
Lean4
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) ω)) μ := by
classical
induction s using Finset.induction_on with
| empty =>
simp only [sum_apply, sum_empty, mul_zero, exp_zero]
exact aestronglyMeasurable_const
| insert i s hi_notin_s
h_rec =>
have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
h_int i (mem_insert_of_mem hi)
specialize h_rec this
rw [sum_insert hi_notin_s]
apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec
