Liouville's theorem (differential algebra)

Proved

LiouvilleDiffAlg.liouville_basic_theorem

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebrasymbolic-integration

Let $F \subseteq G$ be differential fields of characteristic zero with the same constants, $\operatorname{Con}(F) = \operatorname{Con}(G)$ , and suppose that $G$ is an elementary differential extension of $F$ . Suppose $f \in F$ and $g \in G$ satisfy $Dg = f$ (that is, $G$ contains an antiderivative of $f$ ). Then there exist $n \ge 0$ , constants $c_1, \dots, c_n \in \operatorname{Con}(F)$ , nonzero elements $f_1, \dots, f_n \in F$ and $s \in F$ such that

f = c_1\frac{Df_1}{f_1} + \cdots + c_n\frac{Df_n}{f_n} + Ds.

In words: if $f$ has an antiderivative in an elementary extension of $F$ , then that antiderivative is an element of $F$ plus a constant linear combination of logarithms of elements of $F$ . This is the theorem on which the Risch algorithm is based.

Formalization Note The characteristic-zero hypothesis is not written in the source article. It is the standing convention of the theorem in its standard references (Rosenlicht 1972; Geddes–Czapor–Labahn §12.4). The equality of constants is stated as: the image of $\operatorname{Con}(F)$ in $G$ equals $\operatorname{Con}(G)$ .

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_Basic

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem liouville_basic_theorem {F G : Type*} [Field F] [Field G] [Differential F]
    [Differential G] [Algebra F G] [DifferentialAlgebra F G] [CharZero F]
    (hcon : algebraMap F G '' constants F = constants G)
    (helem : IsElementaryDifferentialExtension F G)
    (f : F) (g : G) (hg : g′ = algebraMap F G f) :
    ∃ (n : ℕ) (c : Fin n → F) (u : Fin n → F) (v : F),
      (∀ i, c i ∈ constants F) ∧ (∀ i, u i ≠ 0) ∧
      f = ∑ i, c i * ((u i)′ / u i) + v′ := by sorry

end LiouvilleDiffAlg

Source

Wikipedia, "Liouville's theorem (differential algebra)", revision oldid=1349223559, https://en.wikipedia.org/w/index.php?title=Liouville%27s_theorem_(differential_algebra)&oldid=1349223559, section "Basic theorem"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements below (Aristotle, by Harmonic), with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; please compare it against the Lean code yourself.

Let $F$ and $G$ be fields, each with a derivation $D$ (over $\mathbb{Z}$ ), with an algebra map $\iota : F \to G$ commuting with the derivations ( $D\,\iota(a) = \iota(Da)$ ), and assume $F$ has characteristic zero. Assume:

$\iota(\{a \in F : Da = 0\}) = \{b \in G : Db = 0\}$ (equality of sets);
$G$ is an elementary differential extension of $F$ : there are $m \in \mathbb{N}$ and intermediate fields $K_0 = \iota(F) \subseteq \dots$ , $K_m = G$ , where each $K_{i+1}$ ( $i < m$ ) is generated over $F$ by $K_i$ and a single $t \in G$ . This $t$ is algebraic over $K_i$ , or transcendental over $K_i$ with $Dt = Ds/s$ for some nonzero $s \in K_i$ , or transcendental over $K_i$ with $Dt/t = Ds$ for some $s \in K_i$ , with derivatives computed in $G$ ;
$f \in F$ and $g \in G$ with $Dg = \iota(f)$ .

Then there exist $n \in \mathbb{N}$ (possibly $0$ ), elements $c_1, \dots, c_n \in F$ with $Dc_j = 0$ , elements $u_1, \dots, u_n \in F$ with every $u_j \neq 0$ , and $v \in F$ such that, in $F$ ,

f = \sum_{j=1}^{n} c_j \frac{Du_j}{u_j} + Dv.

When $n = 0$ the sum is empty and the conclusion says $f = Dv$ .

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph