Analysis

Content created by Louis Wasserman.

Created on 2025-09-03.
Last modified on 2025-12-30.

module analysis where

open import analysis.absolute-convergence-series-real-numbers public
open import analysis.comparison-test-series-real-numbers public
open import analysis.complete-metric-abelian-groups 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.derivatives-of-real-functions-on-proper-closed-intervals public
open import analysis.metric-abelian-groups public
open import analysis.metric-abelian-groups-normed-real-vector-spaces public
open import analysis.nonnegative-series-real-numbers public
open import analysis.ratio-test-series-real-numbers 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

• 2025-12-30. Louis Wasserman. The ratio test for convergence in real Banach spaces (#1716).
• 2025-12-27. Louis Wasserman. Split out functional analysis as its own module (#1766).
• 2025-12-25. Louis Wasserman. The absolute convergence test in real Banach spaces (#1714).
• 2025-12-03. Louis Wasserman. Series in Banach spaces (#1710).
• 2025-11-21. Louis Wasserman. Derivatives of real functions defined on proper closed intervals (#1680).