English
A pi-variant: the dual characteristic function equality for π-measures characterizes equality with product measure in PiLp context.
Русский
Пи-вариант: равенство двойственной характеристической функции для π-мер характеризует равенство с произведением мер в контексте PiLp.
LaTeX
$$"For all L, χ*(ξ.map toLp p)(L) = ∏ χ*(μ_i)(L ◦ single_i) iff ξ = μ.prod ν"$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is `charFunDual_pi` for `PiLp`.
See `charFunDual_pi` for the Banach space version. -/
theorem charFunDual_pi' (p : ℝ≥0∞) [Fact (1 ≤ p)] {ι : Type*} [Fintype ι] [DecidableEq ι] {E : ι → Type*}
[∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℝ (E i)] {mE : ∀ i, MeasurableSpace (E i)}
{μ : (i : ι) → Measure (E i)} [∀ i, SigmaFinite (μ i)] (L : StrongDual ℝ (PiLp p E)) :
charFunDual ((Measure.pi μ).map (toLp p)) L =
∏ i,
charFunDual (μ i)
(L.comp ((PiLp.continuousLinearEquiv p ℝ E).symm.toContinuousLinearMap.comp (.single ℝ E i))) :=
by
simp_rw [charFunDual_apply, ← integral_fintype_prod_eq_prod, ← Complex.exp_sum, ← Finset.sum_mul, ← ofReal_sum,
L.comp_apply, ← map_sum, ContinuousLinearMap.sum_comp_single]
rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]
simp
