mahlerMeasure_one

Mathlib.Analysis.Polynomial.MahlerMeasure

URI: https://scilib.ai/kg/mathlib#Polynomial.mahlerMeasure_one

English

Re-states that logMahlerMeasure equals the circle average expression.

Русский

Повторно формулируется, что logMahlerMeasure равно выражению через окружность.

LaTeX

$$$$ p.logMahlerMeasure = \\frac{1}{2\\pi} \\int_{0}^{2\\pi} \\log \\left|p\\left(e^{ix}\\right)\\right| dx. $$$$

Lean4

@[simp]
theorem mahlerMeasure_one : (1 : ℂ[X]).mahlerMeasure = 1 := by simp [mahlerMeasure]

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

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

Разделы

Аффилиация

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