English
The characteristic function of a convolution ξ = μ ∗ ν satisfies χ_ξ(t) = χ_μ(t) χ_ν(t) for appropriate spaces and finiteness hypotheses.
Русский
Характеристическая функция конволюции ξ = μ ∗ ν равна произведению χ_μ(t) χ_ν(t) при необходимых условиях.
LaTeX
$$$$\\chi_{(\\mu * \\nu)}(t) = \\chi_{\\mu}(t) \\cdot \\chi_{\\nu}(t).$$$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Hilbert spaces, see `charFunDual_prod`
for the Banach space version. -/
theorem charFun_prod {μ : Measure E} {ν : Measure F} [SFinite μ] [SFinite ν] (t : WithLp 2 (E × F)) :
charFun ((μ.prod ν).map (toLp 2)) t = charFun μ (ofLp t).1 * charFun ν (ofLp t).2 :=
by
simp_rw [charFun, prod_inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_prod_mul, integral_map_equiv]
simp [ofReal_add, add_mul, Complex.exp_add]
