Lam--Litt conjecture

A conjecture of Lam and Litt on algebraic solutions of algebraic ODEs.

Let $g \in \mathbb{Q}(z, y_0, \dots, y_{n-1})$ be a rational function in $n + 1$ variables. Let $f$ be a power series over $\mathbb{Q}$ such that $f^{(n)}(z) = g(z, f(z), f'(z), \dots, f^{(n-1)}(z))$. Also, assume that $g(0, f(0), f'(0), \dots, f^{(n-1)}(0))$ is defined. Then the following are equivalent:

1. $f$ is algebraic over $\mathbb{Q}[z]$.
2. There exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.
3. There exists an integer-valued function $\omega$ on the set of primes with $\lim_{p \to \infty} \omega(p) / p = \infty$ such that, for each prime $p$, the rational numbers $a_0, a_1, \dots, a_{\omega(p)}$ are in $\mathbb{Z}_{(p)}$.

The implication 1) => 2) is due to Eisenstein, and 2) => 3) is trivial.

References:

• Litt's problem 1
• Yeuk Hay Joshua Lam, Daniel Litt, "Algebraicity and integrality of solutions to differential equations", arxiv/2501.13175
• Gotthold Eisenstein. "Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen", Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852

TODO:

• Lam-Litt conjecture implies Grothendieck p-curvature conjecture.
• Examples in Remark 1.1.3 and 1.1.5 on the conditions of the conjecture.

def LamLitt.IsSolutionOfAlgebraicODE (n : ℕ) (f : PowerSeries ℚ) (g : MvRatFunc (Fin (n + 1)) ℚ) : Prop

A power series $f$ is a solution of an algebraic ODE defined by the rational function $g \in \mathbb{Q}(z, y_0, \dots, y_{n-1})$ if $f^{(n)}(z) = g(z, f(z), f'(z), \dots, f^{(n-1)}(z))$. The variable indexed by 0 : Fin (n + 1) corresponds to $z$, and the variable indexed by i.succ corresponds to $y_i = f^{(i)}(z)$.

Equations

• One or more equations did not get rendered due to their size.

def LamLitt.ℤAdjoinInvNat (N : ℕ) : Subalgebra ℤ ℚ

Equations

• LamLitt.ℤAdjoinInvNat N = Algebra.adjoin ℤ {1 / ↑N}

def LamLitt.IsCoeffIntegralAdjointInvNat (f : PowerSeries ℚ) (N : ℕ) : Prop

There exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.

Equations

• LamLitt.IsCoeffIntegralAdjointInvNat f N = ∀ (n : ℕ), (PowerSeries.coeff n) f ∈ LamLitt.ℤAdjoinInvNat N

def LamLitt.omegaIntegral (ω : Nat.Primes → ℤ) (a : ℕ → ℚ) : Prop

For an integer-valued function $\omega$ on the set of primes and a sequence $a_n$ of rational numbers, the condition $\omega$-integrality means that for each prime $p$, the rational numbers $a_0, a_1, \dots, a_{\omega(p)}$ are in $\mathbb{Z}_{(p)}$, i.e. their denominators are not divisible by $p$. When $\omega(p) < 0$ the constraint at $p$ is vacuous.

Equations

• LamLitt.omegaIntegral ω a = ∀ (p : Nat.Primes) (j : ℕ), ↑j ≤ ω p → (a j).den.Coprime ↑p

def LamLitt.omegaSuperlinear (ω : Nat.Primes → ℤ) : Prop

The growth condition on $\omega$: the ratio $\omega(p) / p$ tends to infinity as the prime $p$ tends to infinity, i.e. $\lim_{p \to \infty} \omega(p) / p = \infty$. Here the source filter is Filter.atTop on the primes, obtained by pulling back Filter.atTop on $\mathbb{N}$ along the coercion Nat.Primes → ℕ.

Equations

• LamLitt.omegaSuperlinear ω = Filter.Tendsto (fun (p : Nat.Primes) => ↑(ω p) / ↑↑p) (Filter.comap (fun (p : Nat.Primes) => ↑p) Filter.atTop) Filter.atTop

theorem LamLitt.lam_litt.variants.eisenstein (f : PowerSeries ℚ) (hAlg : IsAlgebraic (Polynomial ℚ) f) : ∃ (N : ℕ), IsCoeffIntegralAdjointInvNat f N

Eisenstein's theorem (1852): an algebraic power series over $\mathbb{Q}[z]$ has bounded denominators, i.e., there exists $N$ such that all coefficients lie in $\mathbb{Z}[1/N]$.

theorem LamLitt.lam_litt.variants.integrality_implies_omega_integrality (f : PowerSeries ℚ) (N : ℕ) (hN : IsCoeffIntegralAdjointInvNat f N) : ∃ (ω : Nat.Primes → ℤ), omegaSuperlinear ω ∧ omegaIntegral ω fun (x : ℕ) => (PowerSeries.coeff x) f

Textbook implication: integrality (2) trivially implies ω(p)-integrality (3).

theorem LamLitt.lam_litt.variants.omega_integrality_implies_algebraicity {n : ℕ} (f : PowerSeries ℚ) (g : MvRatFunc (Fin (n + 1)) ℚ) (hODE : IsSolutionOfAlgebraicODE n f g) (ω : Nat.Primes → ℤ) (hω : omegaSuperlinear ω ∧ omegaIntegral ω fun (x : ℕ) => (PowerSeries.coeff x) f) : ∃ (N : ℕ), IsCoeffIntegralAdjointInvNat f N

3. implies 2): if the coefficients of $f$ satisfy the $\omega$-integrality condition for some superlinear $\omega$, then there exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.

theorem LamLitt.lam_litt.variants.integrality_implies_algebraicity {n : ℕ} (f : PowerSeries ℚ) (g : MvRatFunc (Fin (n + 1)) ℚ) (hODE : IsSolutionOfAlgebraicODE n f g) (N : ℕ) (hN : IsCoeffIntegralAdjointInvNat f N) : IsAlgebraic (Polynomial ℚ) f

2. implies 1): if the coefficients of $f$ are in $\mathbb{Z}[1/N]$ for some $N$, then $f$ is algebraic over $\mathbb{Q}[z]$. Also the version of conjecture of Litt's problem 1 on his website.