English
A pi-variant of the dual equality: the dual characteristic function equality for ν equals that for a product measure; implies ν is the product measure.
Русский
Пи-вариант двойственной равенства: равенство двойственных характеристических функций ν означает, что ν является произведением мер.
LaTeX
$$(∀ L, χ^*(ν)(L) = ∏ χ^*(μ_i)(L ∘ single_i)) ⇔ ν = μ.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 `charFunDual_eq_pi_iff` for `PiLp`.
See `charFun_eq_pi_iff` for the Hilbert space version. -/
theorem charFunDual_eq_pi_iff' (p : ℝ≥0∞) [Fact (1 ≤ p)] {ι : 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 (ν.map (toLp p)) L =
∏ i,
charFunDual (μ i)
(L.comp ((PiLp.continuousLinearEquiv p ℝ E).symm.toContinuousLinearMap.comp (.single ℝ E i)))) ↔
ν = Measure.pi μ
where
mp
h :=
by
refine
(MeasurableEquiv.toLp p (Π i, E i)).map_measurableEquiv_injective <|
Measure.ext_of_charFunDual <| funext fun L ↦ ?_
rw [MeasurableEquiv.coe_toLp, h, charFunDual_pi']
mpr h := by rw [h]; exact charFunDual_pi' p
