Derivatives
We will now proceed toward the development of differential calculus. To begin with, the main notion is that of derivative.
At this stage we will not define a notion of differentiable function, mainly because the natural definition (that of being a function which has some derivative) poses some technical problems; thus, we will postpone that part of our work to a subsequent stage.
Derivative is a binary relation in the type of partial functions, dependent (once again) on a compact interval with distinct endpoints. As before, we do not define pointwise differentiability, mainly for coherence reasons. See Bishop 1967 for a discussion on the relative little interest of that concept. The reason for requiring the endpoints to be apart is mainly to be able to derive the usual properties of the derivative relation---namely, that any two derivatives of the same function must coincide.
Let a,b:IR with a < b and denote by I the interval [a,b]. Throughout this chapter, F, F', G, G' and H will be partial functions with domains respectively P, P', Q, Q' and R.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variable F : PartIR.
Definition Derivative_I F' (P':=Dom F') := ⊆ I (Dom F) and ⊆ I (Dom F') and
(forall e, 0 [<] e -> {d : IR | 0 [<] d | forall x y, I x -> I y -> forall Hx Hy Hx',
AbsIR (x[-]y) [<=] d -> AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e[*]AbsIR (y[-]x)}).
End Definitions.
Section Basic_Properties.
Like we did for equality, we begin by stating a lemma that makes proofs of derivation easier in practice.
Lemma Derivative_I_char : forall F F' (P:=Dom F) (P':=Dom F'),
⊆ I (Dom F) -> ⊆ I (Dom F') ->
(forall e, 0 [<] e -> {d : IR | 0 [<] d | forall x y, I x -> I y -> forall Hx Hy Hx',
AbsIR (x[-]y) [<=] d -> AbsIR (F y Hy[-]F x Hx[-]F' x Hx'[*] (y[-]x)) [<=] e[*]AbsIR (y[-]x)}) ->
Derivative_I Hab' F F'.
Derivative is a well defined relation; we will make this explicit for both arguments:
Variables F G H : PartIR.
Lemma Derivative_I_wdl : ≈ I F G ->
Derivative_I Hab' F H -> Derivative_I Hab' G H.
Lemma Derivative_I_wdr : ≈ I F G ->
Derivative_I Hab' H F -> Derivative_I Hab' H G.
Lemma Derivative_I_wdl : ≈ I F G ->
Derivative_I Hab' F H -> Derivative_I Hab' G H.
Lemma Derivative_I_wdr : ≈ I F G ->
Derivative_I Hab' H F -> Derivative_I Hab' H G.
Derivative is unique.
Finally, the set where we are considering the relation is included in the domain of both functions.
Lemma derivative_imp_inc : Derivative_I Hab' F G -> ⊆ I P.
Lemma derivative_imp_inc' : Derivative_I Hab' F G -> ⊆ I Q.
Any function that is or has a derivative is continuous.
Variable Hab'' : a [<=] b.
Lemma deriv_imp_contin'_I : Derivative_I Hab' F G -> Continuous_I Hab'' G.
Included.
Qed.
Lemma deriv_imp_contin_I : Derivative_I Hab' F G -> Continuous_I Hab'' F.
End Basic_Properties.
If G is the derivative of F in a given interval, then G is also the derivative of F in any smaller interval.
Lemma included_imp_deriv : forall a b Hab c d Hcd F F',
⊆ (compact c d (less_leEq _ _ _ Hcd)) (compact a b (less_leEq _ _ _ Hab)) ->
Derivative_I Hab F F' -> Derivative_I Hcd F F'.