Mahler functions

DefinitionMahler substitution#✓fully proved

For a formal power series \(F \in \mathbb{C}[[z]]\) and natural numbers \(k\) and \(i\), let \(m = k^i\); the power series \(F(z^{k^i})\) is defined coefficientwise. When \(m \ge 1\), its coefficient of \(z^n\) is the coefficient of \(z^{n/m}\) in \(F\) if \(m\) divides \(n\), and \(0\) otherwise; this is the substitution \(z \mapsto z^m\) in \(F\). When \(m = 0\) (that is, \(k = 0\) and \(i \ge 1\)), it is the constant series equal to the constant term of \(F\).

public noncomputable def mahlerSubst
    (F : PowerSeries Complex) (k i : ℕ) : PowerSeries Complex :=
  PowerSeries.mk fun n =>
    if (k ^ i) ∣ n then PowerSeries.coeff (n / (k ^ i)) F else 0

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL16/Bell/bell2.tex.

Used by 1

Used by\(k\)-Mahler functions

Definition\(k\)-Mahler functions#✓fully proved

Let \(k\) be a natural number. A formal power series \(F \in \mathbb{C}[[z]]\) is a \(k\)-Mahler function when \(k \ge 2\) and there exist a natural number \(d\) and polynomials \(a_0(z), \dots, a_d(z) \in \mathbb{C}[z]\) with \(a_0 \ne 0\) and \(a_d \ne 0\) such that the following identity holds in \(\mathbb{C}[[z]]\):

\[\sum_{i=0}^{d} a_i(z)\, F\bigl(z^{k^i}\bigr) = 0.\]

public noncomputable def IsKMahlerFunction (k : ℕ) (F : PowerSeries Complex) : Prop :=
  2 ≤ k ∧
    ∃ (d : ℕ) (a : Fin (d + 1) → Polynomial Complex),
      a ⟨0, Nat.zero_lt_succ d⟩ ≠ 0 ∧
        a ⟨d, Nat.lt_succ_self d⟩ ≠ 0 ∧
          ∑ i : Fin (d + 1),
              Polynomial.toPowerSeries (a i) * mahlerSubst F k i.val = 0

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL16/Bell/bell2.tex.

Uses 1 · Used by 1

Statement usesMahler substitution

Used byNishioka's theorem: algebraic Mahler functions are rational

TheoremNishioka's theorem: algebraic Mahler functions are rational#●ready to prove

Let \(k\) be a natural number and let \(F \in \mathbb{C}[[z]]\) be a \(k\)-Mahler function. If \(F\) is algebraic over \(\mathbb{C}[z]\), that is, \(P(F) = 0\) for some nonzero polynomial \(P\) with coefficients in \(\mathbb{C}[z]\), then \(F\) is rational: there are polynomials \(p, q \in \mathbb{C}[z]\) with \(q \ne 0\) and \(qF = p\) in \(\mathbb{C}[[z]]\).

theorem_wanted nishioka_algebraic_kMahler_is_rational
    (k : ℕ) (F : PowerSeries ℂ)
    (hMahler : IsKMahlerFunction k F)
    (hAlgebraic : ∃ P : Polynomial (Polynomial ℂ), P ≠ 0 ∧
      Polynomial.eval₂ (algebraMap (Polynomial ℂ) (PowerSeries ℂ)) F P = 0) :
    ∃ p q : Polynomial ℂ, q ≠ 0 ∧
      Polynomial.toPowerSeries q * F = Polynomial.toPowerSeries p

Sources

• Jason P. Bell, Michael Coons, and Eric Rowland, "The Rational-Transcendental Dichotomy of Mahler Functions", Journal of Integer Sequences 16 (2013), Article 13.2.10, Nishioka corollary lines 238–241, https://cs.uwaterloo.ca/journals/JIS/VOL16/Bell/bell2.tex. The corollary is attributed to Ku. Nishioka, "Mahler Functions and Transcendence", Lecture Notes in Mathematics 1294, Theorem 5.1.7.

Uses 1

Statement uses\(k\)-Mahler functions

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.