English
If μi are σ-finite measures on spaces Ei (i in a finite index set), then the characteristic function of the product measure on the product space is the product of the individual characteristic functions.
Русский
Пусть μi — сигма-конечные меры на пространствах Ei (i из конечного множества индексов). Тогда характеристическая функция произведения мер на произведённом пространстве равна произведению характеристических функций каждой меры μi.
LaTeX
$$$\operatorname{charFun}((\operatorname{Measure.pi}\,\mu))\, t \,=\, \prod_{i} \operatorname{charFun}(\mu_i)(t_i)$$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see `charFunDual_pi`
for the Banach space version. -/
theorem charFun_pi {μ : (i : ι) → Measure (E i)} [∀ i, SigmaFinite (μ i)] (t : PiLp 2 E) :
charFun ((Measure.pi μ).map (toLp 2)) t = ∏ i, charFun (μ i) (t i) :=
by
simp_rw [charFun, PiLp.inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_fintype_prod_eq_prod, integral_map_equiv]
simp [ofReal_sum, Finset.sum_mul, Complex.exp_sum]
