---
tag: HEB1VQW0DQ
kind: concept
name: Constructive analysis
msc: ["03F60", "03F65"]
uses: [G958EQ8CWW, 08J2M1JYAG, 0PWX18FM4G, 00KAFBR32E]
sources:
  - url: https://en.wikipedia.org/wiki/Constructive_analysis
same_as:
  wikidata: Q2845197
  wikipedia: Constructive analysis
---

## Summary

Constructive analysis is mathematical analysis carried out under the principles of [[constructivism|G958EQ8CWW]].
[[Real numbers|08J2M1JYAG]] are given by [[Cauchy sequences|0PWX18FM4G]] of rationals with an explicit rate of convergence, and every existence proof must give an approximation method.
Bishop's book "Foundations of Constructive Analysis" of 1967 showed that a large part of classical analysis can be developed in this way.
Its theorems are also valid classically, and they carry algorithms.

## Explanations

### L1 human

In constructive analysis, a real number is something you can compute to any accuracy you ask for.
Some classical facts then need care.
For example, you cannot always decide whether a real number is zero, since you may never see a nonzero digit.
So the [[intermediate value theorem|00KAFBR32E]] is replaced by a version that finds a point where the function is as close to zero as you like.
Results like this are often what a computation can actually deliver.