English
The characteristic function of a convolution of measures equals the product of their characteristic functions evaluated at the same argument L.
Русский
Характеристическая функция свёртки мер равна произведению характеристических функций по тем же аргументам L.
LaTeX
$$$\operatorname{charFun}(μ * ν)(L) = \operatorname{charFun}(μ)(L) \cdot \operatorname{charFun}(ν)(L)$$$
Lean4
/-- The characteristic function of a convolution of measures
is the product of the respective characteristic functions. -/
theorem charFunDual_conv {μ ν : Measure E} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (L : StrongDual ℝ E) :
charFunDual (μ ∗ ν) L = charFunDual μ L * charFunDual ν L :=
by
simp_rw [charFunDual_apply]
rw [integral_conv]
· simp [add_mul, Complex.exp_add, integral_const_mul, integral_mul_const]
· exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)
