proposition: Lemma DiscrDerivApply : forall {R : ConstructiveReals} (X : Set) (fn : nat -> @PartialFunction R X) (x : X) (pxn : forall n: nat, Domain (DiscrDeriv X fn n) x) (n : nat) (px : Domain (fn n) x), (CRsum (fun k : nat => partialApply (DiscrDeriv X fn k) x (pxn k)) n == partialApply (fn n) x px).
proof: Proof. induction n. - intros. simpl. apply DomainProp. - intros. transitivity (CRsum (fun k : nat => partialApply (DiscrDeriv X fn k) x (pxn k)) n + partialApply (DiscrDeriv X fn (S n)) x (pxn (S n))). reflexivity. pose proof (DiscrDerivDomainIncReverse X fn x pxn n) as H. specialize (IHn H). rewrite IHn. clear IHn. unfold DiscrDeriv. destruct (pxn (S n)). rewrite (applyXminus (fn (S n)) (fn n)). rewrite (DomainProp (fn (S n)) x d px). rewrite (DomainProp (fn n) x d0 H). rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_r. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions