Learn · Classical analysis
Axeyum for classical analysts
Axeyum provides a concrete place to compare classical existence theorems with constructive algorithms and explicit assumptions.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to classical analysis.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
How does a constructive library compare with familiar classical analysis?
The present library covers real functions on intervals, derivatives, Riemann integration, uniform continuity, constructive suprema, and intermediate and extreme value results. It also records selected Mathlib imports so their assumptions can be compared with Axeyum's constructed route.
This makes familiar theorems useful as controlled comparisons. A classical result may supply an exact object through choice, while the constructive result supplies an approximation procedure or asks for stronger input such as an explicit modulus.
Why it matters
What the current work makes possible
- The library exposes the computational information hidden by an existence proof.
- Axiom footprints make classical and constructive routes directly inspectable.
- The current calculus results are substantial enough to support comparisons theorem by theorem.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next broad layer includes metric and topological spaces, measure, the Lebesgue integral, modes of convergence, and functional analysis.
Those additions can preserve a clear distinction between constructive data, classical assumptions, and executable procedures instead of assigning one policy to the whole library.
Where to begin