$\frac{1}{x^2+1} = \frac{1}{2i}\frac{Du}{u}$ with $u = \frac{1+ix}{1-ix}$

Proved

LiouvilleDiffAlg.inv_X_sq_add_one_liouville_form

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

differential-algebrarational-functions

Equip $\mathbb{C}(x)$ with the standard derivative $D = d/dx$ and let

u = \frac{1 + ix}{1 - ix} \in \mathbb{C}(x).

Then $u \neq 0$ and

\frac{1}{x^2+1} = \frac{1}{2i} \cdot \frac{Du}{u}.

This is the differential-algebra content of the identity $\tan^{-1} x = \frac{1}{2i}\ln\frac{1+ix}{1-ix}$ . It exhibits $1/(x^2+1)$ in the form of Liouville's theorem with $n = 1$ , $c_1 = \frac{1}{2i} \in \operatorname{Con}(\mathbb{C}(x))$ , $f_1 = u$ and $s = 0$ .

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem inv_X_sq_add_one_liouville_form [Differential (RatFunc ℂ)] (hD : IsStandardDerivation) :
    (1 + algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X) /
        (1 - algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X) ≠ 0 ∧
    1 / (RatFunc.X ^ 2 + 1) =
      algebraMap ℂ (RatFunc ℂ) (1 / (2 * Complex.I)) *
        (((1 + algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X) /
            (1 - algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X))′ /
          ((1 + algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X) /
            (1 - algebraMap ℂ (RatFunc ℂ) Complex.I * RatFunc.X))) := 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 "Examples": "a calculation with Euler's formula ... shows that in fact the antiderivatives can be written in the required manner (as logarithms of rational functions)";

\tan^{-1}x = \frac{1}{2i}\ln\left(\frac{1+ix}{1-ix}\right)

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 $\mathbb{C}(x)$ carry a derivation $D$ (over $\mathbb{Z}$ ) with $D(p) = p'$ for every polynomial $p$ . Write $i$ for the imaginary unit viewed as a constant rational function and $u = (1 + i x)/(1 - i x) \in \mathbb{C}(x)$ . The statement asserts both:

$u \neq 0$ ;

\frac{1}{x^2+1} = \frac{1}{2i} \cdot \frac{Du}{u},

where $\frac{1}{2i}$ is the complex number $1/(2i)$ embedded as a constant rational function.

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

1x2+1=12iDuu\frac{1}{x^2+1} = \frac{1}{2i}\frac{Du}{u}x2+11​=2i1​uDu​ with u=1+ix1−ixu = \frac{1+ix}{1-ix}u=1−ix1+ix​

$\frac{1}{x^2+1} = \frac{1}{2i}\frac{Du}{u}$ with $u = \frac{1+ix}{1-ix}$