Analysis

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-09-03.
Last modified on 2026-02-11.

module analysis where

open import analysis.absolute-convergence-series-real-numbers public
open import analysis.addition-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import analysis.alternation-sequences-metric-abelian-groups public
open import analysis.comparison-test-series-real-numbers public
open import analysis.complete-metric-abelian-groups public
open import analysis.composition-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
open import analysis.constructive-intermediate-value-theorem public
open import analysis.convergent-series-complete-metric-abelian-groups public
open import analysis.convergent-series-metric-abelian-groups public
open import analysis.convergent-series-real-numbers public
open import analysis.differentiability-constant-real-maps-on-proper-closed-intervals-real-numbers public
open import analysis.differentiability-identity-map-on-proper-closed-intervals-real-numbers public
open import analysis.differentiability-reciprocal-function-on-positive-proper-closed-intervals-real-numbers public
open import analysis.differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import analysis.intermediate-value-theorem public
open import analysis.limits-of-sequences-metric-abelian-groups public
open import analysis.metric-abelian-groups public
open import analysis.metric-abelian-groups-normed-real-vector-spaces public
open import analysis.monotone-convergence-theorem-increasing-sequences-real-numbers public
open import analysis.nonnegative-series-real-numbers public
open import analysis.ratio-test-series-real-numbers public
open import analysis.scalar-multiplication-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import analysis.sequences-metric-abelian-groups public
open import analysis.series-complete-metric-abelian-groups public
open import analysis.series-metric-abelian-groups public
open import analysis.series-real-numbers public

Recent changes

• 2026-02-11. Louis Wasserman. The derivative of the reciprocal function (#1779).
• 2026-02-11. Fredrik Bakke. Monotone convergence theorem for increasing sequences of reals (#1812).
• 2026-02-04. Louis Wasserman. The constructive intermediate value theorem (#1762).
• 2026-02-03. Louis Wasserman. The chain rule for derivatives of real functions on proper closed intervals (#1775).
• 2026-01-30. Louis Wasserman. Refactor differentiable functions (#1774).