Differentiation on Interval

Abstract

This article generalizes the differential method on intervals, using the Mizar system [2], [3], [12]. Differentiation of real one-variable functions is introduced in Mizar [13], along standard lines (for interesting survey of formalizations of real analysis in various proof-assistants like ACL2 [11], Isabelle/HOL [10], Coq [4], see [5]), but the differentiable interval is restricted to open intervals. However, when considering the relationship with integration [9], since integration is an operation on a closed interval, it would be convenient for differentiation to be able to handle derivates on a closed interval as well. Regarding differentiability on a closed interval, the right and left differentiability have already been formalized [6], but they are the derivatives at the endpoints of an interval and not demonstrated as a differentiation over intervals. Therefore, in this paper, based on these results, although it is limited to real one-variable functions, we formalize the differentiation on arbitrary intervals and summarize them as various basic propositions. In particular, the chain rule [1] is an important formula in relation to differentiation and integration, extending recent formalized results [7], [8] in the latter field of research.