English
If L is a continuous linear map and L' is a dual, then the dual characteristic function of the pushforward μ.map L equals the dual characteristic function of μ composed with L'.
Русский
Для линейного отображения L и двойственного функционала L' выполняется равенство χ^*_{μ.map L}(L') = χ^*_{μ}(L' ∘ L).
LaTeX
$$$\operatorname{charFunDual}(\mu.map L)(L') = \operatorname{charFunDual}(\mu)(L' \circ L)$$$
Lean4
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is `charFunDual_eq_prod_iff` for `WithLp`.
See `charFun_eq_prod_iff` for the Hilbert space version. -/
theorem charFunDual_eq_prod_iff' (p : ℝ≥0∞) [Fact (1 ≤ p)] [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E]
[CompleteSpace F] {ξ : Measure (E × F)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ L,
charFunDual (ξ.map (toLp p)) L =
charFunDual μ
(L.comp ((WithLp.prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inl ℝ E F))) *
charFunDual ν
(L.comp ((WithLp.prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inr ℝ E F)))) ↔
ξ = μ.prod ν
where
mp
h :=
by
refine
(MeasurableEquiv.toLp p (E × F)).map_measurableEquiv_injective <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_
rw [MeasurableEquiv.coe_toLp, h, charFunDual_prod']
mpr h := by rw [h]; exact charFunDual_prod' p
