charFunDual_map_add_const — Mathlib

English

For a Borel space E, a constant shift r adds a factor exp(i L(r)).

Русский

При сдвиге на константу r появляется множитель exp(i L(r)).

LaTeX

$$$\operatorname{charFunDual}(\mu.map(L)\,\text{(shift by } r))\,L' = \operatorname{charFunDual}(\mu)(L') \cdot e^{i\,L'(r)}$$$

Lean4

theorem charFunDual_map_add_const [BorelSpace E] (r : E) (L : StrongDual ℝ E) :
    charFunDual (μ.map (· + r)) L = charFunDual μ L * cexp (L r * I) :=
  by
  rw [charFunDual_apply, charFunDual_apply, integral_map (by fun_prop) (by fun_prop), ← integral_mul_const]
  congr with a
  rw [← Complex.exp_add]
  congr
  simp only [map_add, ofReal_add]
  ring

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