charFun_map_eq_charFunDual_smul — Mathlib

English

The characteristic function of the pushforward μ.map L evaluated at u equals the dual characteristic function of μ evaluated at the scalar multiple uL.

Русский

Характеристическая функция образа μ.map L в точке u равна двойственной характеристической функции μ в точке uL.

LaTeX

$$$\operatorname{charFun}(\mu\mapsto L)(u) = \operatorname{charFunDual}(\mu)(u\,L)$$$

Lean4

theorem charFun_map_eq_charFunDual_smul [OpensMeasurableSpace E] (L : StrongDual ℝ E) (u : ℝ) :
    charFun (μ.map L) u = charFunDual μ (u • L) :=
  by
  rw [charFunDual_apply]
  have : ∫ x, cexp ((u • L) x * I) ∂μ = ∫ x, cexp (u * x * I) ∂(μ.map L) :=
    by
    rw [integral_map]
    · simp
    · fun_prop
    · exact Measurable.aestronglyMeasurable <| by fun_prop
  rw [this, charFun_apply]
  simp

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