charFun_map_add_const — Mathlib

English

Equivalent formulation: χ_{μ.map (r + ·)}(t) = χ_{μ}(t) exp(i⟪r,t⟫).

Русский

Эквивалентная формулировка: χ_{μ.map (r + ·)}(t) = χ_{μ}(t) exp(i⟪r,t⟫).

LaTeX

$$$$\\chi_{\\mu \\mapsto (r + \\cdot)}(t) = \\chi_{\\mu}(t) e^{i \\langle r,t \\rangle}.$$$$

Lean4

theorem charFun_map_add_const [BorelSpace E] (r t : E) : charFun (μ.map (· + r)) t = charFun μ t * cexp (⟪r, t⟫ * I) :=
  by
  rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop), ← integral_mul_const]
  congr with a
  rw [← Complex.exp_add]
  congr
  rw [inner_add_left]
  simp only [ofReal_add]
  ring

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