English
A variant of product dual character function identity for the WithLp setting, expressing a product of dual-character functions on a product measure.
Русский
Вариант тождества для произведения двойственных характеристических функций в обстановке WithLp.
LaTeX
$$$\operatorname{charFunDual}(\mu.prod\nu) L' = \operatorname{charFunDual}(\mu)(L'_1) \cdot \operatorname{charFunDual}(\nu)(L'_2)$$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is `charFunDual_prod` for `WithLp`.
See `charFun_prod` for the Hilbert space version. -/
theorem charFunDual_prod' (p : ℝ≥0∞) [Fact (1 ≤ p)] [SFinite μ] [SFinite ν] (L : StrongDual ℝ (WithLp p (E × F))) :
charFunDual ((μ.prod ν).map (toLp p)) L =
charFunDual μ (L.comp ((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inl ℝ E F))) *
charFunDual ν (L.comp ((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inr ℝ E F))) :=
by
simp_rw [charFunDual_apply, ← integral_prod_mul, ← Complex.exp_add, ← add_mul, ← ofReal_add, L.comp_apply, ← map_add,
ContinuousLinearMap.comp_inl_add_comp_inr]
rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]
simp
