<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>This article generalizes the differential method on intervals, using the Mizar system [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_002">2</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_003">3</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_012">12</xref>]. Differentiation of real one-variable functions is introduced in Mizar [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_013">13</xref>], along standard lines (for interesting survey of formalizations of real analysis in various proof-assistants like ACL2 [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_011">11</xref>], Isabelle/HOL [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_010">10</xref>], Coq [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_004">4</xref>], see [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_005">5</xref>]), but the differentiable interval is restricted to open intervals. However, when considering the relationship with integration [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_009">9</xref>], 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 [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_006">6</xref>], but they are the derivatives at the endpoints of an interval and not demonstrated as a differentiation over intervals.</p>
<p>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 [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_001">1</xref>] is an important formula in relation to differentiation and integration, extending recent formalized results [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_007">7</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0002_ref_008">8</xref>] in the latter field of research.</p>
</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.

Differentiation on Interval

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

{"article-title":"Differentiation on Interval"}

This article generalizes the differential method on intervals, using the Mizar system [2], [3], [12]. Differentiation of real one-variable functions is...

Differentiation on Interval

Online veröffentlicht: 26. Sept. 2023

Seitenbereich: 9 - 21

Akzeptiert: 31. März 2023

DOI: https://doi.org/10.2478/forma-2023-0002

Schlüsselwörter
differentiation on closed interval, chain rule

© 2023 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Differentiation on Interval

Online veröffentlicht: 26. Sept. 2023

Seitenbereich: 9 - 21

Akzeptiert: 31. März 2023

DOI: https://doi.org/10.2478/forma-2023-0002

Schlüsselwörterdifferentiation on closed interval, chain rule

© 2023 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Schlüsselwörter
differentiation on closed interval, chain rule