TDAF

A formal library of applied mathematics, built in two layers. This is the backbone: general mathematics, named for its subject and stated at the weakest hypotheses that carry the proof. It is meant to be read and used without reference to any particular text.

The surfaces are TdafSurface, a library of its own, one directory per textbook and each aligned to its text section by section. A surface proves almost nothing: each declaration instantiates a backbone result at the book's own hypotheses, so a surface reads as an integration test of this library against a published account of the subject. The dependency runs that way and never the other, which is why the surfaces are separate and the backbone builds without them.

Convex analysis

Tdaf.Analysis.Convex is the backbone for convex analysis over real vector spaces, developed at four levels of generality — a bare real vector space, a topological vector space, a locally convex space, and finite-dimensional Euclidean space — with each result stated at the weakest of the four that supports it. TdafSurface.Rockafellar is the surface that tests it, against R. T. Rockafellar, Convex Analysis (Princeton, 1970), covering all thirty-nine sections of the book.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.