  We give a number of formal proofs of theorems from the field of computable
analysis. Many of our results specify executable algorithms that work on
infinite inputs by means of operating on finite approximations and are proven
correct in the sense of computable analysis. The development is done in the
proof assistant Coq and heavily relies on the Incone library for information
theoretic continuity. This library is developed by one of the authors and the
paper can be used as an introduction to the library as it describes many of its
most important features in detail. While the ability to have full executability
in a formal development of mathematical statements about real numbers and the
like is not a feature that is unique to the Incone library, its original
contribution is to adhere to the conventions of computable analysis to provide
a general purpose interface for algorithmic reasoning on continuous structures.
The results that provide complete computational content include that the
algebraic operations and the efficient limit operator on the reals are
computable, that certain countably infinite products are isomorphic to spaces
of functions, compatibility of the enumeration representation of subsets of
natural numbers with the abstract definition of the space of open subsets of
the natural numbers, and that continuous realizability implies sequential
continuity. We also formalize proofs of non-computational results that support
the correctness of our definitions. These include that the information
theoretic notion of continuity used in the library is equivalent to the metric
notion of continuity on Baire space, a complete comparison of the different
concepts of continuity that arise from metric and represented-space structures
and the discontinuity of the unrestricted limit operator on the real numbers
and the task of selecting an element of a closed subset of the natural numbers.
