一句话:构造性证明近似介值定理:仅需逐点连续,避免可数选择与有理逼近表示。
本文研究构造性数学中近似介值定理的证明条件。经典证明用二分法反复选择区间的左半或右半,但该选择在构造性框架下需要额外假设。作者提出一种连续插值左右选择的算法:每次选取一个规模减半的区间,而非离散地二选一。由此证明:若逐点连续函数在某点取负值、另一点取正值,则其函数值可任意接近 0。该证明仅依赖逐点连续,不假设实数带有有理逼近表示,也不使用可数选择。结果强化了构造性分析中近似介值定理的可用范围。
This paper proves the approximate intermediate value theorem, constructively and from notably weak hypotheses: from pointwise rather than uniform continuity, without assuming that reals are presented with rational approximants, and without using countable choice. The theorem is that if a pointwise continuous function has both a negative and a positive value, then it has values arbitrarily close to 0. The proof builds on the usual classical proof by bisection, which repeatedly selects the left or right half of an interval; the algorithm here selects an interval of half the size in a continuous way, interpolating between those two possibilities.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{Frank17,
title = {Interpolating Between Choices for the Approximate Intermediate Value Theorem},
author = {Matthew Frank},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:5)2020}
}