English
The characteristic function of a Dirac measure at x is χ_{dirac x}(t) = e^{i⟨x,t⟩}.
Русский
Характеристическая функция дираковской меры в точке x равна e^{i⟨x,t⟩}.
LaTeX
$$$$\\chi_{\\mathrm{dirac}\\,x}(t) = e^{i \\langle x,t \\rangle}.$$$$
Lean4
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Hilbert spaces, see `charFunDual_eq_prod_iff`
for the Banach space version. -/
theorem charFun_eq_prod_iff {μ : Measure E} {ν : Measure F} {ξ : Measure (E × F)} [IsFiniteMeasure μ]
[IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ t, charFun (ξ.map (toLp 2)) t = charFun μ (ofLp t).1 * charFun ν (ofLp t).2) ↔ ξ = μ.prod ν
where
mp
h :=
by
refine (MeasurableEquiv.toLp 2 (E × F)).map_measurableEquiv_injective <| Measure.ext_of_charFun <| funext fun t ↦ ?_
rw [MeasurableEquiv.coe_toLp, h, charFun_prod]
mpr h := by rw [h]; exact charFun_prod
