English
Variant of the pi dual formula for the PiLp setting; the dual characteristic function for the pi-measure decomposes as a product of duals associated with each coordinate.
Русский
Вариант формулы двойственной функции для pi-мера в PiLp, разлагающийся на произведение двойственных функций по координатам.
LaTeX
$$$\operatorname{charFunDual}(\operatorname{Measure.pi}(\mu)) L = \prod_i \operatorname{charFunDual}(\mu_i)(L_i)$$$
Lean4
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is the version for Banach spaces, see `charFunDual_pi`
for the Hilbert space version. -/
theorem charFunDual_pi {ι : 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 ℝ (Π i, E i)) : charFunDual (Measure.pi μ) L = ∏ i, charFunDual (μ i) (L.comp (.single ℝ E i)) := by
simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum, ←
integral_fintype_prod_eq_prod]
