English
The dual characteristic function of a convolution of measures equals the product of dual characteristic functions evaluated at the same L.
Русский
Двойственная характеристическая функция свертки мер равна произведению двойственных функций на той же переменной L.
LaTeX
$$$\operatorname{charFunDual}(\mu * \nu)(L) = \operatorname{charFunDual}(\mu)(L) \cdot \operatorname{charFunDual}(\nu)(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 the version for Banach spaces, see `charFun_eq_pi_iff`
for the Hilbert space version. -/
theorem charFunDual_eq_pi_iff {ι : Type*} [Fintype ι] [DecidableEq ι] {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)]
[∀ i, NormedSpace ℝ (E i)] {mE : ∀ i, MeasurableSpace (E i)} [∀ i, BorelSpace (E i)]
[∀ i, SecondCountableTopology (E i)] [∀ i, CompleteSpace (E i)] {μ : (i : ι) → Measure (E i)}
{ν : Measure (Π i, E i)} [∀ i, IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] :
(∀ L, charFunDual ν L = ∏ i, charFunDual (μ i) (L.comp (.single ℝ E i))) ↔ ν = Measure.pi μ
where
mp
h := by
refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_
rw [h, charFunDual_pi]
mpr h := by rw [h]; exact charFunDual_pi
