charFunDual_map_const_add — Mathlib

English

For measures on product spaces with suitable finiteness and separability hypotheses, the same as in 143882 but with duals swapped, the product structure is characterized by the equality of dual characteristic functions.

Русский

При подходящих условиях конечности и простоты топологической структуры на модулях равно условию 143882, но с двойственными отображениями.

LaTeX

$$(∀ L, χν(L) = ∏ χμ_i(L∘inl_i) ) ↔ ν = π μ$$

Lean4

theorem charFunDual_map_const_add [BorelSpace E] (r : E) (L : StrongDual ℝ E) :
    charFunDual (μ.map (r + ·)) L = charFunDual μ L * cexp (L r * I) :=
  by
  simp_rw [add_comm r]
  exact charFunDual_map_add_const _ _

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