intervalIntegrable_mahlerMeasure — Mathlib

English

For any p ∈ ℂ[X], the function x ↦ log |p(circleMap(0,1,x))| is integrable on [0, 2π].

Русский

Для любого p ∈ ℂ[X] функция x ↦ log|p(circleMap(0,1,x))| интегрируема на \\[0, 2π\\].

LaTeX

$$$$ \\text{IntervalIntegrable}\\left( x \\mapsto \\log \\left\\| p\\left( \\circleMap(0,1,x) \\right) \\right\\| \\right) \\text{ on } [0,2\\pi]. $$$$

Lean4

theorem intervalIntegrable_mahlerMeasure :
    IntervalIntegrable (fun x ↦ log ‖p.eval (circleMap 0 1 x)‖) MeasureTheory.volume 0 (2 * π) :=
  by
  rw [← circleIntegrable_def fun z ↦ log ‖p.eval z‖]
  exact circleIntegrable_log_norm_meromorphicOn <| (analyticOnNhd_id.aeval_polynomial p).meromorphicOn

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