innerProbChar_apply

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.innerProbChar_apply

English

Define a bounded continuous map x ↦ exp(⟪x, t⟫ I) parameterized by t ∈ E, providing a bounded characertistic-like function.

Русский

Определим ограниченную непрерывную карту x ↦ exp(⟪x, t⟫ I), зависящую от параметра t.

LaTeX

$$innerProbChar(t) : E →ᵇ ℂ with toFun(x) = exp(⟪x, t⟫·I)$$

Lean4

theorem innerProbChar_apply (t x : E) : innerProbChar t x = exp (⟪x, t⟫ * I) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru