charFun_neg

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#MeasureTheory.charFun_neg

English

For any μ and t, χ_μ(-t) equals the complex conjugate of χ_μ(t): χ_μ(-t) = overline{χ_μ(t)}.

Русский

Для любой меры μ и любой t верно χ_μ(-t) = \overline{χ_μ(t)}.

LaTeX

$$$$\\chi_{\\mu}(-t) = \\overline{\\chi_{\\mu}(t)}.$$$$

Lean4

@[simp]
theorem charFun_neg (t : E) : charFun μ (-t) = conj (charFun μ t) := by
  simp [charFun_apply, ← integral_conj, ← exp_conj]

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

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

Разделы

Аффилиация

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