Algebraic Operations
We will now prove the main results about deriving functions built from the algebraic operators. Composition presents some tricky questions, and is therefore discussed in a separated context.
F' and G' will be the derivatives, respectively, of F and G.
We begin with some technical stuff that will be necessary for division.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable F : PartIR.
Hypothesis Fbnd : bnd_away_zero I F.
Lemma bnd_away_zero_square : bnd_away_zero I (F{*}F).
Included.
Qed.
End Lemmas.
Section Local_Results.
Local Results
We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Lemma Derivative_I_const : forall c : IR, Derivative_I Hab' [-C-]c [-C-]0.
Included.
Included.
Qed.
Lemma Derivative_I_id : Derivative_I Hab' FId [-C-]1.
Included.
Included.
Qed.
Variables F F' G G' : PartIR.
Hypothesis derF : Derivative_I Hab' F F'.
Hypothesis derG : Derivative_I Hab' G G'.
Lemma Derivative_I_plus : Derivative_I Hab' (F{+}G) (F'{+}G').
Included.
Included.
Qed.
Lemma Derivative_I_inv : Derivative_I Hab' {--}F {--}F'.
Included.
Included.
Qed.
Lemma Derivative_I_mult : Derivative_I Hab' (F{*}G) (F{*}G'{+}F'{*}G).
As was the case for continuity, the rule for the reciprocal function has a side condition.
Hypothesis Fbnd : bnd_away_zero I F.
Lemma Derivative_I_recip : Derivative_I Hab' {1/}F {--} (F'{/}F{*}F).
End Local_Results.
Section Corolaries.
Variables a b : IR.
Hypothesis Hab' : a [<] b.
Variables F F' G G' : PartIR.
Hypothesis derF : Derivative_I Hab' F F'.
Hypothesis derG : Derivative_I Hab' G G'.
From this lemmas the rules for the other algebraic operations follow directly.
Lemma Derivative_I_minus : Derivative_I Hab' (F{-}G) (F'{-}G').
Lemma Derivative_I_scal : forall c : IR, Derivative_I Hab' (c{**}F) (c{**}F').
Lemma Derivative_I_nth : forall n, Derivative_I Hab' (F{^}S n) (nring (S n) {**} (F'{*}F{^}n)).
Included.
Included.
Qed.
Lemma Derivative_I_poly : forall p, Derivative_I Hab' (FPoly _ p) (FPoly _ (_D_ p)).
Hypothesis Gbnd : bnd_away_zero I G.
Lemma Derivative_I_div : Derivative_I Hab' (F{/}G) ((F'{*}G{-}F{*}G') {/}G{*}G).
Included.
Included.
Included.
Qed.
End Corolaries.
Section Derivative_Sums.
The derivation rules for families of functions are easily proved by
induction using the constant and addition rules.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Hypothesis Hab' : a [<] b.
Lemma Derivative_I_Sum0 : forall f f' : N -> PartIR,
(forall n, Derivative_I Hab' (f n) (f' n)) -> forall n, Derivative_I Hab' (∑0 n f) (∑0 n f').
Lemma Derivative_I_Sumx : forall n (f f' : forall i, i < n -> PartIR),
(forall i Hi Hi', Derivative_I Hab' (f i Hi) (f' i Hi')) ->
Derivative_I Hab' (FSumx n f) (FSumx n f').
Lemma Derivative_I_Sum : forall f f' : N -> PartIR, (forall n, Derivative_I Hab' (f n) (f' n)) ->
forall m n, Derivative_I Hab' (∑ m n f) (∑ m n f').
End Derivative_Sums.