innerProbChar_zero

Mathlib.MeasureTheory.Measure.CharacteristicFunction

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

English

The value of innerProbChar at t and x is exp(⟪x, t⟫ I).

Русский

Значение innerProbChar в точке t и аргументе x равно exp(i ⟨x,t⟩).

LaTeX

$$innerProbChar(t)(x) = exp(⟪x, t⟫ · I)$$

Lean4

@[simp]
theorem innerProbChar_zero : innerProbChar (0 : E) = 1 := by simp [innerProbChar]

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

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

Разделы

Аффилиация

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