charFunDual_eq_charFun_map_one — Mathlib

English

For any L, charFunDual μ L equals the characteristic function of μ mapped by L evaluated at 1.

Русский

Для любого L, χ*_{μ}(L) равно χ_{μ.map L}(1).

LaTeX

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

Lean4

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

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