char_neg

Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

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

English

For all w ∈ W, char(he,hL,-w) equals the complex conjugate of char(he,hL,w).

Русский

Для каждого w ∈ W выполняется: char(he,hL,-w) = conj(char(he,hL,w)).

LaTeX

$$$\\text{char}(he,hL,-w) = \\overline{\\text{char}(he,hL,w)}.$$$

Lean4

theorem char_neg (w : W) : char he hL (-w) = star (char he hL w) := by ext; simp

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

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

Разделы

Аффилиация

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