English
A dual pi-equivalence: the dual characteristic function equality for a product measure characterizes equality with the product measure in the WithLp setting.
Русский
Двойственная эквивалентность для произведения мер в контексте WithLp: равенство двойственных характеристических функций эквивалентно тому, что мера есть произведение.
LaTeX
$$$(∀ L, χ^*(ξ)(L) = χ^*(μ)(L∘inl) χ^*(ν)(L∘inr)) \iff ξ = μ.prod ν$$$
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_prod_iff`
for the Hilbert space version. -/
theorem charFunDual_eq_prod_iff [BorelSpace F] [SecondCountableTopology F] [CompleteSpace E] [CompleteSpace F]
{ξ : Measure (E × F)} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteMeasure ξ] :
(∀ L, charFunDual ξ L = charFunDual μ (L.comp (.inl ℝ E F)) * charFunDual ν (L.comp (.inr ℝ E F))) ↔ ξ = μ.prod ν
where
mp
h := by
refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_
rw [h, charFunDual_prod]
mpr h := by rw [h]; exact charFunDual_prod
