English
For σ-finite measures μi and a measure ν on the product space, the equality χν(t) = ∏ χμi(ti) for all t holds if and only if ν is the product measure μ.
Русский
Для сигма-конечных мер μi и меры ν на произведение пространств верна равенство χν(t) = ∏i χμi(ti) для всех t тогда, когда ν является произведением мер μ.
LaTeX
$$(∀ t, \operatorname{charFun}(ν)(t) = ∏_{i} \operatorname{charFun}(μ_i)(t_i)) \iff ν = \operatorname{Measure.pi}(μ)$$
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_pi_iff`
for the Banach space version. -/
theorem charFun_eq_pi_iff {μ : (i : ι) → Measure (E i)} {ν : Measure (Π i, E i)} [∀ i, IsFiniteMeasure (μ i)]
[IsFiniteMeasure ν] : (∀ t, charFun (ν.map (toLp 2)) t = ∏ i, charFun (μ i) (t i)) ↔ ν = Measure.pi μ
where
mp
h :=
by
refine
(MeasurableEquiv.toLp 2 (Π i, E i)).map_measurableEquiv_injective <| Measure.ext_of_charFun <| funext fun t ↦ ?_
rw [MeasurableEquiv.coe_toLp, h, charFun_pi]
mpr h := by rw [h]; exact charFun_pi
