logMahlerMeasure_def

Mathlib.Analysis.Polynomial.MahlerMeasure

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

English

Equality expressing that logMahlerMeasure is given by 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

theorem logMahlerMeasure_def : p.logMahlerMeasure = circleAverage (fun x ↦ log ‖eval x p‖) 0 1 :=
  rfl

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

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

Разделы

Аффилиация

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