Multivariable Mahler measure

DefinitionPhase of an exponent vector#✓fully proved

For an angle vector \(\theta \in \mathbb{R}^n\) and an exponent vector \(e \in \mathbb{Z}^n\), the real phase of \(e\) at \(\theta\) is \(\sum_{j} e_j \theta_j\).

def realSum (θ : Fin n → ℝ) (e : Fin n → ℤ) : ℝ :=
  ∑ j, (e j : ℝ) * θ j

Used by 2

Used byTorus character · Torus character as a monoid homomorphism

DefinitionTorus character#✓fully proved

For an angle vector \(\theta \in \mathbb{R}^n\), the torus character at \(\theta\) sends an exponent vector \(e \in \mathbb{Z}^n\) to \(\exp\bigl(i \sum_{j} e_j \theta_j\bigr) \in \mathbb{C}\).

def torusCharacter (θ : Fin n → ℝ) (e : Fin n → ℤ) : ℂ :=
  Complex.exp (Complex.I * (realSum θ e : ℂ))

Uses 1 · Used by 1

Statement usesPhase of an exponent vector

Used byTorus character as a monoid homomorphism

DefinitionTorus character as a monoid homomorphism#✓fully proved

For an angle vector \(\theta \in \mathbb{R}^n\), the torus character \(e \mapsto \exp\bigl(i \sum_{j} e_j \theta_j\bigr)\), viewed as a map from the additive group \(\mathbb{Z}^n\) written multiplicatively to the multiplicative monoid of \(\mathbb{C}\), is a monoid homomorphism: it sends \(0\) to \(1\) and sums to products.

def torusCharacterHom (θ : Fin n → ℝ) : Multiplicative (Fin n → ℤ) →* ℂ where
  toFun e := torusCharacter θ e.toAdd
  map_one' := by simp
  map_mul' a b := by
    have h : (a * b).toAdd = a.toAdd + b.toAdd := toAdd_mul a b
    simpa only [h] using torusCharacter_add θ a.toAdd b.toAdd

Uses 2 · Used by 1

Statement usesPhase of an exponent vector · Torus character

Used byEvaluation on the unit torus

DefinitionEvaluation on the unit torus#✓fully proved

For an angle vector \(\theta \in \mathbb{R}^n\), evaluation at the point \((\exp(i\theta_1), \dots, \exp(i\theta_n))\) of the unit torus is the \(\mathbb{C}\)-algebra homomorphism from complex Laurent polynomials in \(n\) variables to \(\mathbb{C}\) that, writing \(X^e\) for the monomial with exponent vector \(e \in \mathbb{Z}^n\), sends \(\sum_e c_e X^e\) to \(\sum_e c_e \exp\bigl(i \sum_{j} e_j \theta_j\bigr)\).

noncomputable def torusEval (θ : Fin n → ℝ) :
    AddMonoidAlgebra ℂ (Fin n → ℤ) →ₐ[ℂ] ℂ :=
  (AddMonoidAlgebra.lift ℂ ℂ (Fin n → ℤ)) (torusCharacterHom θ)

Uses 1 · Used by 1

Statement usesTorus character as a monoid homomorphism

Used byLogarithmic Mahler measure

DefinitionNormalized box integral#✓fully proved

For a function \(f \colon \mathbb{R}^m \to \mathbb{R}\), the normalized box integral of \(f\) is \((2\pi)^{-m} \int_{[0, 2\pi]^m} f(x) \, dx\), the integral taken with respect to Lebesgue measure (and equal to \(0\) when \(f\) is not integrable on the box).

noncomputable def normalizedBoxIntegral {m : ℕ} (f : (Fin m → ℝ) → ℝ) : ℝ :=
  ((2 * Real.pi) ^ m)⁻¹ *
    ∫ x in Set.Icc (0 : Fin m → ℝ) (fun _ => 2 * Real.pi), f x ∂volume

Used by 1

Used byLogarithmic Mahler measure

DefinitionLogarithmic Mahler measure#✓fully proved

For a complex Laurent polynomial \(F\) in \(m\) variables, the logarithmic Mahler measure of \(F\) is the real number \((2\pi)^{-m} \int_{[0, 2\pi]^m} \log |F(e^{i\theta_1}, \dots, e^{i\theta_m})| \, d\theta\), the integral taken with respect to Lebesgue measure.

The cited source applies this formula to nonzero polynomials. As with Mathlib's logarithmic Mahler measure of one-variable polynomials, the definition here is total: \(\log 0 = 0\) and a non-integrable function has integral \(0\), so in particular the value at \(F = 0\) is \(0\).

noncomputable def logarithmicMahlerMeasure {m : ℕ}
    (F : AddMonoidAlgebra ℂ (Fin m → ℤ)) : ℝ :=
  normalizedBoxIntegral fun θ => Real.log ‖torusEval θ F‖

Uses 2

Statement usesNormalized box integral · Evaluation on the unit torus

DefinitionInteger vectors of length one#✓fully proved

The additive isomorphism from \(\mathbb{Z}^1\), the group of functions \(\{0\} \to \mathbb{Z}\) under pointwise addition, to \(\mathbb{Z}\) that sends a function \(e\) to its value \(e(0)\).

def finOneAddEquiv : (Fin 1 → ℤ) ≃+ ℤ :=
  AddEquiv.funUnique (Fin 1) ℤ

Used by 1

Used byIdentification of one-variable Laurent polynomials

DefinitionIdentification of one-variable Laurent polynomials#✓fully proved

The \(\mathbb{C}\)-algebra isomorphism from complex Laurent polynomials whose exponents are vectors \(e \in \mathbb{Z}^1\) (functions \(\{0\} \to \mathbb{Z}\)) to complex Laurent polynomials \(\mathbb{C}[T, T^{-1}]\) in one variable, induced by the additive isomorphism \(\mathbb{Z}^1 \cong \mathbb{Z}\), \(e \mapsto e(0)\). Writing \(X^{e}\) for the monomial with exponent vector \(e\), it sends \(c\,X^{e}\) to \(c\,T^{e(0)}\).

noncomputable def bridgeLaurent :
    AddMonoidAlgebra ℂ (Fin 1 → ℤ) ≃ₐ[ℂ] LaurentPolynomial ℂ :=
  AddMonoidAlgebra.domCongr ℂ ℂ finOneAddEquiv

Uses 1

Statement usesInteger vectors of length one

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.