English
A variant of the product-characteristic-function formula for WithLp spaces; the dual characteristic function of the pi-measure equals product of duals evaluated at single coordinates with a structured composition.
Русский
Вариант формулы произведения характеристических функций для WithLp; двойственная характеристическая функция для π-меры равна произведению двойственных функций на координатах.
LaTeX
$$$\\operatorname{charFunDual}((\\operatorname{Measure.pi}\\,\\mu)^{(p)})\,L = \\prod_i \\operatorname{charFunDual}(\\mu_i)(L_i)$$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see `charFun_prod`
for the Hilbert space version. -/
theorem charFunDual_prod [SFinite μ] [SFinite ν] (L : StrongDual ℝ (E × F)) :
charFunDual (μ.prod ν) L = charFunDual μ (L.comp (.inl ℝ E F)) * charFunDual ν (L.comp (.inr ℝ E F)) := by
simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul, Complex.exp_add, ← integral_prod_mul]
