mahlerMeasure — Mathlib

English

The Mahler measure M(p) of a polynomial p is defined by M(p) = exp(logMahlerMeasure(p)) if p ≠ 0, and M(p) = 0 if p = 0.

Русский

Мера Малера M(p) многочлена p определяется как M(p) = exp(logMahlerMeasure(p)) при p ≠ 0, и M(p) = 0 при p = 0.

LaTeX

$$$$ \\mathrm{mahlerMeasure}(p) = \\begin{cases} \\exp\\left( p.logMahlerMeasure \\right), & p \\neq 0, \\\\ 0, & p = 0. \\end{cases} $$$$

Lean4

/-- The Mahler measure of a polynomial `p` defined as `e ^ (logMahlerMeasure p)` if `p` is nonzero
and `0` otherwise -/
noncomputable def mahlerMeasure : ℝ :=
  if p ≠ 0 then exp (p.logMahlerMeasure) else 0

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