charFunDual_map — Mathlib

English

The dual characteristic function of a product of measures equals the product of the dual characteristic functions of the factors evaluated at the appropriate projections.

Русский

Характеристическая функция двойственной меры произведения равна произведению двойственных характеристических функций факторов, взятых по соответствующим проекциям.

LaTeX

$$$\operatorname{charFunDual}(\mu\prod \nu)(L) = \operatorname{charFunDual}(\mu)(L\circ \iota_1) \cdot \operatorname{charFunDual}(\nu)(L\circ \iota_2)$$$

Lean4

theorem charFunDual_map [OpensMeasurableSpace E] [BorelSpace F] (L : E →L[ℝ] F) (L' : StrongDual ℝ F) :
    charFunDual (μ.map L) L' = charFunDual μ (L'.comp L) :=
  by
  rw [charFunDual_eq_charFun_map_one, charFunDual_eq_charFun_map_one, Measure.map_map (by fun_prop) (by fun_prop)]
  simp

Похожие утверждения