Some of the lab entries related to mathematical analysis include functional analysis, harmonic analysis, complex analysis, Weierstrass preparation theorem, several complex variables, Fourier transform, Pontrjagin dual, functional analysis, differential geometry, Legendre polynomial, dilogarithm, Hilbert space, Banach space, Banach algebra, topological vector space, locally convex space, operator algebras, Gelfand spectrum, measure space, measurable function, Lebesgue space, Sobolev space, bounded operator, compact operator, Fredholm operator, distribution (generalized function), hyperfunction.spectral theory, integral, integration…and a book entry Handbook of analysis and its foundations. Many of the basic notions used in analysis courses are described in lab in the more general topological context if they belong there, e.g. compact space, continuous map, compact-open topology and so on. Many of the aspects of analytic geometry are treated in terms of Riemann surfaces, monodromy, local systems and so on.
Alternative foundations, especially constructive and those using topos theory, are of traditional interest to the category theory community. For example the synthetic differential geometry of Lawvere and Kock (more in next paragraph) and the nonstandard analysis of Robinson, and its variant, internal set theory of Nelson are some of the principal examples. See also Fermat theory, natural numbers object, infinitesimal number etc. Many statements are about the versions without the axiom of choice and so on; we like to state clean and minimal conditions when possible.
Various smoothness concepts in geometry, rarely studied in standard courses of analysis, but sometimes relevant, were studied to fair extent (and sometimes with innovations) in the lab. These smoothness concepts are built using some primitive notions in rather generalized (often categorical) setups: Kähler differential, differential form, tangent space, jet bundles, resolution of diagonal, infinitesimal object, microlinear space, generalized smooth algebra, tangent category, cotangent complex as defining ingredients of various notions of smoothness and smooth spaces. Main framework to systematize in geometry similar notion studied in lab is synthetic differential geometry but many other examples are also represented. Let us mention generalized smooth space, stratifold, Frölicher space, and some graded and super analogues (supermanifold, NQ-supermanifold, integration over supermanifolds); some concepts of smoothness are rather algebraic, e.g. formal smoothness of Grothendieck; see also algebraic approaches to differential calculus. Special attention in lab has been paid to smooth group like objects like Lie group, Lie groupoid and their superanalogues and categorifications, as well as to their tangent structures like Lie algebroids and their interrelations (Lie theory: integration, Lie integration).
Some other entries are related to the conceptual and categorical understanding of Feynman path integral, however so far from physical, conceptual and formal point of view only (and not of analytic theory). This is closely related to understanding various higher categorical spaces of sections in geometry and in study of sigma-models in physics. This is here called geometric function theory (cf. space and quantity, geometric quantization…).
Very relevant for quantization is also the geometric study of differential operators (see D-geometry, diffiety) and distributions (cf. microlocal analysis), by analysis of oscillating integrals (semiclassical approximation), symplectic geometry (esp. the geometry of lagrangian submanifolds which could often be viewed as quantum points) etc. Some of the topological properties of differential operators are studied in index theory, where special role have so called Dirac operators. Sometimes it is possible or even useful to avoid fine analysis by using the algebraic approaches to differential calculus and differential operators, what also makes possible some noncommutative analogues.
See also disambiguation entry calculus.
R. O’Connor, A Monadic, Functional Implementation of Real Numbers. MSCS, 17(1):129-159, 2007 (arXiv:0605058)
R. O’Connor, Certified exact transcendental real number computation in Coq, In TPHOLs 2008, LNCS 5170, pages 246–261, 2008.
R. O’Connor, Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory, PhD thesis, Radboud University Nijmegen, 2009.