Differentiability
We will now use our work on derivatives to define a notion of differentiable function and prove its main properties.
Throughout this section, a,b will be real numbers with a < b, I will denote the interval [a,b] and F,G,H will be differentiable functions.
Usually a function F is said to be differentiable in a proper compact interval [a,b] if there exists another function F' such that F' is a derivative of F in that interval. There is a problem in formalizing this definition, as we pointed out earlier on, which is that if we simply write it down as is we are not able to get such a function F' from a hypothesis that F is differentiable.
However, it turns out that this is not altogether the best definition for the following reason: if we say that F is differentiable in [a,b], we mean that there is a partial function F' which is defined in [a,b] and satisfies a certain condition in that interval but nothing is required of the behaviour of the function outside [a,b]. Thus we can argue that, from a mathematical point of view, the F' that we get eliminating a hypothesis of differentiability should be defined exactly on that interval. If we do this, we can quantify over the set of setoid functions in that interval and eliminate the existencial quantifier without any problems.
Definition Diffble_I (a b : IR) (Hab : a [<] b) (F : PartIR) :=
{f' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR |
Derivative_I Hab F (PartInt f')}.
End Definitions.
Section Local_Properties.
From this point on, we just prove results analogous to the ones for derivability.
A function differentiable in [a,b] is differentiable in every proper compact subinterval of [a,b].
A function differentiable in [a,b] is differentiable in every proper compact subinterval of [a,b].
Lemma included_imp_diffble : forall a b Hab c d Hcd F,
⊆ (compact c d (less_leEq _ _ _ Hcd)) (compact a b (less_leEq _ _ _ Hab)) ->
Diffble_I Hab F -> Diffble_I Hcd F.
A function differentiable in an interval is everywhere defined in that interval.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Lemma diffble_imp_inc : forall F, Diffble_I Hab' F -> ⊆ I (Dom F).
If a function has a derivative in an interval then it is differentiable in that interval.
Lemma deriv_imp_Diffble_I : forall F F', Derivative_I Hab' F F' -> Diffble_I Hab' F.
End Local_Properties.
Section Operations.
All the algebraic results carry on.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Section Constants.
Lemma Diffble_I_const : forall c : IR, Diffble_I Hab' [-C-]c.
Lemma Diffble_I_id : Diffble_I Hab' FId.
Lemma Diffble_I_poly : forall p, Diffble_I Hab' (FPoly _ p).
End Constants.
Section Well_Definedness.
Variables F H : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Lemma Diffble_I_wd : ≈ (Compact Hab) F H -> Diffble_I Hab' H.
End Well_Definedness.
Variables F G : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffG : Diffble_I Hab' G.
Lemma Diffble_I_plus : Diffble_I Hab' (F{+}G).
Lemma Diffble_I_inv : Diffble_I Hab' {--}F.
Lemma Diffble_I_mult : Diffble_I Hab' (F{*}G).
Hypothesis Gbnd : bnd_away_zero I G.
Lemma Diffble_I_recip : Diffble_I Hab' {1/}G.
Included.
Qed.
End Operations.
Section Corollaries.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variables F G : PartIR.
Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffG : Diffble_I Hab' G.
Lemma Diffble_I_minus : Diffble_I Hab' (F{-}G).
Lemma Diffble_I_scal : forall c : IR, Diffble_I Hab' (c{**}F).
Lemma Diffble_I_nth : forall n : N, Diffble_I Hab' (F{^}n).
Hypothesis Gbnd : bnd_away_zero I G.
Lemma Diffble_I_div : Diffble_I Hab' (F{/}G).
End Corollaries.
Section Other_Properties.
Differentiability of families of functions is proved by
induction using the constant and addition rules.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Lemma Diffble_I_Sum0 : forall (f : N -> PartIR),
(forall n, Diffble_I Hab' (f n)) -> forall n, Diffble_I Hab' (∑0 n f).
Lemma Diffble_I_Sumx : forall n (f : forall i, i < n -> PartIR),
(forall i Hi, Diffble_I Hab' (f i Hi)) -> Diffble_I Hab' (FSumx n f).
Lemma Diffble_I_Sum : forall (f : N -> PartIR),
(forall n, Diffble_I Hab' (f n)) -> forall m n, Diffble_I Hab' (∑ m n f).
End Other_Properties.
Finally, a differentiable function is continuous.
Let F be a partial function with derivative F' on I.
Let F be a partial function with derivative F' on I.
Lemma diffble_imp_contin_I : forall a b (Hab' : a [<] b) (Hab : a [<=] b) F,
Diffble_I Hab' F -> Continuous_I Hab F.