probCharDual — Mathlib

English

Define probCharDual for a StrongDual ℝ F as a bounded char function.

Русский

Определим probCharDual для сильного двойственного пространства как ограниченную характеристическую функцию.

LaTeX

$$probCharDual(L) : F →ᵇ ℂ$$

Lean4

/-- The bounded continuous map `x ↦ exp (L x * I)`, for a continuous linear form `L`. -/
noncomputable def probCharDual (L : StrongDual ℝ F) : F →ᵇ ℂ :=
  char continuous_probChar (L := isBoundedBilinearMap_apply.symm.toContinuousLinearMap.toLinearMap₁₂)
    isBoundedBilinearMap_apply.symm.continuous L

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