charFun_eq_charFunDual_toDualMap — Mathlib

English

If L is a linear map E → F and L' is a dual on F, then the dual characteristic function of μ mapped by L evaluated at L' equals the dual characteristic function of μ evaluated at L' composed with L.

Русский

Если L — линейное отображение E → F, и L' — двойной функционал на F, то χ*_{μ.map L}(L') = χ*_{μ}(L' ∘ L).

LaTeX

$$$\operatorname{charFunDual}(\mu\mapsto L)(L') = \operatorname{charFunDual}(\mu)(L'\circ L)$$$

Lean4

theorem charFun_eq_charFunDual_toDualMap {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {mE : MeasurableSpace E} {μ : Measure E} (t : E) :
    charFun μ t = charFunDual μ (InnerProductSpace.toDualMap ℝ E t) := by
  simp [charFunDual_apply, charFun_apply, real_inner_comm]

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