logMahlerMeasure — Mathlib

English

For p ∈ ℂ[X], the logarithmic Mahler measure is defined as the circle average of the logarithm of the modulus of p on the unit circle: log M(p) = (2π)⁻¹ ∫_0^{2π} log |p(e^{ix})| dx.

Русский

Для p ∈ ℂ[X] логарифмическая мера Малера определяется как среднее по окружности от log|p(e^{ix})| на единичной окружности: log M(p) = (2π)⁻¹ ∫_0^{2π} log|p(e^{ix})| dx.

LaTeX

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

Lean4

/-- The logarithmic Mahler measure of a polynomial `p` defined as
`(2 * π)⁻¹ * ∫ x ∈ (0, 2 * π), log ‖p (e ^ (i * x))‖` -/
noncomputable def logMahlerMeasure : ℝ :=
  circleAverage (fun x ↦ log ‖eval x p‖) 0 1

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