LeanFun RevOLVER

How to read this book

The LeanFun RevOLVER is a book about the mathematics behind Chebfun [DHT14] and ApproxFun [AF, OT14]: Chebyshev and Jacobi expansions, their approximation theory, and the banded operators of sparse spectral methods such as the ultraspherical spectral method [OT13]. Every result in the main chapters is formalised in Lean on top of Mathlib.

Reading paths. Part 2 covers Chebyshev approximation, calculus, quadrature and rootfinding, starting from samples and coefficients. Part 3 develops orthogonal-polynomial theory for general measures and the classical families. Part 4 uses those families in sparse differential operators and studies convergence of finite solves. Part 5 treats measure modification and separated bases in several variables, including an annular Dirichlet solver. For Chebfun, Part 2 can be read independently. For ApproxFun, continue through the classical bases to Part 4.

Scope. The book formalises formulas and convergence theorems used by these methods. It does not verify either software package as a whole: the FFT and convergence of the Remez algorithm, for example, are not formalised here. Chapter 4.4 states the assumptions needed for solver convergence. The annular construction identifies its energy completion with the standard \(H^1_0\) space, giving weak Poisson solvability and convergence of the finite spectral solves.

Finding results. Advanced search includes family formulas and individual results, even those in collapsed boxes. Each chapter opens with links to its principal results. Part 1 collects technical definitions for reference; it can be consulted as needed while reading Part 2. Integral equations are in Part 6.

Layout. Each mathematical statement has a collapsed Lean Formalisation box below it. The signature is extracted from Lean and includes all hypotheses, including section variables and instances. Parentheses denote explicit arguments, braces implicit arguments, and square brackets instances such as a field structure. A hypothesis may therefore appear in the displayed signature even if it was introduced before the declaration’s source line. Definitions include their Lean source. The book omits written proofs; the checked Lean source is available in the Lean proof box. Auxiliary results appear in collapsed Supporting results boxes. The dependency graph records which results depend on which, with colours indicating formalisation status.

What is checked. Lean checks every proof. Whether a Lean statement says what the prose claims is a human question. Statements checked by hand carry a person icon, in the book and in the dependency graph, where their nodes also have bold borders. The review is invalidated automatically if the statement changes. Statements with a robot icon are formalised and checked by Lean but not yet human-reviewed. Results supplied by Mathlib carry no icon: they have a purple border, as in the dependency graph, and a Mathlib badge linking to the Mathlib source file at the pinned revision.

References. Sources are cited with a locator, as in [DLMF, Table 18.3.1]; each citation links to its entry in the References at the end of the book.

Conventions.

  • New families use natural-number indices; Mathlib’s Chebyshev polynomials keep their integer indices.

  • Algebraic identities hold over any commutative \(\mathbb {Q}\)-algebra with denominators cleared: division is replaced by multiplication by the relevant factors. Such identities remain meaningful at degenerate parameters. Analytic results state their parameter ranges and nondegeneracy hypotheses explicitly.

  • Lean’s Bochner integral is a total operation: for a nonintegrable function it takes the default value zero. An integral expression alone does not assert integrability; the hypotheses of each analytic theorem matter.

  • An \(L^2\) element is an almost-everywhere equivalence class, rather than a chosen pointwise function. Lean’s HasSum asserts convergence of a series to the specified value. Neither notation alone supplies a uniform or pointwise convergence claim.

  • Polynomial.Sequence describes a degree-graded polynomial family; orthogonality is an additional property. Results and definitions supplied by Mathlib carry the Mathlib badge.

  • Chebyshev expansions keep the full constant term, \(f=a_0+\sum _{n\ge 1}a_nT_n\).

  • Operators are linear maps; matrices are their coordinates in chosen bases.

  • Orthogonality allows free scaling; uniqueness needs a nondegenerate measure.

Notation across chapters. Some letters have different meanings in different chapters:

  • \(S_N\) is the half-endpoint sampling sum in Chapter 2.4; \(S_Nf\) denotes a polynomial partial sum in Chapter 3.5. The shifted Legendre family \(S_n\) occurs in Chapter 3.3, while \(S\) denotes basis conversion in the operator chapters.

  • \(J(z)\) is the Joukowski map in Chapter 2.5; \(J\) is a multiplication matrix in the operator and quadrature chapters. The map \(J_\mu \) sends a polynomial to its \(L^2(\mu )\) class.

  • \(P_N\) can denote interpolation or a finite projection; \(P_n\) denotes a polynomial family, with Jacobi parameters written as superscripts when needed. \(\mathcal Q_N\) is a quadrature rule, whereas \(Q_n\) in coefficient calculus is a primitive and \(Q_{n,k}\) on the triangle is a Proriol polynomial.

  • \(a_n(f)\) is a Chebyshev coefficient; the \(a_k(x)\) in a differential equation are its polynomial coefficients. Recurrence coefficients \(C_n\) are distinct from ultraspherical polynomials \(C_n^{(\lambda )}\).